PROOF-STATUS.adoc

echo-types — Proof Status

Table of Contents

• 1. Proof Witness Grades (PROOF-POLICY §8)
• 2. Agda cold check (2026-11-09)
• 3. CI coverage audit (2026-11-01)
  • 3.1. Local cold-check record (2026-11-01)
• 4. Build invariant (verified)
• 5. Proved (load-bearing, verified)
  • 5.1. Composition track
  • 5.2. Establishment track — Pillars A–D (narrowed by R-2026-05-18)
  • 5.3. Canonical-identity spine (Tier 1/2/3)
  • 5.4. Design audit (2026-11-09)
  • 5.5. Ordinal / Buchholz track — moved
• 6. Identity and adjacency: EI-2 disposition
• 7. Epistemic-types actual-source comparison
• 8. Open (honest — NOT proved)
• 9. Discipline
• 10. 2026-11-06 toolchain and warning receipt

Important

Foundation scope correction, 2026-11-06. The current contract is the standard dependent fibre and its scoped interfaces. Earlier “modality” means a preorder-indexed diagram, and historical “no-section” negatives mean no left inverse. The parallel-arrow example refutes arbitrary-arrow independence, not chosen-composite functoriality. Fibre-composition inverses do not establish a tropical graded monad; erasure obstructions do not ban every graded comonad. Selected lossy-encoding examples do not separate Echo from general Σ-types, and novelty/priority remain unresolved. Build counts and green receipts below are dated records, not certification of local edits; see the audit evidence. These qualifications supersede broader formulations below.

The latest research-cycle receipt records five additional modules, 27 successful direct/aggregate checks, and three sibling integration checks. The claims are finite alphabet bounds, an explicitly sequential protocol and compositional measurements; runtime enforcement and generic tropical coherence remain open.

Honest status of the echo-types Agda formalisation: what is proved, what is open, and the build/guardrail invariant. echo-types is a constructive Agda development (--safe --without-K); the main verified suite (proofs/agda/All.agda) is postulate-free. The one quarantined postulate block outside that suite (the --safe --without-K shadow of propositional truncation) is enumerated below. The ordinal lane, including its order-type Fidelity scaffold, moved to hyperpolymath/ordinal-notation on 2026-10-20.

1. Proof Witness Grades (PROOF-POLICY §8)

Grades are computed per theorem from receipts and §2.2 records. They are never assigned to the repository as a whole.

Theorem	PWG	Record
EchoSearchExample headlines (search-double-6-decided, search-as-echo, search-as-cost, search-as-dec, search-as-feasible)	PWG-2ii, no axioms	proofs/RECHECK-EchoSearchExample.adoc. The Agda receipt is the cold check at ccec4d7 (2026-11-09). The Rocq and Lean legs are re-proved and kernel-checked with no axioms. They are RECONCILED by owner acceptance of the recorded statement comparison (2026-11-09). PWG-1 additionally needs current pinned CI receipts for every witness.

Census (PROOF-POLICY §8.4), counted per theorem on 2026-11-09 over the 722 headline pins in the using clauses of proofs/agda/Smoke.agda (the pins include some definitions as well as theorems): PWG-1 0, PWG-2ii 5, PWG-2i 0, PWG-3 0, ungraded 717. The five graded theorems are the EchoSearchExample headlines above; every other pin is ungraded because no per-theorem record exists for it yet. Agda results for the whole closure are dated checks, not grades.

2. Agda cold check (2026-11-09)

At source commit ccec4d79866e3e433ae2268d2f8b7899396cb34f, with a clean tree and the CI toolchain from scripts/setup-agda.sh (Agda 2.7.0.1; release archive sha256 975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a; stdlib 8326c74; absolute-zero f486c29), these all exited 0:

• the five static guards (kernel, experimental aggregate wiring and controls, invocation lint, foundation guardrail);

• the seven --safe --without-K --cubical-compatible roots, cold (--ignore-interfaces): All, Smoke, AuditSmoke, characteristic/All, examples/All, experimental/echo-additive/All and NarrowingSmoke;

• the --safe --cubical island.

The only warnings were the known UnsupportedIndexedMatch ones (triage remains open; see below). The log is docs/receipts/agda-cold-2026-11-09.log.gz; the uncompressed log has sha256 7f9de4d1f874a0f249eadeb3fc675be346f437cb28cb31fd3e6db1b635e54eb0. This is a local run of a clean commit with the pinned toolchain. It is not a GitHub Actions receipt.

