test: replay atlas evidence from pinned historical root

tests/fixtures/atlas_formal_build_3b39/README.md.txt

@@ -0,0 +1,144 @@
+# Formal package: SIDE24 arithmetic skeleton (Lean 4, core only)
+
+Scientific effect: **NONE**. This directory is the second package in the
+repository's formal-verification lane. The lane's contract is the
+[formal-verification guide](../docs/FORMAL_VERIFICATION.md); new work is claimed in
+the relevant current pull request or work discussion under the
+[current workflow](../governance/OP-WORKFLOW-20260930.md).
+Closed [work item #95](https://github.com/d6g8k5htny-coder/main/issues/95) is the
+historical formal-ladder work item; the first package is the
+[Math- pilot](https://github.com/d6g8k5htny-coder/Math-/tree/cc2989c1280f4f227d0c6aa30c8841d6ba01e46e/formal)
+(13 GP-FOR-192 scalar companions, Lean 4 + Mathlib). This package follows the same
+manifest, status, gate and alignment contract and adds nothing to the
+scientific-status vocabulary.
+
+What it covers: the exact integer and rational identities and inequalities that
+sections 1–4 of the [SIDE24 coefficient note](sources/side24_v1/PROOF.md)
+(`Math-@9d7b6802…`, SHA-256 `c06dacc…`) rely on — 31 theorems, stated in core
+Lean as cross-multiplied integer facts and proved by `decide`. What it does not
+cover is listed target by target in [SCOPE.md](SCOPE.md): not the coefficient
+bound `0.07340691930603427103 < c_{2,24} < 0.07340691930603427104`, not the
+definition of the coefficient, not any Gaussian, Kac–Rice, cone-integral,
+Stirling or interval-arithmetic step, not `coefficient.py`. Relative to the
+guide's historical work-offer table this is the **first step only** of the "Numerical
+formalizer" offer; the exact coefficient definition and the proof-producing
+enclosure pipeline are not supplied.
+
+## Layout
+
+| Path | Role |
+|---|---|
+| `lean-toolchain`, `lakefile.toml`, `lake-manifest.json` | Pinned toolchain `leanprover/lean4:v4.34.1`; Lake package `UniversalLaw` with **no** dependencies (`dependency_revisions` is empty and the gate checks the lock agrees) |
+| `UniversalLaw.lean` | Root module; imports exactly the three registered modules |
+| `UniversalLaw/Side24/Ledger.lean` | 17 targets: pairing count, image constant, `60E < 10^-108`, Taylor partial sum of `exp(288/125)`, odd-block minors, section-4 exponent bounds, density-comparison order of magnitude |
+| `UniversalLaw/Side24/ConeMoments.lean` | 10 targets: conditional variances, transverse covariance thirds, `D_1 = 4/3`, `D_2 = 29/6 − √6` algebra, cube-root simplification, Hessian block eigenvalues |
+| `UniversalLaw/Side24/Endpoints.lean` | 4 targets: the published 20-digit endpoints as integers — adjacency, ordering, magnitude. **Not an enclosure of the coefficient.** |
+| `sources/side24_v1/` | Byte copies of the two pinned Layer 0 sources (`PROOF.md`, `ENCLOSURE.json`) |
+| `manifest.json` | Evidence sidecar: package identity, toolchain, allowed axioms, SHA-256 of every bound file, pinned sources, 31 targets with verbatim informal anchors and `does_not_claim`, executable negative controls |
+| `SCOPE.md` | Exact coverage and "not established" per target; the review contract |
+| `ALIGNMENT.md` | Generated from the manifest (`--write-alignment`); never hand-edited |
+| `GLOSSARY.md` | Descriptive mapping of project terms to standard objects and Lean availability |
+| `REVIEW_LANE.md`, `reviews/` | Independent statement-alignment review procedure, JSON record template, validator |
+
+## Status vocabulary (same as the Math- lane)
+
+- `formalization_status` in `manifest.json` is **`proved`**: proof text is
+  supplied and bound by hash. The manifest cannot say `kernel-checked`; the gate
+  refuses a manifest that self-awards execution.
+- **`kernel-checked`** appears only in the receipt written by a trusted
+  `--run-lean` execution (`formal/.lake/formal-evidence/receipt.json`), which
+  records the checked Git commit, Lean version, manifest digest, per-target
+  transitive axioms (all `[]` here), log hashes, and negative-control outcomes.
+  A receipt supplied by a caller is untrusted until matched to the actual
+  workflow run and commit.
+- `alignment_status` is **`PENDING_INDEPENDENT_REVIEW`**. The author is
+  Anthropic / Claude via a Cursor cloud agent (2026-09-27); an alignment record
+  from the same provider, family or agent is refused by the validator. The
+  manifest cannot say `ACCEPTED`.
+- In the ladder of [#95](https://github.com/d6g8k5htny-coder/main/issues/95)
+  (L0 prose … L5 proof-assistant-checked, `verification_level` separate from
+  scientific status) a target with a trusted `kernel-checked` receipt is L5
+  evidence for exactly that target.
+- None of these labels is a Layer 0 ACCEPT/AMEND verdict or moves one.
+
+## Run it
+
+Toolchain (once, ~200 MB, no Mathlib cache needed):
+
+```sh
+curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
+export PATH="$HOME/.elan/bin:$PATH"
+```
+
+From the repository root:
+
+```sh
+python3 tools/formal_gate_check.py               # source-only: hashes, inventory, anchors, no Lean run
+python3 tools/formal_gate_check.py --run-lean    # fresh build, leanchecker, axiom audit, controls, receipt
+python3 -B -S -m unittest tests.test_formal_gate -v
+```
+
+The source-only gate prints `SOURCE_IDENTITY_PASS (not a Lean build or
+scientific acceptance): <manifest digest>`. `--run-lean` removes `.lake/build`,
+runs `lake build`, `leanchecker` on every module, a transitive `#print axioms`
+audit restricted to `propext` / `Classical.choice` / `Quot.sound`, an
+elaborated-type capture, and the executable negative controls: seven
+tightened-or-wrong statements written into a scratch copy of the Lean text
+(each must be rejected by Lean), plus `sorry`, an indirectly imported custom
+axiom, and `native_decide` (each must be rejected by the axiom gate). It then
+re-runs the source check to confirm the manifest digest did not move, and only
+then writes the receipt. Locally the whole run takes about five seconds.
+
+Maintenance (these write): `--refresh-hashes` after editing any bound file,
+then `--write-alignment` after editing targets, then the gate again.
+
+The gate fails closed on: hash mismatch; an unregistered `.lean` file or any
+unbound file inside `formal/`; a bound file that does not exist; a control or
+scope file missing from the bound set; toolchain or dependency-lock drift;
+`sorry`, `native_decide` or an `axiom` declaration outside comments; a root
+module that imports anything but the registered modules; a target inventory
+that differs from the theorem names actually declared (in module order); a
+pinned source whose local bytes changed or whose repository is not one of the
+project's public repositories; an anchor that is not a verbatim substring; a
+missing `does_not_claim`; a stale `ALIGNMENT.md`; a manifest with duplicate JSON
+keys.
+
+## Why core Lean and not Mathlib here
+
+Everything the arithmetic skeleton needs is `Nat`/`Int` and `decide`, which the
+kernel evaluates with GMP-backed literals in well under a second. That keeps
+this package's CI cost at seconds with no multi-gigabyte cache. The Math- pilot
+already carries the Mathlib dependency (revision
+`d13f23b723b8a846827a245b89c10fc7d3f11612`, same Lean `v4.34.1`); any statement
+here that needs `ℝ`, `Real.Gamma`, `Real.exp`, `Real.pi`, Gaussian measures or
+matrices — the coefficient definition `c_{d,ref}`, the enclosure itself, the
+P15 constant `ρ*` — belongs in that Mathlib lane, not in a second dependency
+tree. See the rollout record for the coordination items.
+
+## Coordination
+
+Find current tasks in [main #275](https://github.com/d6g8k5htny-coder/main/issues/275) and coordinate with
+other contributors on [main #307](https://github.com/d6g8k5htny-coder/main/issues/307).
+The pickup itself belongs in the relevant current pull request or work discussion.
+
+- [docs/FORMAL_VERIFICATION.md](../docs/FORMAL_VERIFICATION.md) — lane contract
+  and the historical work-offer table, not current assignments.
+- [docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md](../docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md)
+  — what this package adds, how it converged onto the Math- contract, what is
+  asked of other repositories and agents, and this session's capability limits.
+  This dated record preserves the original rollout; its pickup routing is
+  superseded by the current workflow linked below.
+- [Work item #95](https://github.com/d6g8k5htny-coder/main/issues/95) — historical
+  formal-ladder work item. Record actual pickup of alignment review or of the remaining
+  "Numerical formalizer" steps in the relevant current pull request or work
+  discussion under the [current workflow](../governance/OP-WORKFLOW-20260930.md).
+
+## What this package does not do
+
+It does not change `STATUS.md`, `PROOF_INDEX.md`, `LANDING_CLAIMS` or any
+ACCEPT/AMEND outcome. It does not turn a hash match, a green build or a
+kernel-checked lemma into acceptance of the theorem built on it. It does not
+verify `coefficient.py`. It does not make AI-authored Lean text independent;
+the author label stays until a distinct reviewer's record validates. It is not
+a second scientific-status database and adds no status vocabulary beyond the
+lane's.

tests/fixtures/atlas_formal_build_3b39/REVIEW_LANE.md.txt

@@ -0,0 +1,94 @@
+# Independent statement-alignment review (this package)
+
+The Lean kernel checks that a proof establishes its statement. It cannot check
+that the statement is the one the informal text makes. That is an independent
+review task with its own lane, distinct from Layer 0 analytic review and from
+the author-side act of writing the Lean text. The contract is the lane's
+([formal-verification guide](../docs/FORMAL_VERIFICATION.md), "Gate and trust
+boundary") and is restated for this package in
+[SCOPE.md § Review contract](SCOPE.md#review-contract).
+
+## Who may review
+
+Anyone whose provider, family **and** agent all differ from the author's
+(`Anthropic` / `Claude` / Cursor cloud agent, 2026-09-27). The validator refuses
+a record where any of the three coincides, case-insensitively. Same-provider
+reviewers earn zero organizational-independence credit whatever they write;
+this is the repository's existing rule and it applies to Lean text as to prose.
+
+## What the reviewer does
+
+Read the exact current head first; a changed source, scope, toolchain or
+manifest stales any earlier record. Then, for each of the 31 targets in
+`manifest.json`:
+
+1. Locate the `informal_anchor` in the pinned local source copy under
+   `sources/side24_v1/` and read its context.
+2. Read the Lean **statement** (not the proof) and its docstring. Decide
+   whether it is the informal statement at the scope stated in `SCOPE.md`:
+   same constants, same quantifiers, same direction of inequality, same
+   scaling. Most targets are cross-multiplied integer forms of rational
+   identities; check the cross-multiplication.
+3. Read `does_not_claim` and the "Not established" column of `SCOPE.md`.
+   Confirm the Lean statement does not silently claim more than the anchor and
+   that what it omits is named.
+4. Record a per-target verdict: `ALIGNED`, `ALIGNED AT NARROWER SCOPE` (say
+   what is narrower) or `MISALIGNED` (say exactly how). Do not grade the proof
+   (the kernel did) and do not grade the Layer 0 mathematics (different lane).
+
+The reviewer need not run Lean, but should quote the gate output at the
+reviewed commit (`SOURCE_IDENTITY_PASS … <manifest digest>` and, if available,
+the workflow run that produced the receipt).
+
+## What the reviewer records
+
+Two files under `reviews/`, named `<date>_<reviewer-slug>.md` and `.json`:
+
+- **Markdown**: reviewer identity and provider; **source exposure** (whether the
+  Lean proof text or docstrings were read before forming a view of each
+  statement — reading the proof first is the weakest form and must be stated);
+  the reviewed commit, manifest digest and scope digest; one row per target
+  with the verdict.
+- **JSON**: copy [`reviews/TEMPLATE_alignment_review.json`](reviews/TEMPLATE_alignment_review.json)
+  and fill it in. `disposition` is `ACCEPTED` only if **every** target is
+  `ALIGNED` or `ALIGNED AT NARROWER SCOPE` with the narrowing recorded;
+  otherwise leave the record unaccepted — the validator refuses it, which is
+  the intended outcome. `manifest_sha256` is the SHA-256 of
+  `formal/manifest.json` at the reviewed commit; `scope_sha256` is the hash of
+  `formal/SCOPE.md` recorded in the manifest's `files`. `targets` is exactly
+  the 31 manifest target names. `evidence` points to the committed Markdown
+  record by repository, 40-character commit, path and SHA-256.
+
+Validate: `python3 tools/formal_gate_check.py --alignment formal/reviews/<file>.json`.
+The validator checks structure, digests, coverage and lineage independence. It
+does not authenticate that the review happened; a controller has to retrieve
+the referenced evidence at the referenced commit.
+
+A `MISALIGNED` verdict is corrected at the source: fix the Lean statement (new
+hash, new `--run-lean` receipt) or fix the anchor, then re-review.
+
+## What this lane cannot do
+
+- Promote a Layer 0 status. `STATUS.md` and `PROOF_INDEX.md` move only through
+  their own source-bound review.
+- Make an author-side proof independent by relabelling; independence is
+  recorded from the reviewer's actual identity and lineage.
+- Substitute for formalising the analytic content. An aligned arithmetic lemma
+  remains an arithmetic lemma.
+- Flip `alignment_status` in `manifest.json`. That field stays
+  `PENDING_INDEPENDENT_REVIEW`; the accepted record is the evidence, and a
+  controller consumes it.
+
+## Current state
+
+All 31 targets: authored by Anthropic / Claude via a Cursor cloud agent on
+2026-09-27; `proved` at source; `kernel-checked` only in the receipt of a
+trusted run; alignment `PENDING_INDEPENDENT_REVIEW`. No record other than the
+template exists. Record actual pickup in the relevant current pull request or work
+discussion under the [current workflow](../governance/OP-WORKFLOW-20260930.md) so two
+reviewers do not duplicate the work. Find current tasks in
+[main #275](https://github.com/d6g8k5htny-coder/main/issues/275) and coordinate with other contributors on
+[main #307](https://github.com/d6g8k5htny-coder/main/issues/307).
+Closed
+[work item #95](https://github.com/d6g8k5htny-coder/main/issues/95) remains the
+historical formal-ladder work item.