Add Layer 1 formal verification: Lean 4 SIDE24 arithmetic pilot, formalization registry, fail-closed gate, review lane

.github/workflows/formal-verification.yml

@@ -0,0 +1,70 @@
+# Layer 1 formal lane. Builds the dependency-free Lean 4 library, audits axioms,
+# and runs the fail-closed formalization gate. A green run establishes that the
+# registered declarations are kernel-checked with allowed axioms only and that
+# the registry, hashes and informal anchors are consistent. It is NOT
+# mathematical acceptance of any Layer 0 claim; see formal/README.md.
+name: formal-verification
+on:
+  pull_request:
+    paths:
+      - 'formal/**'
+      - 'tools/formal_gate_check.py'
+      - 'tests/test_formal_gate.py'
+      - '.github/workflows/formal-verification.yml'
+  push:
+    branches: [main]
+    paths:
+      - 'formal/**'
+      - 'tools/formal_gate_check.py'
+      - 'tests/test_formal_gate.py'
+      - '.github/workflows/formal-verification.yml'
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  kernel-check:
+    name: kernel-check
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
+        with:
+          python-version: '3.11'
+      - name: Install elan (pinned release script, digest checked) and the pinned toolchain
+        run: |
+          set -euo pipefail
+          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/v4.2.4/elan-init.sh -o /tmp/elan-init.sh
+          echo 'a620ff1641616222c8d37c54845492004bb84d6877cdbc944dd65c1aa685bf53  /tmp/elan-init.sh' | sha256sum -c -
+          sh /tmp/elan-init.sh -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+          "$HOME/.elan/bin/elan" toolchain install "$(cat formal/lean-toolchain)"
+      - name: Record toolchain
+        run: |
+          mkdir -p formal-evidence
+          git rev-parse HEAD > formal-evidence/commit.txt
+          (cd formal && lean --version && lake --version) | tee formal-evidence/toolchain.txt
+      - name: Build the Lean library (kernel check)
+        run: cd formal && lake build 2>&1 | tee ../formal-evidence/lake-build.log
+      - name: Axiom audit
+        run: cd formal && lake env lean UniversalLaw/Audit.lean | tee ../formal-evidence/axioms.txt
+      - name: Fail-closed formalization gate
+        run: python -B -S tools/formal_gate_check.py --axioms-output formal-evidence/axioms.txt | tee formal-evidence/gate.json
+      - name: Gate controls, including Lean mutants, in both interpreter modes
+        run: |
+          python -B -S -m unittest tests.test_formal_gate -v 2>&1 | tee formal-evidence/tests-normal.log
+          python -B -O -S -m unittest tests.test_formal_gate -v 2>&1 | tee formal-evidence/tests-optimized.log
+      - name: Describe coverage
+        if: always()
+        run: |
+          echo 'Kernel-checked the registered Lean declarations, audited their axioms, and verified registry hashes and informal anchors. This is formalization status only: no Layer 0 review outcome, STATUS row, or theorem acceptance was established or changed.' >> "$GITHUB_STEP_SUMMARY"
+      - name: Preserve actual results including failures
+        if: always()
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a
+        with:
+          name: formal-verification-${{ github.run_id }}
+          path: formal-evidence
+          if-no-files-found: error
+          retention-days: 30

.gitignore

@@ -1,2 +1,3 @@
 __pycache__/
 *.pyc
+.lake/

AGENTS.md

@@ -31,14 +31,28 @@ Drive record, and collaboration surfaces. This `main` initially contains the ren
 landing, not the complete research stack. Bring improvements into it coherently;
 there is no permanent landing-only restriction.
 
