fix(container)+docs(proofs): real binary build, per-batch rollback, honest wording; PROOF-STATUS ledger

.machine_readable/descriptiles/STATE.a2ml

@@ -36,9 +36,10 @@ issues = [
 [critical-next-actions]
 actions = [
   "Owner decisions taken 2026-11-05 (docs/ROUTE-PLAN.adoc section 9): compiler route; Agda-first; vcl-ut RECOVER verb; name kept; Zig FFI deleted",
-  "Run the empirical gate E1-E6 before the engine session",
+  "Run the empirical gate E1-E7 before the engine session",
   "Re-target src/verisim.rs to real verisim-api routes",
-  "File the cross-repo issues listed in docs/ROUTE-PLAN.adoc section 12",
+  "Proof ledger PROOF-STATUS.adoc (2026-11-09): R2-R10 and R12/R13 theory halves PROVEN in verisimdb/echo-types/tropical-types; R0, R1, R11, R15, R16 OPEN; R17 ASSUMED",
+  "File the cross-repo issues listed in docs/ROUTE-PLAN.adoc section 10",
 ]
 
 [maintenance-status]

0-AI-MANIFEST.a2ml

@@ -98,7 +98,7 @@ This repo follows the **Dual-Track** architecture:
 ├── src/                        # Source code
 │   └── interface/              # Verified Interface Seams
 │       ├── abi/                # Idris2 ABI (The Spec)
-│       ├── ffi/                # Zig FFI (The Bridge)
+│       ├── ffi/                # Reserved for the FFI bridge (template deleted 2026-11-05; see its README)
 │       └── generated/          # C Headers (The Result)
 ├── container/                  # Stapeln container ecosystem
 ├── docs/                       # Technical depths

EXPLAINME.adoc

@@ -11,7 +11,7 @@ The README makes claims. This file backs them up.
 
 *From README:* "A database recovery and reconstruction tool that uses VeriSimDB's octad model and VCL-total's progressive type system to reassemble damaged, fragmented, or inconsistent datasets through cross-modal constraint propagation... Data that passes all 10 levels is formally verified as recovered."
 
-*Evidence:* The reconstruction engine at `src/engine/` is designed as 5-phase progressive constraint propagation: Phase 1 (Loose Constraints, VCL-total Levels 1-3) accepts anything structurally valid; Phase 2 (Cross-Modal Inference) uses populated modalities to infer missing ones (document text → graph edges via NER, graph edges → semantic annotations); Phase 3 (Conflict Resolution) arbitrates contradictions via provenance chains and temporal versions; Phase 4 (Tightening, VCL-total Levels 4-6) enforces null-safety and injection-proofing; Phase 5 (Convergence, VCL-total Levels 7-10) achieves cardinality bounds and linearity. `src/abi/mod.rs` states the invariants the engine must satisfy, in the form an honest mechanisation can target (lexicographic progress rather than monotone real-valued drift; identity preservation; purity of resolve; the VCL-UT ratchet; well-founded termination). **Caveat (2026-11-04):** this is concept stage. The engine, ingest and VeriSimDB client are stubs; no Idris2 proofs exist in this repository yet; VCL-UT can only certify levels L0–L6 from source today. The route to closing each of these gaps is `docs/ROUTE-PLAN.adoc`.
+*Evidence:* The reconstruction engine at `src/engine/` is designed as 5-phase progressive constraint propagation: Phase 1 (Loose Constraints, VCL-total Levels 1-3) accepts anything structurally valid; Phase 2 (Cross-Modal Inference) uses populated modalities to infer missing ones (document text → graph edges via NER, graph edges → semantic annotations); Phase 3 (Conflict Resolution) arbitrates contradictions via provenance chains and temporal versions; Phase 4 (Tightening, VCL-total Levels 4-6) enforces null-safety and injection-proofing; Phase 5 (Convergence) aims at cardinality bounds and linearity, which VCL-total places at Levels 7-10; the gate ceiling today is L6, so Phase 5 is capped there until vcl-ut certifies higher levels from source. `src/abi/mod.rs` states the invariants the engine must satisfy, in the form an honest mechanisation can target (lexicographic progress rather than monotone real-valued drift; identity preservation; purity of resolve; the VCL-UT ratchet; well-founded termination). **Caveat (2026-11-04):** this is concept stage. The engine, ingest and VeriSimDB client are stubs; no Idris2 proofs exist in this repository yet; VCL-UT can only certify levels L0–L6 from source today. The route to closing each of these gaps is `docs/ROUTE-PLAN.adoc`.
 
 === Claim 2: Eight Independent Representations (Octad Modalities) as Mutual Witnesses for Entity Identity
 

PROOF-NEEDS.adoc

@@ -3,10 +3,19 @@
 === Current State
 
 * *LOC*: ~640 Rust (2026-11-05)
-* *Languages*: Rust; an unbuilt Zig FFI template; no Idris2 source yet
-* *Existing proofs*: none. No `.idr` file exists (the template ABI was removed
-  on 2026-03-29, see below). No proof ledger exists yet; one is required by
-  README-EXPLAINME-STANDARD section 5 before any proof is claimed.
+* *Languages*: Rust only. The unbuilt Zig FFI template was deleted on 2026-11-05 (see `src/interface/ffi/README.adoc`); no Idris2 source yet
+* *Existing proofs*: none in this repository. No `.idr` file exists (the
+  template ABI was removed on 2026-03-29, see below). The proofs that DO
+  exist for squeakwell's invariants live in their estate homes — verisimdb
+  `formal/Recovery.v` (Rocq), echo-types `EchoPartialSection.agda` +
+  `EchoFibreIntersection.agda` (Agda), tropical-types
+  `Resource/HubCeiling.lean` (Lean) — and are ledgered per rung, with
+  receipts, in link:PROOF-STATUS.adoc[PROOF-STATUS.adoc] (2026-11-09).
+  These are *theory* results over abstract carriers. In particular the
+  Lean hub-ceiling lemmas hold for any resource algebra whose unit is top;
+  their application to squeakwell's f64 confidence scores (the quantisation
+  layer onto an ℕ-based `MinPlus` carrier, and the walk semantics of
+  `matStar`) is not proved anywhere and stays OPEN (ledger R6, R7 notes).
 * *Prover homes per standards PROOF-POLICY*: Creusot for the Rust kernel
   behaviour, Idris2 for the program/journal/gate wire contracts, Agda (echo-types)
   as theory source rechecked in Rocq (verisimdb/formal) and Lean (tropical-types).

