Phase 0 follow-up: status surfaces agree with the spec on O1-carrier (trope-checker)

AFFIRMATION.adoc

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = AFFIRMATION — trope-checker
-:revdate: 2026-10-27
+:revdate: 2026-11-04
 
 A dated, ground-truthed honesty snapshot (the README/EXPLAINME/AFFIRMATION trio).
 This is the brief's "STATUS" deliverable: what is proved, what is stubbed-and-named,
@@ -139,3 +139,35 @@ should transfer, but that is an argument, not a proof — recorded in PROOF-STAT
 and left for the owner where `spec/calculus.adoc §6/§10` cite it as ratified-carrier.
 
 — Run by the Phase 0 agent; the owner signs on landing.
+
+== As of 2026-11-04 — status surfaces reconciled with `main` after #107
+
+*Anchor.* `main` at `4ecba4f` (Phase 0 landed through #107 `190cc75` on 2026-10-31,
+then #109 decoder fixes, #110, #111), read in an Ubuntu cloud container with rustc
+1.97.0 and no Agda, Idris 2 or Lean toolchain reachable.
+
+*Ground truth (commands run here):*
+
+* `cargo build --release` in `src/rust` → `tropecheck-rs` builds;
+  `TROPECHECK_BIN=src/rust/target/release/tropecheck-rs bash tests/conformance/run.sh` → "conformance: all pass".
+* `grep` over `verification/proofs/lean4/grade-boundary/EffectAtomsRatified.lean` →
+  `theorem atom_factorization (g : GradeR)` with its own `#print axioms` line and no
+  `sorry`; the module is in `lakefile.toml`'s default targets and in the
+  `proofs.yml` `lean-build` module list.
+* Agda, Idris2 and Lean → *NOT RUN here*; the `proofs.yml` run on `main` at
+  `4ecba4f` is the attestation:
+  https://github.com/hyperpolymath/trope-checker/actions/runs/41519571355
+  (Agda Theorem B, both Lean packages with `leanchecker` and the axiom audit, and
+  the comment-aware honesty gate — all green).
+
+*What changed in the record.* Finding (4) of the 2026-10-27 entry is superseded:
+the `GradeR` restatement of the atom factorisation exists and is checked
+(`EffectAtomsRatified.lean`, `GradeR.atom_factorization`), as `spec/calculus.adoc
+§3.5` and `§10` already said on `main`; `docs/status/PROOF-STATUS.adoc` and
+`docs/status/ROADMAP.adoc`, which still called the port open, now agree with the
+spec. The 2026-10-27 entry's note on lean-action's `nanoda` step is history:
+`proofs.yml` no longer uses it (#104 closed). Nothing else in this entry re-asserts a
+result the 2026-10-27 entry stated; where a toolchain was not run here, the run cited
+above is the only evidence claimed.
+
+— Run by the Phase 0 agent; the owner signs on landing.

CHANGELOG.adoc

@@ -10,6 +10,14 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 ==== Changed
 
+* *Status surfaces reconciled with the spec on O1-carrier (2026-11-04).*
+`+docs/status/PROOF-STATUS.adoc+`, `+docs/status/ROADMAP.adoc+` and the README status
+paragraph now say what
+`+spec/calculus.adoc §3.5+`/`+§10+` already said: the atom factorisation is proved
+on the ratified `+GradeR+` (`+EffectAtomsRatified.lean+`), the nine-family
+classification is carrier-independent, and `+EffectAtoms.lean+` is history; the
+"port to `+GradeR+` is open" bullet is gone. `+AFFIRMATION.adoc+` gains a 2026-11-04
+entry superseding finding (4) of the 2026-10-27 entry.
 * *Spec v0.2 consolidation (2026-10-13).* `+docs(spec)+`: consolidate the calculus
 at v0.2 — nine effects with the atom table, ratified carrier inline (A1–A3), L6
 commutativity and the cancellation structure as laws, the tropical factorisation

README.adoc

@@ -149,8 +149,8 @@ claimed lemmas (the Lean results rest on the standard library's `propext`/`Quot.
 and `Classical.choice` in three theorems). On the ratified carrier (ADR 0004, R-2026-07-07) the grade algebra is a commutative
 monoid with the three deceptive bottoms as two-sided zeros; L1–L6, conicality, the
 cancellation boundary (left-cancellative iff ε), the Honest Generation and
-Veridicality theorems, the atom factorisation (O1's carrier half — stated on the v0.1 `Grade`,
-not yet restated on `GradeR`) and the tropical factorisations — pre-ratification
+Veridicality theorems, the atom factorisation (O1's carrier half, proved on the ratified `GradeR` in
+`EffectAtomsRatified.lean`; O1-coord stays open) and the tropical factorisations — pre-ratification
 `GradeFactorisation.lean` veridicality-blind, ratified `GradeFactorisationR.lean`
 veridicality-sighted — are proved across Agda, Idris2 and Lean; Theorem B gives
 grade-exact substitution and β/let subject reduction. The

docs/status/PROOF-STATUS.adoc

@@ -1,7 +1,7 @@
 // SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = Proof status — trope-checker
-:revdate: 2026-10-27
+:revdate: 2026-11-04
 :toc: macro
 :stem: latexmath
 
@@ -88,8 +88,8 @@ toc::[]
 3+^| _Factorisation_
 
 | O1-carrier (atom factorisation)
-| Every grade is the stem:[\triangleright]-product of its single-slot projections; nine atom families, each realised, pairwise disjoint. Stated on the v0.1 `Grade` (`EffectAtoms.lean` imports `GradeBoundary`): the construction is componentwise and does not touch the clause (A1) changed, but a restatement on `GradeR` is not mechanised (see Open).
-| Lean `EffectAtoms.lean`: `Trope.Grade.atom_factorization`, `Trope.nine_families`, `Trope.family_realized`, `Trope.families_disjoint`, `fateFamily_none_iff`.
+| Every grade is the stem:[\triangleright]-product of its single-slot projections; nine atom families, each realised, pairwise disjoint. Proved on the ratified `GradeR` (`EffectAtomsRatified.lean`); the coordinate-value classification into nine families (`EffectAtoms.lean`) is carrier-independent and carries over unchanged. `EffectAtoms.lean`'s `Grade.atom_factorization` is the same statement over the historical pre-ratification carrier, retained as history (`spec/calculus.adoc §3.5`, `§10`).
+| Lean `EffectAtomsRatified.lean`: `Trope.GradeR.atom_factorization` (its `#print axioms` and the CI axiom audit: no `sorryAx`, no user axiom); `EffectAtoms.lean`: `Trope.nine_families`, `Trope.family_realized`, `Trope.families_disjoint`, `fateFamily_none_iff`.
 
 | Tropical factorisation, (B′) sighted
 | A nontrivial surjective monoid homomorphism stem:[\pi_R] onto the commutative tropical fidelity carrier exists and distinguishes `Dropped` (stem:[\infty]) from `Falsified` (stem:[\top]); the verbatim-payload map is not a homomorphism, and any sighted homomorphism squashes `Unknown` to the deceptive top.
@@ -144,11 +144,6 @@ Each is specified; none is asserted. Status words follow `spec/calculus.adoc §1
   its mechanisation in Agda, steps 1–5 of that note's §6 extending `TB.Reduction`,
   is OPEN. It closes Theorem B Target 3 (`fix`, NOT-REACHED, no postulate) and
   grade soundness for conservative lowering (`spec/calculus.adoc §7–§8`).
-* *O1-carrier on `GradeR`* — `atom_factorization` and the nine-family results
-  (`EffectAtoms.lean`) are theorems about the v0.1 `Grade`; porting them to the
-  ratified `GradeR` — expected to be mechanical, the factorisation being
-  componentwise — is OPEN. Until then the ratified-carrier reading in
-  `spec/calculus.adoc §6` and `§10` rests on that transfer argument, not a proof.
 * *O1-coord* — whether `fate`, `bond`, `merge` are exhaustive ways to
   individuate-and-lose; live probe: the bond-transfer move (`spec/calculus.adoc
   §10`; workbench WP-5).

docs/status/ROADMAP.adoc

@@ -26,8 +26,9 @@ what is open: `docs/status/PROOF-STATUS.adoc`, `AFFIRMATION.adoc`,
   Targets 1, 2, 4 proved; Target 3 β/let proved.
 * [x] L4 monotonicity in full, both arguments, every coordinate (Idris2, Lean, Agda); L6
   commutativity.
-* [x] Atom factorisation — O1-carrier proved on the historical `GradeBoundary`
-  carrier (`EffectAtoms.lean`): nine atom families. Restatement on ratified `GradeR` remains open.
+* [x] Atom factorisation — O1-carrier proved on the ratified `GradeR`
+  (`EffectAtomsRatified.lean`); the nine-family classification (`EffectAtoms.lean`)
+  is carrier-independent. O1-coord stays open.
 * [x] Tier-2 cancellation membership exhaustive (`TierTwoComplete.lean`).
 * [x] Tropical factorisation re-run on the ratified carrier: (B′) factors and
   veridicality-sighted (`GradeFactorisationR.lean`).