-## Formal-verification extension — 27 September 2026
-
-Read the [formal-verification guide](docs/FORMAL_VERIFICATION.md) and coordinate
-through [the existing work item #95](https://github.com/d6g8k5htny-coder/main/issues/95).
-Lean kernel evidence, exact source identity, independent statement alignment and
-scientific acceptance are separate requirements. A build, Blueprint link, hash,
-solver result or merge does not satisfy them all. Reuse the source-pinned Math-
-pilot rather than opening a competing registry. Preserve original proof carriers;
-compiler changes are explicit successors. Review the exact current head and record
-actual author/reviewer lineage. Do not credit an unobserved reviewer or assume that
-a prior source-bound review remains valid after its source or scope changes.
+## Formal verification — two pilots, one vocabulary (27 September 2026)
+
+Layer 0 is the existing provenance, scope and source-bound review system. Layer 1
+is Lean kernel evidence, and two pilots exist because two agents answered the same
+owner instruction on the same day:
+
+- the `Math-` pilot ([PR92](https://github.com/d6g8k5htny-coder/Math-/pull/92),
+  Mathlib, 13 GP-FOR-192 scalar companions) described in the
+  [formal-verification guide](docs/FORMAL_VERIFICATION.md);
+- the `main` pilot in [`formal/`](formal/README.md) (core Lean only, the SIDE24
+  arithmetic skeleton) with one formalization status per claim in
+  [`formal/registry.json`](formal/registry.json) and the
+  [rollout record](docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md).
+
+They cover different mathematics and neither is a scientific-status database. Read
+both records before touching either layer, coordinate through
+[the existing work item #95](https://github.com/d6g8k5htny-coder/main/issues/95),
+and do not open a third registry. Lean kernel evidence, exact source identity,
+independent statement alignment and scientific acceptance are separate requirements:
+a build, Blueprint link, hash, solver result or merge does not satisfy them all, and
+no formalization status ever moves a Layer 0 status. Preserve original proof
+carriers; compiler changes are explicit successors. Review the exact current head
+and record actual author/reviewer lineage. Do not credit an unobserved reviewer or
+assume that a prior source-bound review remains valid after its source or scope
+changes.

CONTRIBUTING.md

@@ -142,6 +142,40 @@ back regardless of how good the result looks.
 - **Python 3.11, standard library only.** `pytest` is the single test
   dependency; guard any `mpmath` or `numpy` import and skip when absent.
 
+## Formal verification (Lean 4, Layer 1)
+
+The [`formal/`](formal/README.md) directory holds Lean 4 statements and proofs
+bound by hash to the exact Layer 0 bytes they formalise, and
+[`formal/registry.json`](formal/registry.json) records one **formalization
+status** per claim: `none`, `specified`, `proved`, or `kernel-checked`. Rules:
+
+- **Register every Lean file and every declaration you want counted.** The gate
+  (`tools/formal_gate_check.py`) refuses unregistered `.lean` files, hash
+  mismatches, `sorry`, `native_decide`, and any `axiom` not listed in
+  `project_axioms` with a scope note. After editing Lean text run
+  `--refresh-hashes`, then `--write-alignment`, then the gate with the kernel lane
+  (`--run-lean` or `--axioms-output`), never only `--static-only`.
+- **`kernel-checked` means allowed axioms only.** `propext`, `Classical.choice`,
+  `Quot.sound` or none. A proof that leans on a project axiom (an unformalised
+  parent theorem stated explicitly with a scope note) is `proved`, not
+  `kernel-checked`, until the parent is formalised.
+- **Every Lean statement carries a verbatim `informal_anchor`** from a
+  byte-pinned local source copy under `formal/sources/`, and a `does_not_claim`.
+  Core Lean has no rationals: state rational identities as cross-multiplied
+  integers and give the rational form in the docstring.
+- **Statement alignment is its own review.** AI- or human-authored Lean text is
+  author-side until a distinct reviewer records, under `formal/reviews/`, that
+  the Lean statement says what the anchor says. Follow
+  [`formal/REVIEW_LANE.md`](formal/REVIEW_LANE.md). Same-provider reviewers earn
+  zero independence credit, as everywhere else in this repository.
+- **Formalization status never moves Layer 0 status.** A `kernel-checked` lemma
+  does not edit `STATUS.md`, `PROOF_INDEX.md` or any ACCEPT/AMEND row, and does
+  not make the surrounding analytic argument verified. Use the vocabulary in
+  [`formal/GLOSSARY.md`](formal/GLOSSARY.md) when writing for external readers.
+- **Mathlib is a separate step.** The pilot is dependency-free on purpose. A
+  Mathlib lane (needed for `ℝ`, `Real.Gamma`, `Real.log`, Gaussian measures)
+  changes CI cost and is proposed in its own PR.
+
 ## Claims and status
 
 - **No status moves by merge.** Commits, tests, receipts and reviews cannot

README.md

@@ -84,6 +84,21 @@ For full proof texts, use **[Public mathematics](docs/PUBLIC_MATHEMATICS.md)**.
 - Numerical or floating-point work is labeled non-certifying when it is not a proof.
 - Independent review is recorded separately from same-author checks.
 - A merge, green CI run, hash match, publication, or model agreement does not promote mathematical status.
+- A kernel-checked Lean lemma verifies exactly its own statement; it does not verify the analytic argument around it or promote a Layer 0 status.
+
+## Verification stack
+
+| Layer | What it checks | Where |
+|---|---|---|
+| **Layer 0 — provenance, scope, review** | Exact bytes (SHA-256, Git blobs), declared scope and "does not claim" statements, source-bound nonauthor review, fail-closed intake and landing gates | [`STATUS.md`](STATUS.md), [Math- proof index](https://github.com/d6g8k5htny-coder/Math-/blob/d6628da09384728992dcbe6e921cc28ba85aebb0/PROOF_INDEX.md), [public inventory](docs/public-math/sources.json), [museum](https://d6g8k5htny-coder.github.io/main/site/museum.html) |
+| **Layer 1 — formal (Lean 4)** | Statements and proofs checked by the Lean kernel, bound by hash to Layer 0 bytes, with a per-claim formalization status (`none` / `specified` / `proved` / `kernel-checked`) and a statement-alignment review lane | [`formal/README.md`](formal/README.md), [`formal/registry.json`](formal/registry.json), [glossary](formal/GLOSSARY.md), [review lane](formal/REVIEW_LANE.md) |
+
+The pilot formalises the arithmetic skeleton of the SIDE24 coefficient note: 31 kernel-checked, axiom-free theorems. The coefficient bound itself and every analytic step remain Layer 0 prose with formalization status `none`. See the [rollout record](docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md) for what changed, why, and what each repository is asked to do next.
+
+```sh
+python3 tools/formal_gate_check.py --run-lean      # needs elan/lake; see formal/README.md
+python3 -B -S -m unittest tests.test_formal_gate -v
+```
 
 ## Research still in progress