PROOF-STATUS.adoc

@@ -0,0 +1,192 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= squeakwell — Proof Status (ledger)
+:toc:
+:revdate: 2026-11-09
+
+Requirements: link:PROOF-NEEDS.adoc[PROOF-NEEDS.adoc]. Ladder and repaired
+statements: link:docs/ROUTE-PLAN.adoc[docs/ROUTE-PLAN.adoc] sections 3 and 6.
+Estate rules: standards `3-practice/PROOF-POLICY.adoc`. Mathesis register:
+`mathesis/docs/status/CROSS-PROVER-RECONCILIATION.adoc`.
+
+[IMPORTANT]
+====
+A row says *PROVEN* or *PROVEN-WITH-AXIOMS* only where the named prover ran
+on the named file in a recorded environment, with the receipt below. Nothing
+in `src/` is covered by any row: the Rust engine is a stub and the Creusot
+and Idris2 homes have no source yet. Grades are per theorem, not per repo.
+====
+
+== Status vocabulary
+
+PROVEN (kernel-checked, no axioms beyond the prover's logic) ·
+PROVEN-WITH-AXIOMS (kernel-checked; the axioms are listed) · TESTED (runnable
+check, not a proof) · ASSUMED (used as a hypothesis, not discharged) · OPEN.
+
+== Ledger (one row per rung)
+
+[cols="1,4,2,2,3",options="header"]
+|===
+|Rung |Statement (repaired form) |Home |Status |Artefact / receipt
+
+|R0 |Proptest laws for the resolve kernel; fill never overwrites; `mu`
+lex-decreases or fixpoint; a case where conflicts rise after fill |squeakwell
+`tests/` |OPEN |No property harness yet (`TEST-NEEDS.adoc`: fixed-input
+fixtures only).
+
+|R1 |`weaken : SafetyCertificate s sch n -> CanWeakenStar n m ->
+SafetyCertificate s sch m` |vcl-ut Idris2 |OPEN |Not started.
+
+|R2 |Identity persists through every recovery round, for every oracle |Rocq,
+verisimdb `formal/Recovery.v` |PROVEN-WITH-AXIOMS |`step_preserves_id`,
+`iter_preserves_id`. Axioms: none beyond Octad.v's parameters `mval`, `ident`
+(`Print Assumptions` for both lemmas — receipt C1).
+
+|R3 |Guarded fill is inflationary on the information order and NOT monotone
+on it |Agda source: echo-types `EchoPartialSection.agda`; Rocq recheck
+`Recovery.v` |PROVEN (Agda) / PROVEN-WITH-AXIOMS (Rocq) |Agda:
+`fill-guarded`, `fill-inflationary`, `FillNotMonotone.fill-not-monotone`
+(pointwise, funext-free). Rocq: `fill_guarded`, `fill_inflationary`,
+`fill_not_monotone` — all three on `mval`, `ident` only (no
+`functional_extensionality_dep`; the counter-model is decided by `Nat.eqb`
+on concrete octads, so no function equality is needed). Audit modalities by
+chain prefix: verisimdb `Provenance.v`, not re-proved here.
+
+|R4 |Counter-model: filling can raise the conflict count |Rocq `Recovery.v`
+|PROVEN-WITH-AXIOMS |`fill_can_raise_conflicts` (0 → 2 ordered conflicting
+pairs) under hypotheses `conflict a a = false`, `conflict a b = true`. The
+runnable witness in verisim-api `drift_compute.rs` is TESTED-level evidence,
+not a proof.
+
+|R5 |`weightedResidueMeasure w : ResidueMeasure (List M) R` for any resource
+algebra |Lean, tropical-types `Resource/HubCeiling.lean` |PROVEN
+|`weightedResidueMeasure`, `weightedMeasure_append`; `#print axioms`: none.
+Constant-weight instance `weighted_counts_events` (propext, Quot.sound).
+
+|R6 |Element lemma `a ⊠ b ⊑ a` when `one` is top; matrix and star corollaries
+|Lean `HubCeiling.lean` |PROVEN / PROVEN-WITH-AXIOMS |`factor_le`,
+`factor_le_right`, `zero_bot`, `join_bound`, `lsum_bound` (no axioms);
+`single_hub_ceiling`, `single_hub_star_ceiling` (propext, Quot.sound). The
+star corollary holds only under the explicit `IsStar` fixed-point hypothesis
+(no walk semantics for `matStar` in Lean). `OneTop` discharged at MinPlus and
+MinMax; refuted at MaxPlus (`maxplus_not_one_top`).
+
+|R7 |`reachGrade` monotone in the matrix and in the observed set; observed
+node has full grade |Lean `HubCeiling.lean` |PROVEN / PROVEN-WITH-AXIOMS
+|`lsum_filter_mono`, `reachGrade_mono_mat`, `reachGrade_mono_set` (no
+axioms); `one_le_reachGrade` (propext, Quot.sound).
+
+|R8 |Multi-witness narrowing: binary iso, `Fin n` steps, count shrinks |Agda
+echo-types `EchoFibreIntersection.agda` |PROVEN |`fibre-intersection-iso`,
+`forget-left-witness`, `forget-right-witness`, `narrow-fin-step-to/from`,
+`narrow-shrinks`. "Covering masks ⇒ subsingleton" dropped (needs
+extensionality over opaque identifiers).
+
+|R9 |Permutation invariance of the merge fold under a semilattice resolve;
+PUT kernel is a non-instance |Agda `EchoPartialSection.agda` (merge laws);
+Rocq `Recovery.v` (fold) |PROVEN (Agda laws) / PROVEN-WITH-AXIOMS (Rocq fold)
+|Agda: `merge-comm`, `merge-assoc`, `merge-idem` (pointwise, implications
+from `resolve`). Rocq: `fold_merge_perm` (same-identifier batch, commutative
++ associative resolve; uses `functional_extensionality_dep` because `merge_swap`
+rewrites octads as functions), `put_commutative_iff_trivial` (`mval` only).
+
+|R10 |Lexicographic progress and ≤ 9-round termination with explicit
+hypotheses |Rocq `Recovery.v` |PROVEN-WITH-AXIOMS |`step_progress`,
+`iter_bounded`, `iter_9_fixpoint`, `iter_9_no_conflicts`. Hypotheses
+explicit: `conflict_refl`, `winner_some`. Axioms: `step_progress` and
+`iter_9_fixpoint` use `functional_extensionality_dep` (octad-as-function
+equalities); `iter_9_no_conflicts` uses `mval`, `ident` only. Not restated in Agda or Lean (needs
+the finite octad and a conflict test); the ladder said "Agda source, Rocq and
+Lean rechecks" — Rocq is the source for this rung.
+
+|R11 |Purity and permutation invariance of the Rust resolve kernel |squeakwell
+Creusot |OPEN |No Creusot source; toolchain not installed.
+
+|R12 |Observation fidelity at fragment granularity |Agda
+`EchoPartialSection.agda` |PROVEN (theory half) / OPEN (Creusot export
+postcondition) |`restrict-fibre-agree` (`e : Echo (restrict T) obs` agrees
+with `obs` on every observed modality), `restrict-blind`, `restrict-echo`.
+`RepairJustification` on overruled fragments: not started.
+
+|R13 |Review-queue completeness over the enumerated candidate fibre |Agda
+echo-types (`EchoFiberCount`, `EchoTruncation`, `EchoFibreIntersection`)
+|PROVEN (theory half) / OPEN (Creusot queue predicate) |`hits_y ≡ 0 ⇔
+¬Echo`: `FiberSize-fin≡0⇒no-echo`, `no-echo⇒FiberSize-fin≡0` (pre-existing).
+`hits_y ≥ 2 ⇒` two distinct echoes: `echo-not-prop` /
+`preimages⇒distinct-echoes` (`EchoTruncation`, wired 2026-11-09). Narrowing
+cannot grow the queue: `narrow-shrinks`. The engine predicate itself: OPEN.
+
+|R14 |Fibre-blind functionals are constant on the fibre |Agda echo-types
+`EchoEntropy.agda` |PROVEN (pre-existing) |`entropy-blind-parametric`
+(any functional of any fibre-determined distribution is witness-blind);
+confidence ranks fibres, never selects within one.
+
+|R15 |Reintroduction-statement grading ≥ 1 implies every populated field
+resolves |Idris2 wire contract in squeakwell |OPEN |`vclt-gate` v1 behaviour
+is TESTED (live run in the 2026-11 survey); no Idris2 contract yet.
+
+|R16 |Additive `RepairJustification` extension reopens no theorem |vcl-ut
+Idris2 |OPEN |Needs an `idris2 --build`.
+
+|R17 |`nconflicts o = 0 → every computable pairwise drift = 0` |Rocq,
+verisimdb `Drift.v` |ASSUMED |Not stated; `Drift.v` D1/D2 untouched.
+
+|R18 |Enumerated candidate fibre as a Kripke world set (conjecture) |research
+|OPEN |Unstatable until vcl-ut `Epistemic.idr` line 149 is fixed and
+`Believes` is separated from `Knows`.
+|===
+
+== Receipts (2026-11-09, this session's environment)
+
+[cols="1,3,3",options="header"]
+|===
+|Id |Toolchain and command |Result
+
+|C1 |Coq 8.18.0 (Ubuntu 24.04 apt). `cd verisimdb/formal && coqc -q Octad.v
+&& coqc -q Recovery.v > Recovery.out`; whitelist
+`awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Recovery.out \| sort -u`
+|Exit 0 in 1.8 s. Union of assumptions over all twelve `Print Assumptions`
+blocks: `mval`, `ident`, `functional_extensionality_dep` — identical to the
+`Octad.v` whitelist. Per lemma (re-run 2026-11-09 after review): `mval`,
+`ident` only for `fill_guarded`, `fill_inflationary`, `fill_not_monotone`,
+`fill_can_raise_conflicts`, `normalise_no_conflicts`, `step_preserves_id`,
+`iter_preserves_id`, `iter_9_no_conflicts`; `mval` only for
+`put_commutative_iff_trivial`; `mval`, `ident`, `functional_extensionality_dep`
+for `step_progress`, `iter_9_fixpoint`, `fold_merge_perm` (the three that
+rewrite an octad as a function). The nine pre-existing modules also compile
+and pass their Justfile whitelists. PR:
+https://github.com/hyperpolymath/verisimdb/pull/350.
+
+|A1 |Agda 2.7.0.1 (echo-types `scripts/setup-agda.sh`, checksum-pinned),
+agda-stdlib `8326c7475af1fa456ca04a0203c168d5d7ff842b`, absolute-zero
+`f486c29903434589117fa0662c6f29b0f17d1d5f`. `agda --no-libraries -i
+$AGDA_STDLIB -i $ABSOLUTE_ZERO_AGDA --safe --without-K --cubical-compatible
+-i proofs/agda <file>` on `EchoPartialSection.agda`,
+`EchoFibreIntersection.agda`, then `All.agda` and `Smoke.agda`.
+|Both new modules exit 0 (warnings: `UnsupportedIndexedMatch` only, the same
+class the existing suite emits). `All.agda` and `Smoke.agda` exit 0 before the
+wiring; the post-wiring run is recorded in the echo-types PR. Zero postulates;
+`scripts/kernel-guard.sh` PASS.
+
+|L1 |Lean 4.35.0 via elan (`lean-toolchain` pin). `cd tropical-types && lake
+build`; then `lake env lean axcheck.lean` with `#print axioms` on every new
+headline.
+|`Build completed successfully (21 jobs)`. Axioms: none for `factor_le`,
+`factor_le_right`, `zero_bot`, `join_bound`, `lsum_bound`,
+`lsum_filter_mono`, `reachGrade_mono_mat`, `reachGrade_mono_set`,
+`weightedResidueMeasure`, `weightedMeasure_append` (re-checked 2026-11-09);
+`[propext, Quot.sound]` for the others. No
+`sorry`, no `Classical.choice`. PR:
+https://github.com/hyperpolymath/tropical-types/pull/67.
+|===
+
+== What is NOT covered
+
+* Nothing about the Rust in `src/` is proved. The engine is a stub (see
+  `EXPLAINME.adoc`); the Creusot rows (R11, the R12/R13 engineering halves)
+  and the Idris2 rows (R1, R15, R16) are OPEN.
+* The empirical gate E1–E7 in the route plan has not been run.
+* Cross-prover correspondence between the Agda and Rocq statements of R3/R9 is
+  a *refinement* (pointwise vs. function equality under
+  `functional_extensionality_dep`), recorded as BRIDGE-PENDING in the mathesis
+  register until a checked translation exists.

README.adoc

@@ -61,7 +61,7 @@ Damaged data (fragments, corruption, inconsistencies)
   Drift score: ~0.15
         │
         ▼
-  PHASE 5 — CONVERGENCE (VCL-total Levels 7-10)
+  PHASE 5 — CONVERGENCE (gate ceiling L6; VCL-total Levels 7-10 are future vcl-ut work)
   Cardinality bounds, effect tracking, temporal consistency, linearity.
   The reintroduction statements for an entity are gate-admissible at level k
   (ceiling 6 from VCL text; see docs/ROUTE-PLAN.adoc section 4.4).
@@ -116,18 +116,27 @@ function: recovery is complete when cross-modal drift approaches zero.
   - Phase 1: Loose acceptance + schema inference
   - Phase 2: Cross-modal inference (fill missing modalities)
   - Phase 3: Conflict resolution (provenance + temporal + semantic arbitration)
-  - Phase 4: Type tightening (VCL-total levels 4-6)
-  - Phase 5: Convergence (VCL-total levels 7-10)
-
-* **Invariants** (`src/abi/mod.rs`; no proofs exist yet, prover homes per
-  estate PROOF-POLICY are in `docs/ROUTE-PLAN.adoc`) — the engine is designed so that:
+  - Phase 4: Type tightening (VCL-total levels 4-6; gating planned, the stub does not yet invoke `vclt-gate`)
+  - Phase 5: Convergence (no gate level beyond Phase 4's planned L6 ceiling; VCL-total levels 7-10 are future vcl-ut work)
+
+* **Invariants** (`src/abi/mod.rs`) — the engine is designed so that the
+  following hold. No proof lives in this repository and the Rust engine itself
+  is unproved; the *theory* behind rungs R2–R10 (identity preservation through
+  every round, guarded fill inflationary but not monotone, the conflict-raising
+  counter-model, fold permutation invariance, bounded termination, the
+  fibre-intersection and hub-ceiling lemmas) is mechanised in its estate homes
+  and ledgered with prover receipts in link:PROOF-STATUS.adoc[PROOF-STATUS.adoc];
+  the prover homes per estate PROOF-POLICY are in `docs/ROUTE-PLAN.adoc`:
   - Constraint propagation is monotonic (data only gets more consistent)
   - Cross-modal inference preserves entity identity
   - Conflict resolution is deterministic (same input → same output)
   - Type ratchet is sound (passing level N implies passing levels 1..N-1)
 
-* **VCL-UT integration** — Uses the `vclt-gate` binary (hyperpolymath/vcl-ut) as the certifier.
-  Each phase invokes progressively stricter VCL-total levels.
+* **VCL-UT integration** (planned) — The `vclt-gate` binary (hyperpolymath/vcl-ut)
+  is the certifier. Phase 1 is to gate at L1–3 and Phase 4 at L4–6, the L6
+  ceiling vcl-ut certifies from source today; Phase 5 adds no further gate level
+  (L7–10 are future vcl-ut work). The current engine stub prints the level names
+  and does not yet invoke the gate, so no phase certifies anything today.
 
 * **Output** — Reconstructed database in VeriSimDB format (all 8 modalities
   populated), with per-entity confidence scores, proof certificates, and
@@ -235,10 +244,14 @@ function: recovery is complete when cross-modal drift approaches zero.
 
 == Status
 
-**Concept stage (2026-11-05).** Architecture sketched, phases defined, engine and
-client are stubs, no proofs exist yet. The route to a working recovery and to the
-first mechanised results, the decisions still open, and what must be created in
-verisimdb, vcl-ut, echo-types and tropical-types are in `docs/ROUTE-PLAN.adoc`.
+**Concept stage (2026-11-05; proof ledger 2026-11-09).** Architecture sketched,
+phases defined, engine and client are stubs. No proof lives in this repository
+and nothing about the Rust engine is proved; the first mechanised *theory*
+results for the recovery invariants (rungs R2–R10) landed in verisimdb,
+echo-types and tropical-types and are ledgered with receipts in
+link:PROOF-STATUS.adoc[PROOF-STATUS.adoc]. The route to a working recovery,
+the decisions still open, and what remains to be created in verisimdb, vcl-ut,
+echo-types and tropical-types are in `docs/ROUTE-PLAN.adoc`.
 The crate, repository and clade are named `squeakwell`; the naming table above
 is kept as the record of the alternatives.