feat: accept documentation proposals from anyone

.github/workflows/validate-submission.yml

@@ -72,23 +72,32 @@ jobs:
           [[ "$behind" =~ ^[0-9]+$ ]]
           echo "behind=$behind" >> "$GITHUB_OUTPUT"
 
+      # A documentation proposal (Markdown under docs/, no Lean, no claim) is
+      # accepted here and stops: there is nothing to build, and no candidate
+      # code should run for it. The trusted receiver decides that from the
+      # changed paths, never from the branch name.
       - name: Trusted cheap preflight
+        id: preflight
         env:
           BEHIND_BY: ${{ steps.freshness.outputs.behind || '0' }}
-        run: >-
-          python3 trusted/tools/validate-submission
-          --base-dir "$GITHUB_WORKSPACE/trusted"
-          --candidate-dir "$GITHUB_WORKSPACE/candidate"
-          --preflight-only
-          --behind-by "$BEHIND_BY"
-          --json-out "$GITHUB_WORKSPACE/preflight-report.json"
+        run: |
+          python3 trusted/tools/validate-submission \
+            --base-dir "$GITHUB_WORKSPACE/trusted" \
+            --candidate-dir "$GITHUB_WORKSPACE/candidate" \
+            --preflight-only \
+            --behind-by "$BEHIND_BY" \
+            --json-out "$GITHUB_WORKSPACE/preflight-report.json"
+          docs_only="$(python3 -c 'import json,sys; print(str(json.load(open(sys.argv[1]))["observed"].get("docs_only", False)).lower())' "$GITHUB_WORKSPACE/preflight-report.json")"
+          echo "docs_only=$docs_only" >> "$GITHUB_OUTPUT"
 
       - name: Build trusted validation image
+        if: steps.preflight.outputs.docs_only != 'true'
         run: docker build -f trusted/tools/Dockerfile.validator -t leanfrontier-validator:ci trusted
 
       # The candidate lakefile has already been proven identical to trusted
       # infrastructure. Network is available only for dependency acquisition.
       - name: Fetch pinned dependencies and compiled Mathlib cache
+        if: steps.preflight.outputs.docs_only != 'true'
         run: |
           for attempt in 1 2 3; do
             docker run --rm \
@@ -101,6 +110,7 @@ jobs:
           done
 
       - name: Restricted formal validation
+        if: steps.preflight.outputs.docs_only != 'true'
         run: |
           mkdir -p "$GITHUB_WORKSPACE/report-output"
           chmod 0777 "$GITHUB_WORKSPACE/report-output"

CONTRACT.md

@@ -29,6 +29,14 @@ An ordinary submission also MUST NOT modify
 `lake-manifest.json`, `lean-toolchain`, `CONTRACT.md`, `README.md`,
 `MANIFEST.md`, prompts, tests, or any other trusted infrastructure.
 
+A **documentation proposal** is the one other contribution an ordinary
+contributor may open: a pull request changing only Markdown files under `docs/`,
+with no Lean source and no submission record. It carries no claim, builds
+nothing, and runs no candidate code. `docs/catalogue/` is generated from the
+corpus and `docs/website/` is published under the project's name, so neither is
+prose a submitter may edit. A documentation proposal is never merged
+unattended: a person reads it, because nothing mechanical reads prose.
+
 The receiver rejects binary files, archives, symlinks, generated payloads,
 hidden files outside the permitted source tree, and executable content that is
 not ordinary Lean source. Consumers build LeanFrontier from source and import

CONTRIBUTING.md

@@ -44,6 +44,13 @@ don't hold accepted work back in a queue. Only conjectures have a quota
 Substantive extensions that build on accepted results are especially
 welcome.
 
+## Proposing documentation
+
+A pull request that changes only Markdown under `docs/` needs no claim and no
+Lean source. The receiver accepts it as a documentation proposal and skips the
+build entirely; a maintainer then reads it and merges it. `docs/catalogue/` is
+generated and `docs/website/` is published, so neither can be changed this way.
+
 ## Questions and project maintenance
 
 Use GitHub issues for questions, protocol proposals, and non-sensitive bug

tests/test_validator.py

@@ -188,6 +188,60 @@ def test_a_local_run_detects_a_stale_branch_from_git(self) -> None:
         git("merge", "-q", "main")
         self.assertEqual(frontier_validate.commits_behind("main", repo), 0)
 
