// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = 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 ` 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.