diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 6ac820a..d3fa846 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -14,6 +14,17 @@ concurrency: env: ELAN_HOME: /home/runner/.elan + # The headline results. Kept in the workflow, not in Verify.lean or spec/, so that dropping one + # from the axiom dashboard or from the statement files fails CI. + HEADLINE_RESULTS: >- + SemioticBVP.exists_isWeakCoherentConfiguration + SemioticBVP.exists_pos_isWeakCoherentConfiguration + SemioticGraph.exists_pos_graph + SemioticGraph.exists_pos_graph_of_unweighted + spectral_characterization_1d + linfty_bound_algebraic + monotone_fixed_point_between + scaling_uniqueness jobs: # CONTRACT: org ruleset requires this exact check name 'build' @@ -86,7 +97,7 @@ jobs: run: lake lint # Verify.lean lists the selected declarations, which must include the headline results named - # below. Each needs exactly one record, and every record may use only propext, + # in HEADLINE_RESULTS. Each needs exactly one record, and every record may use only propext, # Classical.choice and Quot.sound. - name: Check axioms if: ${{ !cancelled() && steps.build.outcome == 'success' }} @@ -94,7 +105,7 @@ jobs: set -o pipefail lake env lean -DwarningAsError=true CdFormal/Verify.lean 2>&1 | tee "$RUNNER_TEMP/axioms.txt" python3 - "$RUNNER_TEMP/axioms.txt" <<'EOF' - import collections, pathlib, re, sys + import collections, os, pathlib, re, sys source = pathlib.Path("CdFormal/Verify.lean").read_text(encoding="utf-8") expected = re.findall(r"^#print axioms (\S+)\s*$", source, re.M) lines = [] @@ -116,13 +127,9 @@ jobs: errors.append(f"{m[1]} uses {sorted(used - allowed)}") if not expected: errors.append("Verify.lean selects no declarations") - # Kept here, not in Verify.lean, so that deselecting a headline result fails the check. - headline = ["SemioticBVP.exists_isWeakCoherentConfiguration", - "SemioticBVP.exists_pos_isWeakCoherentConfiguration", - "SemioticGraph.exists_pos_graph", - "SemioticGraph.exists_pos_graph_of_unweighted", - "spectral_characterization_1d", "linfty_bound_algebraic", - "monotone_fixed_point_between", "scaling_uniqueness"] + headline = os.environ["HEADLINE_RESULTS"].split() + if not headline: + errors.append("HEADLINE_RESULTS is empty") for name in headline: if name not in expected: errors.append(f"headline result {name} is not selected in Verify.lean") @@ -142,6 +149,100 @@ jobs: "results, one record each, using only propext, Classical.choice and Quot.sound.") EOF + # spec/Spec.lean restates each headline result with `sorry` as its proof: the statement is + # the specification. spec/Check.lean compares every statement there with the library + # declaration of the same name (type up to binder names, a theorem with a proof term, + # axioms within the allowlist) and rejects a statement file that proves instead of states. + - name: Check statement files + if: ${{ !cancelled() && steps.build.outcome == 'success' }} + run: | + set -o pipefail + # Split on any whitespace, so a list of only newlines or tabs counts as empty. + read -r -d '' -a headline <<< "$HEADLINE_RESULTS" || true + if [ "${#headline[@]}" -eq 0 ]; then + echo "::error::HEADLINE_RESULTS is empty" + exit 1 + fi + # spec/ holds the statement file and its checker, nothing else. + specfiles=$(git ls-files 'spec/*') + status=0 + others=$(printf '%s\n' "$specfiles" | grep -v -x -F -e spec/Spec.lean -e spec/Check.lean) || + status=$? + if [ "$status" -gt 1 ]; then + echo "::error::could not list spec/ (grep exit $status)" + exit 1 + fi + if [ -n "$others" ]; then + echo "::error::unexpected files in spec/: $others" + exit 1 + fi + lake build Spec 2>&1 | tee "$RUNNER_TEMP/spec-build.txt" + # The statement file's own messages, read as JSON from Lean with the package's options + # (linters included), not by filtering Lake's text output. Allowed: its sorry warnings. + # Any other message (information included: the file must not print), or any output that + # is not JSON, fails the step. Warnings in the + # library are the build step's concern: it runs with warnings as errors. + lake --quiet lean spec/Spec.lean -- --json > "$RUNNER_TEMP/spec-messages.jsonl" \ + 2> "$RUNNER_TEMP/spec-stderr.txt" + if [ -s "$RUNNER_TEMP/spec-stderr.txt" ]; then + echo "::error::Lean wrote to stderr while elaborating the statement file" + cat "$RUNNER_TEMP/spec-stderr.txt" + exit 1 + fi + python3 - "$RUNNER_TEMP/spec-messages.jsonl" "$RUNNER_TEMP/spec-sorries.txt" <<'EOF' + import json, os, sys + spec = os.path.realpath("spec/Spec.lean") + sorries, other = 0, [] + for line in open(sys.argv[1], encoding="utf-8"): + if not line.strip(): + continue + try: + m = json.loads(line) + except json.JSONDecodeError: + print(f"::error::output from Lean that is not JSON: {line.strip()}") + sys.exit(1) + if (m["severity"] == "warning" and m.get("kind") == "hasSorry" + and os.path.realpath(m["fileName"]) == spec): + sorries += 1 + continue + other.append(f'{m["fileName"]}:{m["pos"]["line"]}: {m["severity"]}: {m["data"]}') + if other: + print("::error::the statement file has a message other than its sorry warnings") + print("\n".join(other)) + sys.exit(1) + if sorries == 0: + print("::error::the statement file reports no sorry warning") + sys.exit(1) + open(sys.argv[2], "w").write(f"{sorries}\n") + print(f"{sorries} sorry warnings and no other message in spec/Spec.lean") + EOF + lake env lean -DwarningAsError=true spec/Check.lean 2>&1 | tee "$RUNNER_TEMP/spec.txt" + # A Lean panic prints, substitutes a default value and continues with exit code 0. + status=0 + grep -q -F 'PANIC' "$RUNNER_TEMP/spec.txt" || status=$? + if [ "$status" -ne 1 ]; then + echo "::error::Lean panicked while checking the statement files (grep exit $status)" + exit 1 + fi + # One sorry warning per statement: a sorry anywhere else (an example, say) is not a + # statement the comparator checked. + statements=$(sed -n 's/^\([0-9][0-9]*\) statements match the library$/\1/p' "$RUNNER_TEMP/spec.txt") + sorries=$(cat "$RUNNER_TEMP/spec-sorries.txt") + # String comparison of two single numbers: a malformed count must not fall through. + if ! [[ "$statements" =~ ^[0-9]+$ && "$sorries" =~ ^[0-9]+$ ]] || + [ "$statements" != "$sorries" ]; then + echo "::error::$sorries sorry warnings for ${statements:-no} checked statements" + exit 1 + fi + missing="" + for name in "${headline[@]}"; do + grep -qxF "SPEC OK $name" "$RUNNER_TEMP/spec.txt" || missing="$missing $name" + done + if [ -n "$missing" ]; then + echo "::error::headline results without a matching statement:$missing" + exit 1 + fi + # Every Lean name written in inline code in the README and the docs, and every declaration # shown in a Lean code block there, must resolve. - name: Check documented names @@ -177,29 +278,35 @@ jobs: fi echo "$(grep -c '^#check' "$RUNNER_TEMP/DocNames.lean") documented names resolve." - # No axiom may be declared in any CdFormal module, even one that no selected declaration - # uses. The check reads the compiled environment, so it cannot be fooled by layout. It first - # proves it can fail: a module declaring a two-line axiom must be reported. - - name: Check that no axiom is declared + # No axiom and no opaque constant may be declared in any CdFormal module, even one that no + # selected declaration uses: the kernel cannot see an opaque constant's value, and neither + # #print axioms nor a text search reports one. The check reads the compiled environment, so + # it cannot be fooled by layout. It first proves it can fail: a module declaring a two-line + # axiom and an opaque constant must have both reported. + - name: Check that no axiom or opaque constant is declared if: ${{ !cancelled() && steps.build.outcome == 'success' }} run: | cat > "$RUNNER_TEMP/axiom_check.lean" <<'EOF' open Lean in #eval show CoreM Unit from do let env ← getEnv - let mut found := #[] + let mut axioms := #[] + let mut opaques := #[] let mut modules := 0 for mod in env.header.moduleNames, data in env.header.moduleData do if mod.getRoot == `CdFormal then modules := modules + 1 for c in data.constants do - if c matches .axiomInfo _ then found := found.push c.name - unless found.isEmpty do throwError "axioms declared in CdFormal: {found}" - IO.println s!"no axiom declared in any of {modules} CdFormal modules" + if c matches .axiomInfo _ then axioms := axioms.push c.name + if c matches .opaqueInfo _ then opaques := opaques.push c.name + unless axioms.isEmpty && opaques.isEmpty do + throwError "axioms declared in CdFormal: {axioms}; opaque constants: {opaques}" + IO.println s!"no axiom or opaque constant declared in {modules} CdFormal modules" EOF fixture=CdFormal/CiAxiomFixture.lean trap 'rm -f "$fixture" .lake/build/lib/lean/CdFormal/CiAxiomFixture.*' EXIT - printf 'import CdFormal.Basic\n\naxiom\n ciAxiomFixture : False\n' > "$fixture" + printf '%s\n' 'import CdFormal.Basic' '' 'axiom' ' ciAxiomFixture : False' '' \ + 'opaque ciOpaqueFixture : Nat' > "$fixture" lake build CdFormal.CiAxiomFixture { echo 'import CdFormal.CiAxiomFixture'; cat "$RUNNER_TEMP/axiom_check.lean"; } \ > "$RUNNER_TEMP/SelfTest.lean" @@ -207,9 +314,9 @@ jobs: status=0 lake env lean "$RUNNER_TEMP/SelfTest.lean" > "$RUNNER_TEMP/selftest.txt" 2>&1 || status=$? cat "$RUNNER_TEMP/selftest.txt" - if [ "$status" -eq 0 ] || - ! grep -qF 'axioms declared in CdFormal: [ciAxiomFixture]' "$RUNNER_TEMP/selftest.txt"; then - echo "::error::the axiom self-test did not report ciAxiomFixture" + expected='axioms declared in CdFormal: [ciAxiomFixture]; opaque constants: [ciOpaqueFixture]' + if [ "$status" -eq 0 ] || ! grep -qF "$expected" "$RUNNER_TEMP/selftest.txt"; then + echo "::error::the self-test did not report ciAxiomFixture and ciOpaqueFixture" exit 1 fi rm -f "$fixture" .lake/build/lib/lean/CdFormal/CiAxiomFixture.* @@ -223,7 +330,8 @@ jobs: shell: python run: | import pathlib, re, subprocess, sys - files = subprocess.run(["git", "ls-files", "CdFormal.lean", "CdFormal/*.lean"], + files = subprocess.run(["git", "ls-files", "CdFormal.lean", "CdFormal/*.lean", + "spec/*.lean"], capture_output=True, text=True, check=True).stdout.split() header = re.compile(r"/-\nCopyright \(c\) 20\d\d [^\n]+\. All rights reserved\.\n" r"Released under Apache 2\.0 license as described in the file LICENSE\.\n" @@ -243,8 +351,9 @@ jobs: sys.exit("header check failed:\n " + "\n ".join(bad or ["no files"])) print(f"{len(files)} files have a copyright header and a module docstring after the imports.") - # 'sorry' and 'sorryAx' may not appear anywhere in the Lean sources, comments included, and - # no axiom may be declared. + # 'sorry' and 'sorryAx' may not appear anywhere in the library sources, comments included. + # The statement files under spec/ are outside this audit: their proofs are sorry by design, + # and the statement-file check requires it. - name: Audit placeholders if: ${{ !cancelled() }} run: | diff --git a/AGENTS.md b/AGENTS.md index d5c4ebb..89cec8d 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -28,7 +28,9 @@ A formalization of the existence theory for the Creative Determinant problem ## Invariants -- **No `sorry` on the default branch.** Every declaration is fully proved before merge. +- **No `sorry` in the library on the default branch.** Every declaration under `CdFormal/` is + fully proved before merge. The statement files under `spec/` are the one exception: each + restates a headline result with `sorry` as its proof, and CI requires that. - **No `axiom` declarations.** Classical results that are not proved are assumed through a typeclass or structure field (see *Assumed results*, which needs approval), never through `axiom`. @@ -59,13 +61,24 @@ lake exe cache get # Mathlib oleans; never bui lake build --wfail # warnings are errors (includes sorry) lake lint # Mathlib environment linters lake env lean -DwarningAsError=true /Verify.lean # axiom dashboard +lake build Spec && lake env lean spec/Check.lean # statement files against the library ``` - `CdFormal/Verify.lean` holds exactly one `#print axioms` record per selected declaration: every headline result and the supporting declarations the docs cite. The headline results - are listed in the CI workflow, not in `Verify.lean`, so dropping one from the dashboard - fails CI; add a new headline result to both. Every record may use only `propext`, - `Classical.choice` and `Quot.sound`. + are listed once, in the CI workflow (`HEADLINE_RESULTS`), not in `Verify.lean` or `spec/`, + so dropping one from the dashboard or from the statement files fails CI. Add a new headline + result to all three: the workflow list, a `#print axioms` record, and a statement in + `spec/Spec.lean` copied from the source with its proof replaced by `sorry`. Every record may + use only `propext`, `Classical.choice` and `Quot.sound`. +- `spec/` holds `Spec.lean` and `Check.lean` only; CI rejects any other file there. The only + messages `spec/Spec.lean` may produce are its own `sorry` warnings, one per statement, read by + CI as Lean's JSON messages with the package's linters on. Each statement's proof is `sorry` + itself, not a proof that uses `sorry` somewhere. +- A statement file states; it does not prove. `spec/Check.lean` rejects a statement whose proof + is not `sorry`, a statement whose type differs from the library declaration of the same name + (binder names and annotations aside), a library declaration that is not a theorem, and a + library proof whose axioms leave the allowlist. - If the sandbox cannot install Lean or fetch the Mathlib cache, push to a draft PR and let CI build and verify. Report which checks ran where; never claim a local build that did not happen. @@ -76,9 +89,12 @@ lake env lean -DwarningAsError=true /Verify.lean # axiom dashboard - Test the checkers themselves. An axiom or `sorry` gate that silently passes is worse than none (a pipe without `pipefail` once hid Lean failures here). When you add or change a gate, also add a small negative fixture that must fail it and a snapshot of expected - axiom output that its parser must accept. This repo's CI has neither yet: after changing - the axiom check or the audit, test it by hand against a file that uses `sorry` or declares - an `axiom`. + axiom output that its parser must accept. In this repo's CI only the environment check + carries a fixture (an `axiom` and an `opaque` constant it must report). After changing the + axiom dashboard parser, the statement-file comparator or the audit, test them by hand: a + file that uses `sorry`, a statement with a changed hypothesis, a statement proved instead + of stated, and a library proof that uses native evaluation (which declares an auxiliary + axiom under Lean v4.34.1). - Change `lake-manifest.json` only in an intentional dependency bump. No CI guard enforces this here; check the diff yourself. - If a repo has a docs site, `uv run zensical build` must succeed; CI also checks the @@ -88,14 +104,18 @@ lake env lean -DwarningAsError=true /Verify.lean # axiom dashboard - `lake build --wfail` of the root and every module, then `lake lint`; - the axiom check: the selection includes every headline result, one record each, all within the allowlist; + - the statement-file check: every headline result has a statement in `spec/Spec.lean`, and + every statement there matches its library declaration as described above; - the documented-names check: every inline-code token in the README and docs that looks like a Lean name containing an uppercase letter, `_` or `.`, and every declaration shown in a Lean code block there, must resolve (all-lowercase names are not checked); - the header check: every file has the copyright header and a module docstring after the imports (Lean itself rejects an `import` after any command, so imports come first); - - the placeholder audit: no `sorry` or `sorryAx` anywhere, and no line that starts an - `axiom` declaration (a text search; `#print axioms` still catches any axiom a selected - result uses); + - the placeholder audit: no `sorry` or `sorryAx` anywhere in the library sources, comments + included (a text search; `spec/` is outside it by design); + - the environment check: no module of the library declares an `axiom` or an `opaque` + constant, read from the compiled environment, after a self-test with a fixture that + declares both; - the docs build, and a link check that also verifies fragments. Everything else in this file is a convention to follow, not an automated gate. - If a repo has a `Makefile`, use its targets (`build`, `verify`, `audit`, `lint`) as @@ -407,5 +427,18 @@ Aristotle grinds leaf lemmas and detects dependencies. It is not the theorem arc `pp.all`; none of them belongs in a leaf proof. - Rebuild with `lake build --wfail`: Aristotle doesn't run the project's style linters. - Before trusting output, check Aristotle's Lean version against `lean-toolchain`. +- Elaborating a file runs code (`#eval`, `initialize`, tactics, macros), so elaborate a + returned file in a sandbox before it touches the repository: no network, home directory + hidden, the project read-only. With bubblewrap, from the project root: + + ```bash + bwrap --ro-bind /usr /usr --symlink usr/lib /lib --symlink usr/lib /lib64 \ + --symlink usr/bin /bin --ro-bind /etc /etc --tmpfs "$HOME" \ + --ro-bind "$HOME/.elan" "$HOME/.elan" --ro-bind "$PWD" "$PWD" \ + --ro-bind /untrusted --proc /proc --dev /dev --tmpfs /tmp \ + --unshare-all --die-with-parent --chdir "$PWD" lake env lean /untrusted/.lean + ``` + + Adjust the binds to where elan and the toolchain live on your machine. - Keep raw prover artifacts and run logs out of the public repository. Commit only the rewritten proofs, and credit Aristotle in the README. diff --git a/CdFormal/Theorems.lean b/CdFormal/Theorems.lean index 184c608..8ba4a39 100644 --- a/CdFormal/Theorems.lean +++ b/CdFormal/Theorems.lean @@ -93,7 +93,10 @@ checked; the hypotheses are assumed and appear as arguments. -/ Uses `PDEInfra.T_compact`, `PDEInfra.linfty_bound`, `PDEInfra.schaefer`, `PDEInfra.fixed_point_nonneg` and `SolutionOperator.T_fixed_point`. With the default - `SemioticBVP.equation`, Φ ≡ 0 is already a solution (`zero_solves_equation`). -/ + `SemioticBVP.equation`, Φ ≡ 0 is already a solution (`zero_solves_equation`). + + Conditional: the obligation to meet these hypotheses is the named gap `gap:pde-infra` + (docs/explanation/axiom-boundary.md). -/ theorem SemioticBVP.exists_isWeakCoherentConfiguration (bvp : SemioticBVP n M) (solOp : SolutionOperator bvp) @@ -117,7 +120,10 @@ theorem SemioticBVP.exists_isWeakCoherentConfiguration Note: The paper's Thm 3.16 says "assume the hypotheses of Thm 3.12" (including bounded b). This Lean statement omits `B`/`hB` because `monotone_iteration` uses sub/super-solution theory that does not - require an explicit bound on b. -/ + require an explicit bound on b. + + Conditional: the obligation to meet these hypotheses is the named gap `gap:pde-infra` + (docs/explanation/axiom-boundary.md). -/ theorem SemioticBVP.exists_pos_isWeakCoherentConfiguration (bvp : SemioticBVP n M) (solOp : SolutionOperator bvp) diff --git a/README.md b/README.md index 6054f03..6603b39 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ A Lean 4 and Mathlib (v4.34.1) formalization of the existence theory in N. Spence, *The Creative Determinant: Autopoietic Closure as a Nonlinear Elliptic Boundary Value Problem with Lean 4-Verified Existence Conditions* (2026). The problem is −ΔΦ = a|∇Φ| + bΦ − c(Φ₊)ᵖ in M with Φ = 0 on ∂M, where a = κγμ and p > 1. Documentation: [docs.projectnavi.ai/cd-formalization](https://docs.projectnavi.ai/cd-formalization/). -- **Continuum results (conditional).** `SemioticBVP.exists_isWeakCoherentConfiguration` gives a nonnegative solution when `b` is bounded above, and `SemioticBVP.exists_pos_isWeakCoherentConfiguration` one that is positive at some interior point when a supplied principal eigenvalue is negative. Both are derived from the hypotheses `PDEInfra` and `SolutionOperator`, which stand in for elliptic results not proved here; the manifold's Laplacian, gradient norm and boundary are abstract data. +- **Continuum results (conditional).** `SemioticBVP.exists_isWeakCoherentConfiguration` gives a nonnegative solution when `b` is bounded above, and `SemioticBVP.exists_pos_isWeakCoherentConfiguration` one that is positive at some interior point when a supplied principal eigenvalue is negative. Both are derived from the hypotheses `PDEInfra` and `SolutionOperator`, which stand in for elliptic results not proved here; the manifold's Laplacian, gradient norm and boundary are abstract data. The open obligation is the named gap `gap:pde-infra` (see the assumption boundary page). - **Finite graphs (proved).** For the discretization selected here, on a finite weighted graph with a Dirichlet boundary, `SemioticGraph.exists_pos_graph` gives a solution positive at every interior vertex when the interior graph is connected, the principal eigenvalue of L − diag(b) is negative, and a(x) ≤ √w(x,y) and a(y) ≤ √w(x,y) for every edge of positive weight between distinct interior vertices x and y. The operators and eigendata are constructed. The edge condition is sufficient for this proof, not claimed necessary, and holds for 0/1 weights (`SemioticGraph.exists_pos_graph_of_unweighted`). - **Supporting lemmas**, among them `spectral_characterization_1d`, `linfty_bound_algebraic`, `monotone_fixed_point_between` (Knaster–Tarski) and `scaling_uniqueness`. @@ -14,9 +14,10 @@ The [assumption boundary](https://docs.projectnavi.ai/cd-formalization/explanati lake exe cache get lake build --wfail lake env lean -DwarningAsError=true CdFormal/Verify.lean +lake build Spec && lake env lean spec/Check.lean ``` -`CdFormal/Verify.lean` prints the axioms of the headline results and the declarations the documentation cites; CI requires each to use only `propext`, `Classical.choice` and `Quot.sound`. This check cannot see hypotheses: `PDEInfra` appears in the signatures of the conditional theorems. +`CdFormal/Verify.lean` prints the axioms of the headline results and the declarations the documentation cites; CI requires each to use only `propext`, `Classical.choice` and `Quot.sound`. This check cannot see hypotheses: `PDEInfra` appears in the signatures of the conditional theorems. `spec/Spec.lean` states every headline result with `sorry` as its proof; `spec/Check.lean` checks the library against those statements, so a reader can audit a headline claim from the statement file alone. ## Credit and license diff --git a/docs/explanation/axiom-boundary.md b/docs/explanation/axiom-boundary.md index be1de62..6e405db 100644 --- a/docs/explanation/axiom-boundary.md +++ b/docs/explanation/axiom-boundary.md @@ -95,6 +95,10 @@ Classically: \(\varepsilon\varphi_1\) is a sub-solution, a large constant is a s Replacing a field by a proof would also require the operators to be constructed from the metric and the boundary to be the boundary of a manifold with boundary. +## The named gap + +The obligation the two continuum theorems leave open is named `gap:pde-infra`, so that it can be cited wherever they are. It is: for the concrete problem on a compact manifold with boundary, construct a solution operator and prove the fields of `PDEInfra` and `SolutionOperator` (and, for the second theorem, construct the principal eigendata), or prove the conclusions without them. Until then `SemioticBVP.exists_isWeakCoherentConfiguration` and `SemioticBVP.exists_pos_isWeakCoherentConfiguration` are implications. Nothing in the library instantiates their hypotheses, and an axiom report cannot show whether they can be met: `#print axioms` lists Lean axioms, not hypotheses. The statement file `spec/Spec.lean` shows both theorems with every hypothesis written out. + ## The finite-graph theorem `SemioticGraph.exists_pos_graph` takes no hypothesis of the kind above. On a finite graph the Laplacian and the gradient norm are defined from the weights, the principal eigenvalue is defined as an infimum, attained when the interior is nonempty, and shown to have a positive eigenvector when the interior graph is connected, and the fixed point comes from `monotone_fixed_point_between`. Its hypotheses (a connected interior graph, a negative principal eigenvalue, and the edge-dominance condition) are mathematical conditions stated in its signature; see the [theorem catalog](../reference/theorems.md#finite-graph-existence). diff --git a/docs/reference/theorems.md b/docs/reference/theorems.md index 8a9391f..46abbc7 100644 --- a/docs/reference/theorems.md +++ b/docs/reference/theorems.md @@ -50,7 +50,7 @@ theorem SemioticBVP.exists_isWeakCoherentConfiguration (∀ x, Phi x ≥ 0) ``` -Uses `PDEInfra.T_compact`, `PDEInfra.linfty_bound`, `PDEInfra.schaefer`, `PDEInfra.fixed_point_nonneg` and `SolutionOperator.T_fixed_point`. With the default equation, \(\Phi \equiv 0\) is already such a solution (`zero_solves_equation`, below). +Uses `PDEInfra.T_compact`, `PDEInfra.linfty_bound`, `PDEInfra.schaefer`, `PDEInfra.fixed_point_nonneg` and `SolutionOperator.T_fixed_point`. With the default equation, \(\Phi \equiv 0\) is already such a solution (`zero_solves_equation`, below). Conditional on the named gap `gap:pde-infra` ([assumption boundary](../explanation/axiom-boundary.md)). ### Solution positive at an interior point (Paper Theorem 3.16) @@ -68,7 +68,7 @@ theorem SemioticBVP.exists_pos_isWeakCoherentConfiguration (∃ x, x ∉ bvp.boundary ∧ Phi x > 0) ``` -Uses `PDEInfra.monotone_iteration`, `PDEInfra.fixed_point_nonneg` and `SolutionOperator.T_fixed_point`. Positivity is at one interior point. +Uses `PDEInfra.monotone_iteration`, `PDEInfra.fixed_point_nonneg` and `SolutionOperator.T_fixed_point`. Positivity is at one interior point. Conditional on the named gap `gap:pde-infra` ([assumption boundary](../explanation/axiom-boundary.md)). ## Algebra and real analysis diff --git a/docs/reference/verification-audit.md b/docs/reference/verification-audit.md index b3ede6a..ded7a2f 100644 --- a/docs/reference/verification-audit.md +++ b/docs/reference/verification-audit.md @@ -15,8 +15,8 @@ What is checked, how, and what remains outside the formalization. Toolchain and | Lemma 3.7 (compactness of \(T\)) | `PDEInfra.T_compact` | Hypothesis | | Lemma 3.10 (L∞ bound) | `PDEInfra.linfty_bound`; `linfty_bound_algebraic` | Hypothesis; algebraic step proved | | Lemma 3.11 (\(C^{1,\alpha}\) bound) | none | Not formalized | -| Theorem 3.12 (existence) | `SemioticBVP.exists_isWeakCoherentConfiguration` | Proved from `PDEInfra` | -| Theorem 3.16 (nontrivial existence) | `SemioticBVP.exists_pos_isWeakCoherentConfiguration` | Proved from `PDEInfra`; positive at one interior point | +| Theorem 3.12 (existence) | `SemioticBVP.exists_isWeakCoherentConfiguration` | Proved from `PDEInfra`; named gap `gap:pde-infra` | +| Theorem 3.16 (nontrivial existence) | `SemioticBVP.exists_pos_isWeakCoherentConfiguration` | Proved from `PDEInfra`; named gap `gap:pde-infra`; positive at one interior point | | Section 3.4 (spectral condition, 1D) | `spectral_characterization_1d` | Algebraic inequality proved; eigenvalue identification not formalized | | Open Problem 3 (uniqueness) | `scaling_uniqueness` | Rules out solution multiples \(k\Phi\), \(k > 1\); uniqueness open | @@ -32,14 +32,15 @@ The required `build` job, on every pull request and on `main`: - runs the Mathlib environment linters (`lake lint`); - runs `CdFormal/Verify.lean` with warnings as errors and requires exactly one `#print axioms` record for each listed declaration, each using only `propext`, `Classical.choice` and `Quot.sound`; - fails if a headline result is missing from that list: the two continuum existence theorems, `SemioticGraph.exists_pos_graph` and its unweighted corollary, and the supporting lemmas the README names; +- checks the statement files: `spec/Spec.lean` restates every headline result with `sorry` as its proof, and `spec/Check.lean` requires each statement there to match the library declaration of the same name (the same type up to binder names and annotations, a theorem with a proof term, axioms within the allowlist), each statement's proof to be `sorry`, and every headline result to have a statement; - resolves, with `#check`, every inline-code token in the README and on these pages that looks like a Lean name containing an uppercase letter, `_` or `.`, and every declaration shown in a Lean code block there (all-lowercase names are not checked); - checks that every Lean file has the copyright header and a module docstring after its imports (Lean itself requires imports to come first); - fails if `sorry` or `sorryAx` appears anywhere in the Lean sources, comments included; -- fails if any module of the library declares an `axiom`, by inspecting the compiled environment rather than the source text; the check first confirms it reports an `axiom` declared across two lines. +- fails if any module of the library declares an `axiom` or an opaque constant, by inspecting the compiled environment rather than the source text; the check first confirms it reports both, an `axiom` declared across two lines and an `opaque` constant. An opaque constant is not an axiom, but the kernel cannot see its value and neither `#print axioms` nor a text search reports it. A proof by native evaluation (the tactic native_decide) declares an auxiliary axiom under Lean v4.34.1, so it fails this check and the axiom dashboard, and Mathlib's linter rejects it under warnings as errors. The `docs` job builds this site, checks that every navigation page is built and every built page is in the navigation, and checks local links, assets and anchors. It does not check external links. -These checks establish that the proofs compile against the pinned Mathlib and use no further axioms. They do not discharge hypotheses such as `PDEInfra`, and resolving a name does not show that the prose describes the statement; the statements on these pages are copied from the source. +These checks establish that the proofs compile against the pinned Mathlib and use no further axioms. They do not discharge hypotheses such as `PDEInfra` (the named gap `gap:pde-infra`), and resolving a name does not show that the prose describes the statement; the statements on these pages are copied from the source. ## Known limitations diff --git a/lakefile.toml b/lakefile.toml index 80f2ce1..d5de635 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -25,3 +25,9 @@ rev = "v4.34.1" [[lean_lib]] name = "CdFormal" + +# Statement files: the headline results restated with `sorry` as the specification, compared +# with the library by spec/Check.lean in CI. Not a default target; never imported by CdFormal. +[[lean_lib]] +name = "Spec" +srcDir = "spec" diff --git a/spec/Check.lean b/spec/Check.lean new file mode 100644 index 0000000..651447c --- /dev/null +++ b/spec/Check.lean @@ -0,0 +1,100 @@ +/- +Copyright (c) 2026 Nelson Spence. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Nelson Spence +-/ +import CdFormal +import Spec + +/-! +# Comparator for the statement files + +`#check_statements` takes every theorem `Spec.name` in the module `Spec` (`spec/Spec.lean`) and +checks it against the library declaration `name`: + +1. the statement's proof is `sorry` itself (`isBareSorry`: exactly Lean's sorry under the + statement's binders, not applied to anything), so the statement file states and does not + prove; +2. the library declaration exists and is a theorem, not an axiom or an opaque constant; +3. the two types are equal up to binder names and annotations, after the statement's universe + parameters are replaced by the library's; +4. the library proof uses no axiom outside `propext`, `Classical.choice` and `Quot.sound` + (the walk is `Lean.collectAxioms`, transitive over the proof term). + +It prints `SPEC OK name` for each match and fails with every mismatch listed. CI also requires +each headline result to have a `SPEC OK` line. Run with `lake env lean spec/Check.lean` after +`lake build Spec`. +-/ + +open Lean Elab Command + +/-- The axioms a library proof may use. -/ +def specAllowedAxioms : List Name := [``propext, ``Classical.choice, ``Quot.sound] + +/-- Whether `v`, the proof of a statement, is `sorry` itself: under the statement's binders, + Lean's labelled sorry `sorryAx (∀ tag : Name, T) false tag`, with a closed label built from + `Lean.Name` constructors and `Nat` literals only, or the unlabelled `sorryAx T false`. A sorry + applied to further arguments, wrapped in `let` or `have`, or inside an otherwise real proof + is not. The kernel has already checked that `T` is the statement's conclusion. -/ +def isBareSorry (v : Expr) : Bool := Id.run do + let mut v := v.consumeMData + while v.isLambda do + v := v.bindingBody!.consumeMData + unless v.isAppOf ``sorryAx do return false + match v.getAppArgs with + | #[_, synthetic] => return synthetic.isConstOf ``Bool.false + | #[t, synthetic, tag] => + -- The label is data: `Lean.Name` constructors and `Nat` literals (`OfNat.ofNat`). + let nameOnly := tag.getUsedConstants.all (fun c => (`Lean.Name).isPrefixOf c || + [``OfNat.ofNat, ``Nat, ``instOfNatNat].contains c) + match t.consumeMData with + | .forallE _ (.const ``Lean.Name []) body _ => + return synthetic.isConstOf ``Bool.false && !tag.hasLooseBVars && !tag.hasFVar && + !tag.hasMVar && nameOnly && !body.hasLooseBVar 0 + | _ => return false + | _ => return false + +/-- Check every statement of the module `Spec`; see the module docstring. -/ +elab "#check_statements" : command => do + let env ← getEnv + let mut statements : Array ConstantInfo := #[] + for mod in env.header.moduleNames, data in env.header.moduleData do + if mod == `Spec then + statements := data.constants.filter (fun c => !c.name.isInternal) + if statements.isEmpty then + throwError "no statements found in the module Spec" + let mut errors : Array MessageData := #[] + for s in statements do + let name := s.name.replacePrefix `Spec Name.anonymous + let .thmInfo st := s + | errors := errors.push m!"{s.name}: a statement file may declare theorems only"; continue + -- The proof must be `sorry` itself (see `isBareSorry`): depending on `sorryAx` somewhere, + -- or applying a sorry to further arguments, is not enough. + unless isBareSorry st.value do + errors := errors.push m!"{s.name}: the statement is proved; its proof must be sorry" + continue + let some d := env.find? name + | errors := errors.push m!"{name}: no library declaration"; continue + unless d matches .thmInfo _ do + errors := errors.push m!"{name}: the library declaration is not a theorem" + continue + unless s.levelParams.length == d.levelParams.length do + errors := errors.push m!"{name}: {s.levelParams.length} universe parameters in the \ + statement, {d.levelParams.length} in the library" + continue + let sType := s.type.instantiateLevelParams s.levelParams (d.levelParams.map Level.param) + unless sType == d.type do + errors := errors.push m!"{name}: the statement differs from the library\n \ + statement: {sType}\n library: {d.type}" + continue + let axioms ← collectAxioms name + let bad := axioms.filter (fun a => !specAllowedAxioms.contains a) + unless bad.isEmpty do + errors := errors.push m!"{name}: the library proof uses {bad}" + continue + logInfo m!"SPEC OK {name}" + unless errors.isEmpty do + throwError m!"statement check failed:\n{MessageData.joinSep errors.toList "\n"}" + logInfo m!"{statements.size} statements match the library" + +#check_statements diff --git a/spec/Spec.lean b/spec/Spec.lean new file mode 100644 index 0000000..0ec6505 --- /dev/null +++ b/spec/Spec.lean @@ -0,0 +1,149 @@ +/- +Copyright (c) 2026 Nelson Spence. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Nelson Spence +-/ +import CdFormal + +/-! +# Statement files for the headline results + +Each declaration below restates one headline result of the library with its statement written +out in full and its proof replaced by `sorry`. The `sorry` is deliberate: this file is the +specification, not the proof. `spec/Check.lean` compares the type of every statement here with +the type of the library declaration of the same name (alpha-equivalence after instantiating the +universe parameters), confirms that the library declaration is a theorem with a proof term, and +walks its axioms. CI runs that comparison, so a reader can check a headline claim against this +file alone, and a change to a library statement that is not mirrored here fails CI. + +This library is not a default target, is never imported by `CdFormal`, and lies outside the +placeholder audit, which covers the `CdFormal` tree only. + +## The named gap `gap:pde-infra` + +`SemioticBVP.exists_isWeakCoherentConfiguration` and +`SemioticBVP.exists_pos_isWeakCoherentConfiguration` take the class `PDEInfra` and the +structures `SolutionOperator` and `PrincipalEigendata` as hypotheses. Their fields are +propositions that no file instantiates, and `#print axioms` cannot see them. The statements +below show those hypotheses in full; the two theorems are implications, and the obligation to +discharge their hypotheses for a concrete operator is the gap named `gap:pde-infra` in +docs/explanation/axiom-boundary.md and docs/reference/verification-audit.md. +-/ + +-- The proofs below are `sorry` by design, so every hypothesis is unused. +set_option linter.unusedVariables false + +noncomputable section + +open scoped Manifold Bundle + +namespace Spec + +section Continuum + +variable {n : ℕ} {M : Type*} + [TopologicalSpace M] + [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] + [IsManifold (SemioticModel n) ⊤ M] + [MetricSpace M] [CompactSpace M] [ConnectedSpace M] + [SemioticManifold n M] + +/-- Statement of `SemioticBVP.exists_isWeakCoherentConfiguration` (paper Theorem 3.12). + Conditional: `gap:pde-infra`. -/ +theorem SemioticBVP.exists_isWeakCoherentConfiguration + (bvp : SemioticBVP n M) + (solOp : SolutionOperator bvp) + [infra : PDEInfra bvp solOp] + (B : ℝ) (hB : ∀ x, bvp.ctx.b x ≤ B) : + ∃ Phi : M → ℝ, + IsWeakCoherentConfiguration bvp Phi ∧ + (∀ x, Phi x ≥ 0) := sorry + +/-- Statement of `SemioticBVP.exists_pos_isWeakCoherentConfiguration` (paper Theorem 3.16). + Conditional: `gap:pde-infra`. -/ +theorem SemioticBVP.exists_pos_isWeakCoherentConfiguration + (bvp : SemioticBVP n M) + (solOp : SolutionOperator bvp) + [infra : PDEInfra bvp solOp] + (beta : ℝ) + (eig : PrincipalEigendata bvp beta) + (eigval_neg : eig.eigval < 0) : + ∃ Phi : M → ℝ, + IsWeakCoherentConfiguration bvp Phi ∧ + (∀ x, Phi x ≥ 0) ∧ + (∃ x, x ∉ bvp.boundary ∧ Phi x > 0) := sorry + +/-- Statement of `scaling_uniqueness`: no solution has a solution multiple kΦ with k > 1 at a + point where c > 0 and Φ > 0. Unconditional. -/ +theorem scaling_uniqueness + (ops : SemioticOperators n M) + (ctx : SemioticContext n M) + (Φ : M → ℝ) (k : ℝ) + (hk : k > 1) + (hΦ_eq : ∀ x, -(ops.laplacian Φ x) = + (ctx.a x) * (ops.gradNorm Φ x) + (ctx.b x) * (Φ x) - + (ctx.c x) * (max (Φ x) 0) ^ ctx.p) + (hkΦ_eq : ∀ x, + -(ops.laplacian (fun y ↦ k * Φ y) x) = + (ctx.a x) * (ops.gradNorm (fun y ↦ k * Φ y) x) + + (ctx.b x) * (k * Φ x) - + (ctx.c x) * (max (k * Φ x) 0) ^ ctx.p) + (x₀ : M) (hc : ctx.c x₀ > 0) (hΦpos : Φ x₀ > 0) : + False := sorry + +end Continuum + +/-- Statement of `spectral_characterization_1d`: for b > 0, β above the threshold + (π/L)²/b gives (π/L)² − βb < 0. Arithmetic; the eigenvalue identification is classical. -/ +theorem spectral_characterization_1d + (L : ℝ) (b : ℝ) (beta : ℝ) (hb : b > 0) : + let beta_star := viabilityThreshold L b + beta > beta_star → (Real.pi / L) ^ 2 - beta * b < 0 := sorry + +/-- Statement of `linfty_bound_algebraic`: from b·v ≥ c·v^p, v ≤ (b/c)^{1/(p−1)}. -/ +theorem linfty_bound_algebraic + (v b c p : ℝ) (hv : v > 0) (hc : c > 0) (hp : p > 1) + (h : b * v ≥ c * v ^ p) : + v ≤ (b / c) ^ (1 / (p - 1)) := sorry + +section Order + +universe u + +variable {α : Type u} [CompleteLattice α] (f : α →o α) + +/-- Statement of `monotone_fixed_point_between`: a monotone self-map of a complete lattice has a + fixed point between an ordered sub-fixed point and super-fixed point. -/ +theorem monotone_fixed_point_between + {sub super : α} + (h_sub : sub ≤ f sub) + (h_super : f super ≤ super) + (h_le : sub ≤ super) : + ∃ x : α, f x = x ∧ sub ≤ x ∧ x ≤ super := sorry + +end Order + +section Graph + +variable {V : Type*} [Fintype V] (G : SemioticGraph V) + +/-- Statement of `SemioticGraph.exists_pos_graph` (paper Theorem 3.23): connected interior, + the edge condition and a negative principal eigenvalue give a solution positive at every + interior vertex. Unconditional. -/ +theorem SemioticGraph.exists_pos_graph (hconn : G.interiorGraph.Connected) + (hdom : ∀ x y, x ∉ G.boundary → y ∉ G.boundary → x ≠ y → 0 < G.w x y → + G.a x ≤ √(G.w x y)) + (hneg : G.principalEigenvalue < 0) : + ∃ u : V → ℝ, G.IsSolution u ∧ ∀ x, x ∉ G.boundary → 0 < u x := sorry + +/-- Statement of `SemioticGraph.exists_pos_graph_of_unweighted`: with 0/1 weights the edge + condition is automatic. Unconditional. -/ +theorem SemioticGraph.exists_pos_graph_of_unweighted (hw : ∀ x y, G.w x y = 0 ∨ G.w x y = 1) + (hconn : G.interiorGraph.Connected) (hneg : G.principalEigenvalue < 0) : + ∃ u : V → ℝ, G.IsSolution u ∧ ∀ x, x ∉ G.boundary → 0 < u x := sorry + +end Graph + +end Spec + +end