+    def docs_tree(self) -> None:
+        for root in (self.base, self.candidate):
+            (root / "docs").mkdir(exist_ok=True)
+            (root / "docs" / "CONTRIBUTION-DIRECTIONS.md").write_text("# directions\n")
+        (self.candidate / "LeanFrontier" / "Algebra" / "New.lean").unlink()
+        (self.candidate / "Submissions" / "valid-bundle.json").unlink()
+
+    def test_a_documentation_only_change_is_accepted_without_a_claim(self) -> None:
+        """Twice a docs PR from the one external contributor was refused for not being a submission.
+
+        `maintenance/` only routes around the submission rules for the owner, so
+        a fork cannot propose documentation at all.
+        """
+        self.docs_tree()
+        (self.candidate / "docs" / "CONTRIBUTION-DIRECTIONS.md").write_text("# directions\n\nnew target\n")
+        status, report = self.validate()
+        self.assertEqual(status, 0, report["diagnostics"])
+        self.assertTrue(report["accepted"])
+        self.assertTrue(report["observed"]["docs_only"])
+
+    def test_a_new_documentation_file_is_accepted(self) -> None:
+        self.docs_tree()
+        (self.candidate / "docs" / "threat-model.md").write_text("# threat model\n")
+        status, report = self.validate()
+        self.assertEqual(status, 0, report["diagnostics"])
+
+    def test_documentation_mixed_with_lean_source_is_rejected(self) -> None:
+        self.docs_tree()
+        (self.candidate / "docs" / "CONTRIBUTION-DIRECTIONS.md").write_text("# directions\n\nnew\n")
+        (self.candidate / "LeanFrontier" / "Algebra" / "Sneak.lean").write_text("theorem sneak : True := trivial\n")
+        status, report = self.validate()
+        self.assertEqual(status, 1)
+        self.assertFalse(report["observed"].get("docs_only"))
+
+    def test_the_published_site_and_catalogue_are_not_documentation(self) -> None:
+        """docs/website is deployed to Pages and docs/catalogue is generated."""
+        for relative in ("docs/website/index.html", "docs/catalogue/index.html"):
+            with self.subTest(path=relative):
+                self.setUp()
+                self.docs_tree()
+                target = self.candidate / relative
+                target.parent.mkdir(parents=True, exist_ok=True)
+                target.write_text("<p>hello</p>\n")
+                status, report = self.validate()
+                self.assertEqual(status, 1)
+                codes = {item["code"] for item in report["diagnostics"]}
+                self.assertIn("PATH_POLICY_VIOLATION", codes)
+
+    def test_documentation_may_not_delete(self) -> None:
+        self.docs_tree()
+        (self.candidate / "docs" / "CONTRIBUTION-DIRECTIONS.md").unlink()
+        status, report = self.validate()
+        self.assertEqual(status, 1)
+
     def test_unauthorized_path_is_rejected(self) -> None:
         (self.candidate / "README.md").write_text("payload")
         self.assert_rejected("PATH_POLICY_VIOLATION")

tests/test_workflow_contract.py

@@ -50,6 +50,14 @@ def test_a_stale_pull_request_is_named_as_stale(self) -> None:
         # Untrusted values reach the shell only through the environment.
         self.assertNotIn("compare/${{", WORKFLOW)
 
+    def test_a_documentation_change_skips_the_lean_stages(self) -> None:
+        self.assertIn('--json-out "$GITHUB_WORKSPACE/preflight-report.json"', WORKFLOW)
+        self.assertIn("docs_only", WORKFLOW)
+        # Every stage that builds or runs candidate code is gated on it.
+        for stage in ("Build trusted validation image", "Fetch pinned dependencies", "Restricted formal validation"):
+            index = WORKFLOW.index(stage)
+            self.assertIn("steps.preflight.outputs.docs_only != 'true'", WORKFLOW[index:index + 900], stage)
+
     def test_receiver_has_restricted_formal_execution_and_report(self) -> None:
         for required in (
             "--network none",

tools/frontier_validate.py

@@ -190,6 +190,21 @@ def is_allowed_path(path: str) -> bool:
     return path.startswith("LeanFrontier/") or SUBMISSION_RE.fullmatch(path) is not None
 
 
+def is_documentation_path(path: str) -> bool:
+    """Prose a contribution may propose on its own, with no Lean and no claim.
+
+    Markdown under `docs/` only. `docs/catalogue/` is generated from the corpus
+    and `docs/website/` is deployed to GitHub Pages, so neither is prose a
+    submitter may edit: a change there would publish under the project's name.
+    """
+    return (
+        path.startswith("docs/")
+        and path.endswith(".md")
+        and not path.startswith("docs/catalogue/")
+        and not path.startswith("docs/website/")
+    )
+
+
 def line_count(path: Path) -> int:
     try:
         return path.read_text(encoding="utf-8").count("\n") + 1
@@ -369,6 +384,15 @@ def static_preflight(base: Path | None, candidate: Path, limits: dict[str, Any],
     changed, before = changed_paths(base, candidate)
     corpus = corpus_skeletons(base)
     report.observations["changed_files"] = sorted(changed)
+    # A documentation proposal: prose, no Lean, no claim, nothing to build. It
+    # is admitted by the same trusted receiver as everything else, and merged by
+    # a human like every other change that is not an ordinary submission.
+    if changed and all(path is not None and is_documentation_path(relative) for relative, path in changed.items()):
+        oversized = [relative for relative, path in changed.items() if path is not None and path.stat().st_size > limits["max_individual_file_bytes"]]
+        for relative in oversized:
+            report.reject("RESOURCE_LIMIT_EXCEEDED", "individual file exceeds policy limit", relative)
+        report.observations["docs_only"] = not oversized
+        return {}, None
     if len(changed) > limits["max_changed_files"]:
         report.reject("RESOURCE_LIMIT_EXCEEDED", "too many changed files")
     changed_bytes = 0
@@ -1129,7 +1153,7 @@ def main(argv: list[str] | None = None) -> int:
                 base, candidate, submitted_modules(changed),
                 [e for e in metadata.get("entrypoints", []) if isinstance(e, str)],
                 metadata, load_json(DEFAULT_CONJECTURE), report)
-        if report.accepted and not args.preflight_only:
+        if report.accepted and not args.preflight_only and not report.observations.get("docs_only"):
             if metadata is None:
                 report.reject("SCHEMA_INVALID", "no valid metadata record was available for audit")
             else: