PROOF-STATUS.adoc

squeakwell — Proof Status (ledger)

Table of Contents

• Status vocabulary
• Ledger (one row per rung)
• Receipts (2026-11-09, this session’s environment)
• What is NOT covered

Requirements: PROOF-NEEDS.adoc. Ladder and repaired statements: 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)

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)

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: hyperpolymath/verisimdb#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: hyperpolymath/tropical-types#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.