3. CI coverage audit (2026-11-01)

• experimental/echo-additive/ has a separate aggregate entrypoint, but it is currently a step in both existing Agda jobs, not a separately named job. Grade, VarianceGate, GradedCarrier, GradedCarrierFaithful, GradedMonad, GradedComonad, and GradedAdjunction are imported by that entrypoint. They remain outside the shipped All.agda closure; the retracted comonad claim is not reinstated. A static CI check now rejects direct files missing from the aggregate; it is only a wiring check, not a proof check.

• NarrowingSmoke, EchoExampleTruncation, EchoExampleBitNarrowing, and EchoBitNarrowingNumeric are retained for the bit-narrowing exhibit. The working-tree workflow invokes NarrowingSmoke (which imports the other three) in warm and cold jobs under the standard profile. A local cold check now succeeds as detailed below; the changed workflow has not yet had a successful CI run. The exhibit remains outside the shipped All.agda closure and is not a clean-commit PWG-3 receipt.

• On 2026-11-01 the local cold checks and static guards passed with Agda 2.7.0.1-cf6e2d9 and stdlib v2.3. The compiler is not the latest upstream stable; CI’s compiler remains unpinned (#322). Full provenance, warnings, and the dirty-working-tree limitation are recorded below. The workflow verifies stdlib commit 8326c7475af1fa456ca04a0203c168d5d7ff842b but does not pin Agda.

• GitHub Actions run 41240570315 at source commit b0982c44f36133acd2d0e1d4e03cf031fff7a470 reports success for both check and cold-check, including the experimental aggregate step and cold typecheck. This is a prior CI receipt, not a run of the current working-tree changes; GitHub job logs were inaccessible here, so the compiler version, warning counts and per-module output were not independently inspected. The narrowing exhibit was not invoked.

bash scripts/check-grade3.sh runs all six non-cubical entrypoints with --ignore-interfaces --safe --without-K --cubical-compatible, the separate full-cubical island with --ignore-interfaces --safe --cubical, and the static guards. This follows the default invocation in the estate proof policy, §2.1. The local run below checked these invocations. The full-cubical island needs the policy’s separately reviewed profile; its historical success is not review or a receipt for the default profile. The current working-tree entrypoint uses the source’s existing separate --safe --cubical options because it constructs propositional truncation as a higher inductive type; profile review remains OPEN, and this island is not part of the --without-K aggregate. The postulated shadow remains quarantined as documented in docs/proof-debt.adoc.

3.1. Local cold-check record (2026-11-01)

bash scripts/check-grade3.sh exited 0 with --ignore-interfaces on All, Smoke, characteristic/All, examples/All, experimental/echo-additive/All, and NarrowingSmoke, using the combined --safe --without-K --cubical-compatible profile. The separately checked EchoImageFactorizationPropCubical also exited 0 with --safe --cubical; that is not approval of its separate profile. The invocation lint, kernel, foundation, and aggregate-wiring guards passed. An independent test module with an unsolved hole was rejected (exit 42); it is not a theorem check.

• Agda: PyPI agda==2.7.0.1, native Python 3.11 x86-64 wheel SHA-256 361ba14d06cac8cdcd5a703acd8dc52104f8e2dddc9d55f58c6cb5915d076a4d; reported 2.7.0.1-cf6e2d9. Its missing data directory was supplied from upstream Agda v2.7.0.1 source commit a6fc20c27ae953149b53a8997ba4a1c8b17d628a. This is not the latest upstream release (v2.8.0.2) and is not a CI toolchain pin.

• Stdlib v2.3: 8326c7475af1fa456ca04a0203c168d5d7ff842b; absolute-zero: f486c29903434589117fa0662c6f29b0f17d1d5f. Both checkouts and the Agda data source had clean tracked files.

• Source base b0982c44f36133acd2d0e1d4e03cf031fff7a470, with a dirty working tree for documentation, workflow, and scripts; no proofs/agda files were changed relative to that base. The complete proof-source hash manifest is docs/receipts/agda-local-2026-11-01-sources.sha256. This is a working-tree result, not a clean-commit CI receipt or a blanket grade for every theorem/file.

• Output had 957 UnsupportedIndexedMatch warning occurrences: 353 for All, 351 for Smoke, 100 for characteristic, 106 for examples, 43 for experimental, 4 for narrowing, and 0 for the cubical island. Repeated checks include the same warnings: 81 distinct source locations in 24 proof files. The warning says affected functions do not compute when applied to transports in Cubical Agda. Exit 0 is not warning-free Cubical computational compatibility. Triage remains open.

• Complete combined stdout/stderr is preserved in docs/receipts/agda-local-2026-11-01.log.gz (uncompressed SHA-256 617263834bee297a9f8e092c32e7cd9934af940f1e9fa7f9e19663b44cde99ad). No new clean-commit PWG-3 promotion is asserted on this basis.

In separate copied proof trees, replacing fin-injective refl = refl in experimental Grade with a hole caused its aggregate to exit 42, while the main aggregate on that same mutated tree exited 0. Replacing the halve-double zero proof in EchoExampleTruncation with a hole caused NarrowingSmoke to exit 42. These local tests used --no-libraries with explicit library paths and the standard safety flags; their logs are docs/receipts/agda-mutant-{grade,grade-main,narrow}-2026-11-01.log.gz. They establish local sensitivity and experimental isolation, not a green CI run or the separate named CI check requested in #321.

4. Build invariant (verified)

• --safe --without-K throughout proofs/agda/**.

• agda proofs/agda/All.agda and agda proofs/agda/Smoke.agda exit 0. Last verified 2026-11-09 (local, cold, Agda 2.7.0.1 + the pinned stdlib and absolute-zero via scripts/setup-agda.sh; all eight CI entrypoints and the four guard scripts passed; not a CI receipt).

• Guardrails are CI-enforced (tools/check-guardrails.sh): every file under proofs/agda/** must declare {-# OPTIONS --safe --without-K #-}, and believe_me, postulate, TERMINATING, REWRITE, NO_POSITIVITY_CHECK, primTrustMe, etc. are rejected. The main suite is postulate-free.

5. Proved (load-bearing, verified)

5.1. Composition track

• Echo-comp-iso — base accumulation isomorphism.

• cancel-iso — per-fibre cancellation (parameterised by s-left/s-right
  both triangle identities).

• Pentagon coherence — Echo-comp-pent-Σ-assoc (full Σ-associativity iso).

5.2. Establishment track — Pillars A–D (narrowed by R-2026-05-18)

• A EchoFiberBridge.agda — echo↔fib definitional bridge (Echo ≡ fibre).

• B EchoGradedComonad.agda and EchoPullback.agda are real modules, but R-2026-05-18 withdrew the "graded-comonad laws" and "terminal-cone universal property" readings (docs/retractions.adoc). What stands: EchoGraded is a thin-poset reindexing modality, and EchoPullback proves existence with pointwise uniqueness; the strict universal property is the funext-qualified F4 module.

• C EchoSeparating.agda — separating model; characteristic law refuted.

• D EchoRelModel.agda — GCLaws instantiated at set-model and rel-model, which share one grade poset: carrier-parametricity over a fixed poset, not semantic model-independence. The conservativity metatheorem was withdrawn and now lives in docs/retracted/conservativity.adoc.

5.3. Canonical-identity spine (Tier 1/2/3)

EchoTotalCompletion (A ≃ Σ B (Echo f)), EchoOrthogonalFactorizationSystem, EchoImageFactorization, EchoNoSectionGeneric, EchoLossTaxonomy, EchoResidueTaxonomy, EchoDecorationStructure, EchoObservationalEquivalence, EchoEntropy, EchoLLEncoding, the funext-qualified full-OFS gate F5 (EchoOFSUnivF5*), the audience moves (EchoProvenance, EchoSecurity, EchoProbabilisticSupport, EchoDifferential), EchoCanonicalIdentitySuite, EchoDeniability, and EchoAggregation (micro→macro aggregation as an Echo map; pairSum-non-injective + no-canonical-disaggregation).

5.4. Design audit (2026-11-09)

A statement-level review against the claims in this file, Smoke.agda comments and module headers. Every term type-checks; these entries record where a statement says less than the surrounding text claimed. Comments and labels were corrected in the same change; no proof term changed.

Result	What it actually states
EchoThermodynamicsArbitrary.bennett-reversible-arbitrary	Vacuous as stated: the injectivity hypothesis is unused and the cost is 0 for every f. Kept, deprecated. Resolved 2026-11-09: bennett-enumerated computes the cost from an enumeration of the fibre (preimages, complete, no repeats) and needs inj; landauer-fan-in proves the converse (two distinct preimages cost at least k·T), and collapse-erasure-cost shows Bool → ⊤ costs exactly T.
EchoDeniability.partial-deniable-restricted	Restates its hypothesis (IsConstantOpener d is the goal). No exactness or minimality of the constant-opener class is proved.
Echo.Separation.NotResourceInstance.measure-not-injective	Conditional: a measure that already agrees on two distinct echoes identifies them. It does not show every measure is lossy.
EchoAbstractionBarrier	Shows affine consumers are blind and proj₁ is not. There is no enforced barrier: Echo is a transparent Σ.
EchoEntropy	The shadow is constant, so "blind" holds by construction. Not a Shannon entropy result; real-valued entropy stays open.
EchoLLEncoding	Holds for encodings whose linear carrier is a proposition. Not a statement about all LL encodings (the identity encoding keeps no-section).
F5 (EchoOFSUnivF5*)	Existence of a comparison iso, not its uniqueness; the lifting uses only that one leg is an equivalence. "F5 full pass" means the three slices landed, not a full orthogonal factorisation system in the usual sense.
EchoVariance, EchoGradedComonadF1 (Smoke comments)	The maps do not supply a graded monad, the fibre round trips are not an adjunction, and F1 is a lossless writer that does not mention Echo.
EchoProvenance	Its Echo-vs-Σ clearance claim does not hold (Echo is definitionally Σ).
EchoImageFactorizationProp	Conditional on a TruncInterface that the --safe build does not supply; the (epi, mono) gate stays open.

Under PROOF-POLICY §8 every theorem here is ungraded: no PWG-3 receipt (Agda version, standard-library pin, flags, import cone, commit) is recorded in-repo, and no Rocq or Lean leg exists. CNO-facing results also inherit the limits recorded in absolute-zero’s 2026-11-09 design audit (its IsCNO is degenerate).

5.5. Ordinal / Buchholz track — moved

The ordinal lane left echo-types on 2026-10-20 (echo-types#349, decision D-2026-06-21) and now lives in hyperpolymath/ordinal-notation, with its results and open problems. What stays here is the echo-to-ordinal bridge EchoOrdinal (ordinal-collapse-non-injective) and the two modules it imports, Ordinal.OmegaMarkers and Ordinal.Buchholz.Syntax.

6. Identity and adjacency: EI-2 disposition

• Closed negatively — EI-2, PATH B. The claim that the existing decoration-order / echo-indexed-family / transport recipe supplies substantive simultaneous cross-axis interaction as a Gate 1 distinctness argument did not survive the investigated cases. The seven recorded data points and the RoleRole structural argument support that verdict; they are not a universally quantified no-go theorem. The generic 2D iff remains unproved. See docs/EI2_REPORT.adoc.

• Narrowed, not retracted wholesale. Gate 1’s remaining arguments concern proof-relevant witnesses versus specified propositional or single-witness accounts, and the cited quotient/Galois 2-cell constructions. These are neighbour- and model-specific, not proof that the fibre is a novel construction. Echo f y is definitionally a fibre; bare Echo coincides with HoTT fibres and Σ-relevant refinements.

• Open and separate. The adequacy of a characteristic theorem family for an overall positive identity remains contested: README criterion 2 remains unmet, while the historical Gate 2 audit records a narrower protocol pass (docs/characteristic.adoc). They are not the same standard. Specific encodability/comparison questions against QTT and modal calculi, type-theoretic IFC, and the Galois/quotient settings remain, as do any coupled-state or multiple-live-position extensions; none reopens EI-2 or earns back the rejected distinctness claim merely by encoding or failing to encode RoleGraded.

7. Epistemic-types actual-source comparison

At epistemic-types commit 5422cd5bf1418c44321bf0f77e894737a451d8f5, tests/integration/CanonicalEcho.agda imports Echo source pinned by its workflow to 46cd1a32d4dcf1020f01dd1aab41f816742da10e. It proves fromTo and toFrom for its local certified-residue record and EchoResidue.EchoR, plus lowerAgreesWithCanonical for lowering an introduced source witness. The local interface supplies observe, retain, Cert, and sound; it is not a representation of all Echo structure and supplies no unconditional recovery, provenance or loss bound. Resource bounds are separate from Echo’s identity.

The sibling’s GitHub Actions run 40445723481 reports the correspondence job and its proof step successful at that sibling commit. This is a CI receipt for its pinned Echo revision, not a proof of identity distinctness.

On 2026-11-01 the same sibling integration module was also checked locally against both its pinned Echo revision and this checkout’s unmodified proof sources (base b0982c44f36133acd2d0e1d4e03cf031fff7a470). Both exited 0 with Agda 2.7.0.1-cf6e2d9, stdlib v2.3, --no-libraries --safe --without-K --cubical-compatible --double-check --ignore-interfaces and explicit sibling, Echo and stdlib include paths. Each emitted 37 UnsupportedIndexedMatch warnings. This is a different compiler and stdlib from the sibling CI and did not use its -W error configuration; it is a local check of that test, not a re-run of the sibling’s workflow. Logs are docs/receipts/epistemic-{pinned,current}-local-2026-11-01.log.gz (uncompressed SHA-256 respectively bd2241d145490034f869c3e412659abe366c0e2d286d880ab8bf58e32b4630bb and 2728522400edb96b9e96af91840d8cec015b11797999737af29e79f7099b7640). This does not broaden what the test proves.

8. Open (honest — NOT proved)

• Bachmann–Howard order-type fidelity — OPEN, now tracked in ordinal-notation together with its two quarantined postulates (denotation, ordinal-upper-bound).

• EchoImageFactorizationPropPostulated.agda — 1 isolated postulate block (four truncation primitives). Not imported by All.agda; tracked as (c) in docs/proof-debt.adoc.

• (epi, mono) image truncation — ∥_∥ is constructed only in the --cubical island EchoImageFactorizationPropCubical.agda; under --safe --without-K it remains a shadow (it cannot be built within --safe --without-K without HITs).

• Pillar E paper (docs/echo-types/paper.adoc) — LIVING DRAFT with [EXPAND] tags (background, related work, evaluation, ordinal consumer-evidence appendix gated on the BH milestone, now an ordinal-notation milestone). Not submitted.

9. Discipline

• No postulate in load-bearing tracks (the one truncation-shadow block in EchoImageFactorizationPropPostulated.agda is the sole, isolated, documented exception).

• Smoke.agda pins selected headline theorems; it is not a coverage guarantee for every module. The main All.agda closure is distinct from the separately invoked cubical and experimental roots. The narrowing root now has its own Bit-narrowing exhibit job, which passed at repair head f413ea14012a6d2ea428a3746070e4b92678df1f in Agda run 42226213296; see the dated November 6 update and readiness ledger below. Unwired modules must not be treated as checked.

• The EI-2 integration-recipe-distinctness investigation is terminated negatively and must not be reopened (see docs/EI2_REPORT.adoc); the narrower adjacency questions above are separate.

10. 2026-11-06 toolchain and warning receipt

This dated update supersedes the earlier current-status wording about unpinned CI and undispatched narrowing. PR #360 introduces the checksum-pinned official Agda 2.7.0.1 binary and separate core, cold, experimental, narrowing and Cubical jobs. Local setup verifies stdlib commit 8326c7475af1fa456ca04a0203c168d5d7ff842b (v2.3) and absolute-zero commit f486c29903434589117fa0662c6f29b0f17d1d5f. The main-branch release status must be read from the readiness ledger; a draft PR and local checks do not mean every remote job has passed.

Fresh warning counts under these exact dependencies are measured below. A count is the number of emitted warning: -W[no]UnsupportedIndexedMatch diagnostics, with the immediately preceding .agda location used to identify stdlib origins. Warnings may be replayed through imports; these are log-message counts, not distinct defects or a comparable score across different root/cache profiles. No warning-suppression flag was used.

Receipt	All emitted	Stdlib emitted	Scope
AuditSmoke-cold.log	1264	1167	Fresh --ignore-interfaces AuditSmoke closure
All-final.log	888	771	Final local All check with existing interfaces
container-build.log	1935	1522	Fresh container All closure, ordinary safe profile

The exact reproduction commands, source identities, ordinary/Cubical boundary, new ordered-erasure warning limitations and independent proof-lane negative controls are recorded in the proof ledger and the readiness ledger. Raw local receipts and warning-counts.json remain under ignored build/audit-2026-11-06/. The older November 1 measurements retain their original date and candidate toolchain; they are not silently relabeled.