diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml index 5637283..bf6ccac 100644 --- a/.github/workflows/agda.yml +++ b/.github/workflows/agda.yml @@ -45,6 +45,12 @@ jobs: - name: Kernel funext-free certificate + classification guard run: sh scripts/kernel-guard.sh + - name: Check experimental aggregate covers its direct modules + run: bash scripts/check-experimental-aggregate.sh + + - name: Check Agda invocation profiles (static) + run: python3 scripts/check-agda-invocations.py + - name: Install Agda and standard library run: | sudo apt-get update @@ -73,6 +79,7 @@ jobs: run: | STDLIB_DIR="$HOME/agda-stdlib" git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git "$STDLIB_DIR" + test "$(git -C "$STDLIB_DIR" rev-parse HEAD)" = 8326c7475af1fa456ca04a0203c168d5d7ff842b echo "stdlib_dir=$STDLIB_DIR" >> "$GITHUB_OUTPUT" - name: Fetch absolute-zero library (PINNED) @@ -138,16 +145,16 @@ jobs: agdai-${{ runner.os }}-stdlib2.3- - name: Typecheck full suite - run: agda -i proofs/agda proofs/agda/All.agda + run: agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/All.agda - name: Smoke-check headline theorems - run: agda -i proofs/agda proofs/agda/Smoke.agda + run: agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/Smoke.agda - name: Typecheck characteristic lane (Gate #2 audit modules) - run: agda -i proofs/agda proofs/agda/characteristic/All.agda + run: agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/characteristic/All.agda - name: Typecheck examples lane (Gate #3 canonical examples) - run: agda -i proofs/agda proofs/agda/examples/All.agda + run: agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/examples/All.agda # Cubical lane: the (epi, mono) truncation discharge. A --cubical # --safe island (zero postulates) that CONSTRUCTS ∥_∥ as a HIT — @@ -155,7 +162,7 @@ jobs: # is typechecked directly here. Its --without-K-profile shadow is # EchoImageFactorizationPropPostulated (proof-debt (a)/(c)). - name: Typecheck cubical lane (epi/mono truncation discharge) - run: agda -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda + run: agda --safe --cubical -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda # Experimental lane: the echo-additive grade tree, typechecked through # its own aggregate root (--safe --without-K from the pragmas); @@ -165,7 +172,11 @@ jobs: # that vendor Grade.agda (choreographic-types) learn here, not # in their own CI, when an edit breaks it. - name: Typecheck experimental echo-additive lane (standalone, not in the closure) - run: agda -i proofs/agda proofs/agda/experimental/echo-additive/All.agda + run: agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/experimental/echo-additive/All.agda + + # A separate entrypoint, not evidence about the shipped closure. + - name: Typecheck bit-narrowing exhibit + run: agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/NarrowingSmoke.agda cold-check: # Belt-and-braces: NO interface cache, --ignore-interfaces cold @@ -195,9 +206,11 @@ jobs: run: | STDLIB_DIR="$HOME/agda-stdlib" git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git "$STDLIB_DIR" + test "$(git -C "$STDLIB_DIR" rev-parse HEAD)" = 8326c7475af1fa456ca04a0203c168d5d7ff842b ABSZ_DIR="$HOME/absolute-zero" git clone https://github.com/hyperpolymath/absolute-zero.git "$ABSZ_DIR" git -C "$ABSZ_DIR" checkout --quiet "$ABSZ_REF" + test "$(git -C "$ABSZ_DIR" rev-parse HEAD)" = "$ABSZ_REF" mkdir -p "$HOME/.agda" printf 'name: standard-library\ninclude: %s/src\n' "$STDLIB_DIR" > "$RUNNER_TEMP/sl.agda-lib" printf 'name: absolute-zero\ninclude: %s/proofs/agda\n' "$ABSZ_DIR" > "$RUNNER_TEMP/az.agda-lib" @@ -206,9 +219,10 @@ jobs: - name: Cold typecheck (--ignore-interfaces, no cache) run: | - agda --ignore-interfaces -i proofs/agda proofs/agda/All.agda - agda --ignore-interfaces -i proofs/agda proofs/agda/Smoke.agda - agda --ignore-interfaces -i proofs/agda proofs/agda/characteristic/All.agda - agda --ignore-interfaces -i proofs/agda proofs/agda/examples/All.agda - agda --ignore-interfaces -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda - agda --ignore-interfaces -i proofs/agda proofs/agda/experimental/echo-additive/All.agda + agda --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/All.agda + agda --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/Smoke.agda + agda --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/characteristic/All.agda + agda --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/examples/All.agda + agda --ignore-interfaces --safe --cubical -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda + agda --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/experimental/echo-additive/All.agda + agda --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/NarrowingSmoke.agda diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index ff2d733..1770942 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -237,6 +237,9 @@ we name them as three. * *The retracted "graded comonad" reading stands retracted* (R-2026-05-18): echo-types is a loss-graded _reindexing modality_ (thin-poset action); the experimental `echo-additive/` tree is not wired into the shipped closure. + The current Agda workflow invokes its separate aggregate as a step in + both jobs, not as an independently named job; see `PROOF-STATUS.adoc` + for the coverage and verification limits. [#reproduce] == Reproduce it yourself diff --git a/CLAUDE.md b/CLAUDE.md index d684a0f..a905113 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -1,5 +1,14 @@ +# Proof policy + +The normative estate policy is +https://github.com/hyperpolymath/standards/blob/main/3-practice/PROOF-POLICY.adoc. +Its default Agda theory profile is `--safe --without-K --cubical-compatible`; +full Cubical proofs require a separate reviewed profile. Record toolchain, +assumptions, results and exact source revisions; historical checks do not +prove the new profile. Mathesis grades are theorem- and receipt-specific. + # Ecosystem context This repo (echo-types) is one node in the hyperpolymath / PanLL ecosystem. @@ -7,8 +16,10 @@ Adjacent projects, in one line each, for session bootstrapping: - echo-types — constructive Agda formalization of fiber-based structured loss ("echo types"); `Echo f y := Σ (x : A) , (f x ≡ y)`. Gated - identity-claim development; `--safe --without-K` throughout. The - ordinal-notation / Buchholz lane moved out on 2026-10-20 (see below). + identity-claim development; ordinary proof roots use `--safe --without-K + --cubical-compatible`. The full-cubical island is a separate profile; + the postulated shadow remains quarantined. The ordinal-notation / + Buchholz lane moved out on 2026-10-20 (see below). https://github.com/hyperpolymath/echo-types - PanLL — three-pane cognitive-relief HTI; Ambient/Symbolic/Neural/World panes. https://github.com/hyperpolymath/panll diff --git a/Justfile b/Justfile index 0bc3099..afd0482 100644 --- a/Justfile +++ b/Justfile @@ -5,13 +5,13 @@ # Build all echo type modules build-echo: @echo "Building echo type modules..." - agda -i proofs/agda proofs/agda/All.agda + agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/All.agda @echo "✅ All echo modules built successfully" # Build stability tests build-tests: @echo "Building stability tests..." - agda -i proofs/agda proofs/agda/Echo/Bridges/EchoStabilityTests.agda + agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/EchoStabilityTests.agda @echo "✅ Stability tests built successfully" # Run comprehensive build @@ -25,31 +25,31 @@ build-all: test-core: @echo "Testing core echo type properties..." - agda -i proofs/agda proofs/agda/Echo/Core.agda + agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/Echo.agda @echo "✅ Core tests passed" # Test CNO bridge test-cno: @echo "Testing CNO bridge..." - agda -i proofs/agda proofs/agda/Echo/Bridges/EchoCNOBridge.agda + agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/EchoCNOBridge.agda @echo "✅ CNO bridge tests passed" # Test thermodynamic bridge test-thermo: @echo "Testing thermodynamic bridge..." - agda -i proofs/agda proofs/agda/Echo/Bridges/EchoThermodynamics.agda + agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/EchoThermodynamics.agda @echo "✅ Thermodynamic tests passed" # Test categorical bridge test-cat: @echo "Testing categorical bridge..." - agda -i proofs/agda proofs/agda/Echo/Bridges/EchoCategorical.agda + agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/EchoCategorical.agda @echo "✅ Categorical tests passed" # Test stability suite test-stability: @echo "Testing stability suite..." - agda -i proofs/agda proofs/agda/Echo/Bridges/EchoStabilityTests.agda + agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/EchoStabilityTests.agda @echo "✅ Stability tests passed" # Run all tests diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 0c17470..4c441d2 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -14,6 +14,102 @@ below. The ordinal lane, including its order-type *Fidelity* scaffold, moved to https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation] on 2026-10-20. +== 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 Grade 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 + https://github.com/hyperpolymath/echo-types/actions/runs/41240570315[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 +https://github.com/hyperpolymath/standards/blob/main/3-practice/PROOF-POLICY.adoc[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`. + +=== 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 Grade 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. + + == Build invariant (verified) * `--safe --without-K` throughout `proofs/agda/**`. @@ -58,6 +154,65 @@ 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`. +== 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`. + +== 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 +https://github.com/hyperpolymath/epistemic-types/actions/runs/40445723481[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. + == Open (honest — NOT proved) * *Bachmann–Howard order-type fidelity* — *OPEN*, now tracked in @@ -80,8 +235,11 @@ imports, `Ordinal.OmegaMarkers` and `Ordinal.Buchholz.Syntax`. * No `postulate` in load-bearing tracks (the one truncation-shadow block in `EchoImageFactorizationPropPostulated.agda` is the sole, isolated, documented exception). -* Every headline theorem is pinned in `Smoke.agda`; every module is wired into - `All.agda` (orphan modules that compile but are not in `All.agda` are treated - as dead code). +* `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 + working-tree narrowing root is pending its first CI check; see the CI + coverage audit above. Unwired modules must not be treated as checked. * The EI-2 integration-recipe-distinctness investigation is *terminated - negatively* and must not be reopened (see `.machine_readable/6a2/STATE.a2ml`). + negatively* and must not be reopened (see `docs/EI2_REPORT.adoc`); + the narrower adjacency questions above are separate. diff --git a/README.adoc b/README.adoc index bb89441..d52929c 100644 --- a/README.adoc +++ b/README.adoc @@ -113,7 +113,7 @@ The matched-negatives are where the identity claim does its hardest work: provin [CAUTION] ==== -**Positive identity is open.** Matched-negatives establish that Echo is *not* its obvious neighbours. The falsifiability criteria also require a *characteristic theorem family* — results that are naturally Echo-shaped, not just generic fiber lemmas. Whether emphasis + vocabulary + separation suffices for identity is the question the repo is designed to answer. +**Positive identity is not established.** EI-2 terminated negatively via PATH B: the investigated integration recipe does not supply substantive simultaneous cross-axis interaction as a distinctness argument. The narrower truncation and 2-cell arguments remain for the specified neighbour models; Echo itself is the fibre, not a novel construction. Whether the remaining evidence satisfies a positive identity claim is separate from the closed EI-2 question, and the characteristic-family criterion remains contested. ==== [CAUTION] @@ -224,17 +224,19 @@ The claim is established only if all three are met: If these fail, we record that result and stop the identity claim. -Criterion 1 is supported by the matched-negatives (Echo is not entropy, not LL encoding, not a resource grade). Criterion 2 is open: the Tier-1 theorem is standard, and the remaining theorems are standard consequences of non-injectivity restated in Echo vocabulary. Criterion 3 is supported by the audience surfaces and tutorials. The repo is structured to make the gap in criterion 2 visible and falsifiable. +Criterion 1 has scoped matched-negative evidence, not a universal separation from all neighbouring formalisms. EI-2's attempted simultaneous cross-axis integration argument is *closed negatively*, not an open identity obligation; Gate 1 was narrowed to the truncation and 2-cell arguments (`docs/EI2_REPORT.adoc`). Per-neighbour encodability comparisons against modal type theories and type-theoretic IFC remain open, but do not restore the rejected argument. + +Criterion 2 is not established under this README's demand for results beyond generic fibre lemmas: the Tier-1 theorem is standard, and the remaining results must be judged against that demand. `docs/characteristic.adoc` records a historical, narrower protocol pass for its nominees; that pass does not by itself settle the stronger identity claim. Criterion 3 has supporting examples and tutorials. See `PROOF-STATUS.adoc` for these distinctions and the narrowly scoped epistemic-types actual-source correspondence. == Build [source,bash] ---- # Core -agda -i proofs/agda proofs/agda/Echo.agda +agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/Echo.agda -# Full suite -agda -i proofs/agda proofs/agda/All.agda +# Main aggregate (does not include the separate experimental, narrowing or cubical roots) +agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/All.agda ---- == Installing as a library diff --git a/docs/EI2_REPORT.adoc b/docs/EI2_REPORT.adoc index 8f2c025..ed8c7f3 100644 --- a/docs/EI2_REPORT.adoc +++ b/docs/EI2_REPORT.adoc @@ -4,9 +4,9 @@ :toc: macro :source-highlighter: rouge -This document is the working record for EI-2. It will be updated as -data points accumulate. EI-2 is *not terminated* until expressly -declared terminated in this document or in `next-questions.adoc`. +This document preserves the working record for EI-2. The authoritative +final status below is *terminated negatively via PATH B*; earlier +investigation stages and superseded criteria are retained as history. toc::[] @@ -59,9 +59,10 @@ to reflect this across five doc locations (see "Documentation cascade" below). *Why PATH B (partial formalisation accepted as sufficient).* The -full 2D iff theorem is not formalisable in safe Agda without -postulates (decidable equality on decoration types, F-collapses -axioms, extensionality on cell actions). `RecipeTheorem.agda` +full generic 2D iff theorem was not formalised: the attempted route +would require additional assumptions (decidable equality on decoration +types, F-collapses axioms, extensionality on cell actions). This is +not a proof that every safe formulation is impossible. `RecipeTheorem.agda` proves the per-axis halves; `RecipeNonTriviality.agda` proves the concrete construction-by-construction halves; `RoleRole.agda` provides the structural argument that even two non-loss-only @@ -407,10 +408,10 @@ formalising the conjectured 2D iff (technical work, structural obstructions known and documented) or declaring partial closure acceptable. -== Termination criteria for EI-2 +== Earlier termination criteria for EI-2 (superseded) -EI-2 will be declared *terminated* if and only if one of the -following holds, with explicit formalised evidence: +Before PATH B, the investigation proposed termination if one of the +following held with explicit formalised evidence: * *Strict-reading falsifier sustained:* multiple data points show that the recipe is uniformly trivial across loss-only axis @@ -430,9 +431,8 @@ following holds, with explicit formalised evidence: (e.g., a different choice of family `F : D₁ → D₂ → Set`), and ModeGrade's 0-non-trivial result is shown to be artefactual. -Until one of these is satisfied, *EI-2 is open*. This document is -updated when new data points are added; the status line at the top -is the authoritative current state. +That earlier rule no longer governs the status: PATH B accepted the +partial formalisation and recorded the negative verdict above. [NOTE] ==== diff --git a/docs/adjacency/README.adoc b/docs/adjacency/README.adoc index add7d15..c7d25ab 100644 --- a/docs/adjacency/README.adoc +++ b/docs/adjacency/README.adoc @@ -132,7 +132,7 @@ multiplicity-vs-truncation distinction noted explicitly. | Modal type theories (QTT, etc.) | Wins against propositional-mode accounts | N/A (modal type theories make 2-cells syntactic primitives) -| Co-extensive with QTT-class systems on bare echo; integration recipe is open +| Co-extensive with QTT-class systems on bare echo; specific recipe encodings remain untested, not an open EI-2 distinctness claim | HoTT fibers | N/A (HoTT fibers are echo by another name) @@ -332,9 +332,9 @@ via `EchoVsGalois.Sophisticated`). The remaining neighbours (IFC, provenance, modal type theories, HoTT fibers) have prose adjacency notes here but no dedicated Agda formalisation. Each note states what would be required for -formalisation and forwards the obligation to either Q2.x (for -recipe-level distinctness from a given neighbour) or to Q3.x -(for a canonical example exercising the distinctness). +formalisation and forwards specified neighbour-comparison obligations +to Q2.x or example work to Q3.x. These are not a reopening of EI-2's +terminated integration-distinctness claim. The honest summary: gate #1 has a strong consolidated argument plus formalised obstructions against the two strongest neighbours diff --git a/docs/adjacency/information-flow.adoc b/docs/adjacency/information-flow.adoc index 50cbd0c..bd66c89 100644 --- a/docs/adjacency/information-flow.adoc +++ b/docs/adjacency/information-flow.adoc @@ -83,7 +83,7 @@ the primitive object; there are no parallel transports between classes to compare. Type-theoretic IFC variants might admit a 2-cell argument; this is part of the open question. -== Recipe-level distinctness (open question) +== Recipe encodability (open comparison, not EI-2) The substantive question this neighbour raises: @@ -92,10 +92,10 @@ Does any type-theoretic IFC variant carry the recipe (custom propositional decoration order + echo-indexed family + transport action) natively? -If yes, gate-1 weakens against that variant — type-theoretic IFC -becomes a co-extensive neighbour, like Σ-relevant refinement and -QTT-class modal type theories. If no, the recipe is genuinely -echo-specific against this neighbour. +An encoding would document a correspondence for the chosen variant; +a failed attempt would not by itself prove non-encodability. EI-2 +already closed the simultaneous cross-axis integration distinctness +argument negatively, independently of this neighbour comparison. I do not know the answer. Type-theoretic IFC includes a wide family: dependent-type-system non-interference (e.g., Coq @@ -111,8 +111,9 @@ A worked formalisation would: . If yes, write the recipe in that variant's syntax and check whether the resulting "characteristic" theorem family (in the gate-2 sense) is non-trivial. -. If non-trivial, weaken the gate-1 distinctness claim against - that variant; if trivial or impossible, retain. +. Record exactly the resulting statement, assumptions and any + non-triviality evidence. Do not infer an impossibility theorem from + a stuck attempt or restore the rejected integration argument. == What echo adds (over relational IFC) @@ -134,11 +135,10 @@ policy enforcement. == What echo may not add (over type-theoretic IFC) -This is the open question. If a type-theoretic IFC variant -carries the recipe natively, the win against that variant -weakens. The honest framing would then mirror the modal-type- -theory case: "co-extensive with type-theoretic IFC variant X; -distinct from relational variants." +The open question is which specified type-theoretic IFC variants +can express the relevant witness structures and recipe. Any +correspondence needs a precise statement; neither an encoding nor +its absence alone establishes a general Gate 1 verdict. == Retraction conditions @@ -175,8 +175,9 @@ Forwarding to: * Truncation argument (relational IFC): *formalised* via `EpistemicUpdate.echo-not-prop`. -* Recipe-level argument (type-theoretic IFC): *open*. Genuinely - open work, not boilerplate. +* Encodability in specified type-theoretic IFC variants: *open + comparison*. EI-2's simultaneous-interaction distinctness argument + is *closed negatively*. * No dedicated `proofs/agda/adjacency/IFC.agda` formalisation. == References diff --git a/docs/adjacency/modal-type-theories.adoc b/docs/adjacency/modal-type-theories.adoc index e5dc241..d4d9320 100644 --- a/docs/adjacency/modal-type-theories.adoc +++ b/docs/adjacency/modal-type-theories.adoc @@ -9,8 +9,9 @@ _Axes engaged: 5 (Comp), 7 (PR/PI); axis 8 (IT/Comp) open — QTT-style quantita *Verdict: co-extensive with QTT-class systems on bare echo.* Not distinct from native modal type theories on the type level; the win is over propositional / classical accounts of modes. -Integration recipe is an open question against modal type -theories with sufficient ambient structure. +Whether specific modal theories can express the recipe is an open +*comparison*, not an open claim of simultaneous cross-axis distinctness: +EI-2 terminated that claim negatively via PATH B. This neighbour was identified during gate-3's `LinearErasure` analysis. It was not on the original five-neighbour list in the @@ -53,8 +54,10 @@ win for Echo; no loss either." Echo coincides with native modal type theories on the type level in QTT-class systems. The win is over *propositional* / *classical* accounts of mode erasure, not over modal type theories themselves. -Integration recipe distinctness against modal type theories with -sufficient ambient mode structure is an *open question*. +Whether a specified modal type theory expresses the recipe or +`RoleGraded.choreo-grade-commute` natively is an *open comparison*. +EI-2's negative finding removes that recipe from the Gate 1 +distinctness argument, regardless of the comparison's outcome. == Truncation argument (against propositional accounts) @@ -82,7 +85,7 @@ type theories have rules that one accepts or rejects. The right comparison here is *recipe-level*, not 2-cell. -== Recipe-level distinctness (open question) +== Recipe encodability (open comparison, not EI-2) The substantive question: @@ -110,11 +113,9 @@ A worked formalisation would: . Attempt to prove `RoleGraded.choreo-grade-commute` (or its modal-type-theory analog) using only the modal type theory's primitives. -. Either succeed (gate-1 weakens against that variant — modal - type theories become co-extensive on the integration recipe, - not just on bare echo) or extract a stuck point (gate-1 - holds, with the modal-type-theory specific stuck point as a - distinctness witness). +. Record the result for that specified variant and its assumptions. + Success identifies an encoding; a stuck proof attempt does not prove + non-encodability or restore the terminated EI-2 distinctness claim. == What echo adds (over propositional mode accounts) @@ -153,9 +154,9 @@ as such. *Genuinely open.* Likely outcome unknown. . A demonstration that the modal type theory's mode-indexed Σ-types are *strictly* the same as echo even at the - integration-recipe level. Would weaken gate-1 against modal - type theories from "co-extensive on bare echo" to "co-extensive - on the integration recipe", a substantial reframing. + integration-recipe level. This would refine the comparison with + that specified theory, not retract or re-establish the already + terminated EI-2 argument. == Open obligation @@ -179,16 +180,17 @@ Forwarding to: * Q1.8 — adding modal type theories to the canonical neighbour list (this note is the addition). -This is the most leveraged open work in the adjacency -directory: closing the recipe-level QTT question would -substantially sharpen the gate-1 distinctness claim either way -(by retraction or by formalisation). +The QTT comparison can sharpen the scope of the neighbour analysis, +but neither outcome reverses EI-2's negative result. A proposed +coupled-state or multiple-live-position extension is a separate, +currently parked research question. == Status * Truncation argument: *formalised* via `LinearErasure.echo-not-prop`. -* Recipe-level argument: *open*. Most under-formalised case in - this directory. +* Recipe encodability in specified modal systems: *open comparison*; + the EI-2 simultaneous-interaction distinctness argument is *closed + negatively* and cannot be earned back by this comparison alone. * No dedicated Agda formalisation. == References diff --git a/docs/adjacency/provenance.adoc b/docs/adjacency/provenance.adoc index 36dc136..3217724 100644 --- a/docs/adjacency/provenance.adoc +++ b/docs/adjacency/provenance.adoc @@ -131,7 +131,11 @@ This variant is uncommon (most provenance systems prefer single-witness over propositional), but worth noting for completeness. -== Recipe-level distinctness +== Recipe comparison (not the terminated EI-2 claim) + +The discussion below compares specified annotation interfaces; it is +not a proof of universal non-encodability. EI-2 closed the simultaneous +cross-axis integration distinctness route negatively. Provenance semirings (Green-Karvounarakis-Tannen) formalise *how-provenance* as semiring-valued annotations. The recipe @@ -203,7 +207,8 @@ characteristic theorem). truncation distinction made explicit in this note). * 2-cell argument (transitive provenance): *argued* via reduction to S-2; not separately formalised. -* Recipe-level distinctness: *argued* in prose; not formalised. +* Recipe comparison with provenance annotations: *argued* in prose; + not formalised or a distinctness result after EI-2. == References diff --git a/docs/adjacency/refinement-types.adoc b/docs/adjacency/refinement-types.adoc index b595c43..231f23d 100644 --- a/docs/adjacency/refinement-types.adoc +++ b/docs/adjacency/refinement-types.adoc @@ -126,7 +126,11 @@ In propositional-predicate refinement, there's no 2-cell to argue about — the propositional predicate is opaque to the refinement- type system's term language. -== Recipe-level distinctness +== Recipe comparison (not the terminated EI-2 claim) + +The discussion below is a comparison of specified refinement interfaces. +EI-2 closed the simultaneous cross-axis integration distinctness route +negatively; this comparison cannot by itself restore it. The recipe (custom propositional decoration order + echo-indexed family + transport action — see `gate-2-handoff.adoc` Observation @@ -188,17 +192,17 @@ formalisation of "refinement-type-with-propositional-predicate ≡ propositional truncation of echo" would make the narrow distinctness claim sharper. -This is forwarded to Q2.1 (the general `echo-not-prop` -generalisation) — closing Q2.1 also discharges this open -obligation. +Q2.1 supplies a general `echo-not-prop` result; that does not by +itself formalise an equivalence for any particular refinement system. +That system-specific comparison remains open. == Status * Truncation argument: *formalised* on three domains via - `echo-not-prop`. Specific refinement-type formalisation - awaits Q2.1. -* Recipe-level distinctness: *argued* in prose; not - formalised. + `echo-not-prop`; Q2.1 provides a general form. A specific + refinement-system correspondence remains unformalised. +* Recipe encodability for specified refinement systems: *argued* + in prose, not formalised; not a distinctness result after EI-2. * Honest tied case (Σ-relevant refinement): *acknowledged explicitly*, not glossed. diff --git a/docs/bridges/cross-repo-bridge-status.adoc b/docs/bridges/cross-repo-bridge-status.adoc index ef3e53d..08a4b29 100644 --- a/docs/bridges/cross-repo-bridge-status.adoc +++ b/docs/bridges/cross-repo-bridge-status.adoc @@ -10,6 +10,25 @@ touches other repositories. [width="100%",cols="20%,20%,20%,20%,20%",options="header",] |=== |Track |echo-types side |Adjacent side |Current status |Main blocker + +|Epistemic certified-residue correspondence +|`+proofs/agda/Echo.agda+` and `+EchoResidue.agda+`, at sibling's pin +`+46cd1a32d4dcf1020f01dd1aab41f816742da10e+` +|`+epistemic-types@5422cd5bf1418c44321bf0f77e894737a451d8f5+`, +`+tests/integration/CanonicalEcho.agda+` +|The sibling test constructs both representation round trips between +its local certified-residue `+Echo+` and `+EchoResidue.EchoR+` and +proves agreement of lowering an introduced source witness. Its +https://github.com/hyperpolymath/epistemic-types/actions/runs/40445723481[run 40445723481] +reports the correspondence job and proof step successful. This is not +an Echo identity/distinctness theorem or an Echo resource instance. +|The sibling CI receipt applies to that pinned Echo revision. Subsequent +local checks of the same test passed against both that pin and this checkout, +with a different toolchain and warnings; see `+PROOF-STATUS.adoc+` for the +exact commands and logs. Recovery, provenance, loss bounds and combined runtime +behaviour require their own assumptions or evidence; the local +builtins-only interface is intentionally smaller than the full Echo +interface. |CNO bridge (Agda) |`+proofs/agda/EchoCNOBridge.agda+` |`+absolute-zero/proofs/agda/CNO.agda+` (direct import) |*Content-bridge done.* Bridge imports `+IsCNO+`, `+empty-is-cno+`, `+halt-is-cno+`, diff --git a/docs/characteristic.adoc b/docs/characteristic.adoc index 31c0b74..331183c 100644 --- a/docs/characteristic.adoc +++ b/docs/characteristic.adoc @@ -353,17 +353,13 @@ because the role-reachability constructors are reflexive (5 cases). The 2D family is asymmetric — the role parameter is only live at keep grade. -This is a *protocol-correct* closure of EI-1. It is *substantively -narrow*. The follow-up question — is the recipe robust across -other 2D combinations (Role × Mode, Mode × Grade, etc.), or did -`RoleGraded` benefit from a fortunate axis pair? — is tracked as -EI-2 in `docs/next-questions.adoc`. EI-2 is a sharpening question, -not a survival question; its negative resolution would weaken -EI-1's closure to "closed-but-narrow" but would not invalidate it. - -Do not relabel EI-1 as open. The protocol pass is the protocol -pass. EI-2 records what's still substantively open without moving -the goalposts. +This is a *protocol-correct* closure of EI-1, substantively narrow. +The follow-up EI-2 was subsequently *closed negatively via PATH B*: +the investigated pairings do not establish substantive simultaneous +cross-axis interaction. EI-1's shape tests remain passed, but the +integration recipe does not carry Gate 1's distinctness load. See +`docs/EI2_REPORT.adoc`; narrower neighbour encodability questions are +separate and do not reopen EI-2. === Status as a candidate Gate 2 nominee diff --git a/docs/estate-proof-followups.adoc b/docs/estate-proof-followups.adoc new file mode 100644 index 0000000..3238fd7 --- /dev/null +++ b/docs/estate-proof-followups.adoc @@ -0,0 +1,63 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Estate follow-up prompts + +These are requests to the owners, not assertions that the other projects +have already implemented the proposed work. Source references and current +local evidence are in `PROOF-STATUS.adoc` and `docs/proof-witness-audit.adoc`. + +== hyperpolymath/epistemic-types + +At commit `5422cd5bf1418c44321bf0f77e894737a451d8f5`, review the +`CanonicalEcho.agda` correspondence and its workflow pin to Echo +`46cd1a32d4dcf1020f01dd1aab41f816742da10e`. Independently recheck the +same integration test against a proposed newer Echo revision using your +pinned CI compiler and library, without weakening safety or the warning +policy. If it passes, decide whether to advance the pin and preserve both +revision IDs and CI output. Keep the claim limited to the two representation +round trips and agreement of lowering; do not infer recovery, loss bounds, +or equivalence of the whole theories. Echo's local Agda 2.7.0.1 test +against base `b0982c44f36133acd2d0e1d4e03cf031fff7a470` is supporting +evidence, not your project's CI receipt. + +== hyperpolymath/standards + +Review the separately identified `--safe --cubical` profile for Echo's +higher-inductive propositional truncation against `3-practice/PROOF-POLICY.adoc` +§2.1. State explicitly whether this profile is accepted, with its trust and +compatibility limits and required receipt metadata. Separately clarify how +`UnsupportedIndexedMatch` warnings under `--cubical-compatible` affect +claims about computational behavior under transport; do not treat flag +acceptance as a warning-free result. Echo's local report lists 81 distinct +warning locations across 24 files and retains the raw log. + +== hyperpolymath/the-metadatastician + +At `afac64d8b670716d23ad0bcf9c0fd0e8b45f7a0e`, inspect the README's +claim-grounding and release-evidence descriptions against +`scripts/validate-docs.sh`, `scripts/invariant-path.sh`, and +`.github/workflows/ci.yml`. The observed CI runs the documentation baseline; +the invariant-path wrapper expects a sibling checkout and invokes Cargo. +Determine which evidence checks actually run for a standalone clone and in +CI, document the boundary, and add reproducible pinned checks or explicitly +mark unavailable checks as manual. Exercise both missing-tool and failed-check +cases; do not claim grounded documentation merely because the baseline passes. +Also reconcile the README layout's `MAINTAINERS.md` with the validator's +`MAINTAINERS.adoc` after inspecting the repository's actual files. + +== hyperpolymath/ephapax + +For `formal/Echo.v` at `800030f3c92536cce57acb5e82da6cf27b942826`, run +the actual Rocq/Coq build and `Print Assumptions` for +`no_section_collapse_to_residue`, and compare its exact statement, +assumptions, and source revisions with Echo's +`EchoResidue.no-section-collapse-to-residue`. Preserve the checker output +and do not count a skipped build or a merely similar theorem as a verified +cross-language witness. See `docs/proof-witness-audit.adoc`. + +== Repository locations needed + +GitHub API requests for `hyperpolymath/stuff-of-awesome` and +`hyperpolymath/catachresis-colloquium` returned 404, and repository search +under that owner found no matching names. Supply their exact URLs or access +before tailoring prompts: their content and relation to Echo have not been +inspected and should not be inferred from their names. diff --git a/docs/gate-1-distinct-phenomenon.adoc b/docs/gate-1-distinct-phenomenon.adoc index b68740f..cf1e899 100644 --- a/docs/gate-1-distinct-phenomenon.adoc +++ b/docs/gate-1-distinct-phenomenon.adoc @@ -57,8 +57,9 @@ Two neighbours not in the original five-neighbour list are now also covered: * *Modal type theories* (QTT, Reed-Pfenning, etc.) — co-extensive - with echo on bare echo in QTT-class systems; recipe-level - distinctness is an open question. See + with echo on bare echo in QTT-class systems; recipe encodability + in particular systems remains a separate open comparison, not an + open EI-2 distinctness claim. See `docs/adjacency/modal-type-theories.adoc`. * *HoTT homotopy fibers* — echo IS the homotopy fiber; the win is over the propositional truncation modality, not over fibers @@ -85,39 +86,17 @@ domains (tropical, epistemic, linear). The remaining neighbours have framed but only-partially-formalised distinctness claims; see each file for what's done and what's open. -== Where distinctness can live +== Integration evidence after EI-2 -Not in the object. In the *integration of structured-loss across -orthogonal axes*. - -The bridge modules in `proofs/agda/` already span: - -* choreographic — role projection (`EchoChoreo`) -* epistemic — indistinguishability and knowledge (`EchoEpistemic`) -* affine/linear — strict weakening to residues (`EchoLinear`) -* graded — compositional degradation (`EchoGraded`) -* tropical — argmin-style witnesses (`EchoTropical`) - -None of the five neighbour traditions span this breadth natively. -Galois lives in lattices. IFC lives in security policies. Quotients -are usually fixed (no native graded-chain construction). Refinements -have no native grading or choreography. Provenance has no tropical -version. - -The integration theorem now in the repository is -`characteristic.RoleGraded.choreo-grade-commute`: a single theorem -on a 2D family `RoleGEcho : Role → Grade → Set` carrying both a -choreographic role decoration and a graded loss decoration, with -two independent actions (`applyRole`, `applyGrade`) that commute. -Both decoration witnesses appear on both sides of the equation, -satisfying the same-data test that the previous nominee -(`EchoIntegration.knowledge-and-controlled-degradation`, which gate-2's -audit exhibited as a literal product of disjoint facts — -see `proofs/agda/characteristic/IntegrationAudit.agda`) failed. - -This combination is not native to any one neighbour tradition. Each -neighbour would have to import machinery from at least two others to -express it. +The five bridge domains (choreographic, epistemic, linear, graded, +tropical) and `characteristic.RoleGraded.choreo-grade-commute` remain +examples of the recipe's organisation. They do not establish a novel +construction or substantive simultaneous cross-axis interaction. +EI-2 terminated that distinctness route negatively via PATH B; the +non-trivial observed cell carries one-axis-at-a-time content. The +remaining Gate 1 arguments are the scoped truncation and 2-cell +comparisons below. Specific neighbour encodings remain research +questions, not a basis for reopening EI-2. [#claim] === The Gate #1 claim @@ -168,9 +147,13 @@ This is the claim that has to survive falsification. [#falsification] == Falsification tests -Three concrete tests. Each carries an explicit retraction condition. -If any one test succeeds against echo types, Gate #1 is retracted or -substantially weakened. +T1–T3 were originally framed as attacks on the integration-based +claim. After EI-2 they remain neighbour-comparison questions, not +independent pass/fail tests for the narrowed Gate 1: the recipe no +longer carries that gate's distinctness load. Successful encodings +refine the comparison; an unsuccessful attempt alone does not prove +non-encodability. The truncation and 2-cell arguments must be assessed +against their own explicit assumptions. === T1 — Galois reduction @@ -179,14 +162,9 @@ abstract-interpretation terms — Galois connection between concrete and abstract domains, with grading expressed as a chain of approximations. -PASSES (gate falsified) if:: -The rewrite preserves all proof-relevant content with no machinery -imported from outside abstract interpretation. - -FAILS (gate supported) if:: -The rewrite cannot express the cross-axis composition without -importing graded or choreographic primitives that AI does not -natively contain. +A Galois-only encoding would establish a scoped correspondence for +the selected statement. Record any required assumptions; an unclosed +attempt is not a proof that no encoding exists. Attempt scaffolded in `proofs/agda/EchoVsGalois.agda`. @@ -196,13 +174,9 @@ Same theorem, restated as a statement about the quotient `B = A / ker f` plus a quotient-of-quotients construction for the graded chain. -PASSES (gate falsified) if:: -The restatement goes through cleanly using only quotient operations. - -FAILS (gate supported) if:: -The graded composition or choreographic action does not commute with -the quotient stacking, leaving a residue that quotient theory cannot -express. +A quotient-only restatement would establish a scoped correspondence +for the selected statement. A failure to construct one is not by itself +a universal quotient no-go theorem. Attempt scaffolded in `proofs/agda/EchoVsQuotient.agda`. @@ -212,13 +186,9 @@ Show that `EchoEpistemic`'s indistinguishability-and-knowledge results are derivable from `EchoLinear` plus a forgetful functor — i.e., that the epistemic axis is not pulling its weight. -PASSES (gate weakened) if:: -Derivation goes through. The "five axes" claim shrinks to four or -fewer; the integration argument weakens correspondingly. - -FAILS (gate supported) if:: -Derivation fails at a specific point where epistemic structure -carries content not present in linear structure. +A derivation would clarify the relation between these specified axes; +a failed attempt alone is not a proof of independence. EI-2 already +removed the five-axis integration argument from the distinctness load. This test is currently unstubbed; see <>. diff --git a/docs/next-questions.adoc b/docs/next-questions.adoc index 24bba3d..78e3f03 100644 --- a/docs/next-questions.adoc +++ b/docs/next-questions.adoc @@ -24,6 +24,13 @@ toc::[] == Gate 1: distinct phenomenon +*Scope after EI-2:* the recipe's purported simultaneous cross-axis +integration distinctness is CLOSED negatively via PATH B. Q1.1/Q1.2 +and the modal/IFC comparisons below may still ask whether specified +neighbours can encode particular constructions; those comparisons do +not reopen EI-2, and a failed encoding attempt is not a no-go theorem. +See `PROOF-STATUS.adoc` § Identity and adjacency. + === Q1.1 — Galois reduction Does there exist a Galois-theoretic construction that expresses the @@ -43,14 +50,15 @@ quotient case via the diagonal correspondence formalised. Attack path:: -Either (a) instantiate `T1-obligation` in `EchoVsGalois.agda` with -`choreo-grade-commute`'s actual signature and complete a Galois- -only proof — gate #1 falsified — or (b) extract the precise stuck -goal as a distinctness witness. +Instantiate `T1-obligation` with `choreo-grade-commute`'s +signature and investigate a Galois-only encoding, recording its +assumptions or the precise unresolved goal. This compares a specified +construction; a stuck goal alone is not a distinctness theorem. -Retraction:: -If (a) succeeds without importing primitives outside abstract -interpretation, gate #1 is falsified by T1. +Interpretation:: +A successful encoding informs the Galois comparison. EI-2 has already +removed this recipe from Gate 1's distinctness load, so this test alone +neither falsifies the remaining arguments nor restores the rejected one. === Q1.2 — Quotient reduction @@ -69,14 +77,14 @@ structural barriers to safe-Agda formalisation. See Q1.6 for the sub-case state. Attack path:: -Same as Q1.1: instantiate `T2-obligation` with -`choreo-grade-commute`'s signature and either complete a -quotient-only proof or extract the stuck goal. +As in Q1.1, instantiate `T2-obligation` with +`choreo-grade-commute`'s signature and investigate a quotient-only +encoding, recording its assumptions or unresolved goal. -Retraction:: -If a quotient encoding without echo machinery succeeds on the -characteristic-family commutation theorem, gate #1 is falsified -by T2. +Interpretation:: +An encoding refines the quotient comparison; a failed attempt is not +proof of non-encodability. Neither outcome by itself decides the +narrowed Gate 1 arguments or reopens EI-2. === Q1.3 — Informativeness collapse @@ -96,16 +104,12 @@ Attack path:: . Construct the candidate forgetful functor `EchoLinear → EchoEpistemic`. . Attempt to derive `knowledge-preservation` along it. -Retraction:: -If the derivation goes through, the "five axes" claim weakens to -four or fewer, and the integration argument weakens -correspondingly. - -Refined target (after gate-3's RoleGraded landing):: -A sharper version: with `RoleGraded` in place, ask whether the -role-or-grade axis is derivable from the other plus a forgetful -functor. If yes, the cross-decoration integration construction -is also weakened. +Interpretation:: +A derivation would clarify the relationship between the specified +interfaces. The five-axis simultaneous-integration distinctness route +has already been removed from Gate 1 by EI-2; this test does not +reopen it. The analogous role/grade comparison is likewise a separate +interface question, not a new Gate 1 verdict. === Q1.4 — Additional axes @@ -679,9 +683,11 @@ Documentation cascade (applied as of integration commit):: * `README.md` — integration-bridge bullet updated. Why PATH B (partial formalisation accepted as sufficient):: -The full 2D iff theorem is not formalisable in safe Agda without -postulates (decidable equality on decoration types, F-collapses -axioms, extensionality on cell actions). `RecipeTheorem.agda` +The full generic 2D iff theorem was not formalised. The attempted +route would require additional assumptions (decidable equality on +decoration types, F-collapses axioms, extensionality on cell actions); +this is not a proof that every safe formulation is impossible. +`RecipeTheorem.agda` proves the per-axis halves; `RecipeNonTriviality.agda` proves the concrete construction-by-construction halves. Together with the seven data points and the structural argument from diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index f136d1d..6916997 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -130,8 +130,10 @@ later by the WIRED `+EchoVariance.agda+`* (#243, 2026-06-20 — in (`+no-bare-recovery+` via `+no-section-of-collapsing-map+` is the obstruction; sharpens `+R-2026-05-18+` from "`graded comonad withdrawn`" to "`decided against`"). Cite the WIRED `+EchoVariance+` for the -verdict; the orphaned `+experimental/echo-additive/+` track is the -retired earlier attempt. See +verdict; the `+experimental/echo-additive/+` track is the earlier +attempt, still outside the shipped closure. The current workflow invokes +its own aggregate in both Agda jobs; it is not a separately named job. +See `+PROOF-STATUS.adoc+` for the current coverage and verification limits. See `+docs/echo-types/variance-resolution.adoc+`. Build on the wired `+Echo+` / `+EchoResidue+`, `+EchoVariance+`, `+EchoGradedComonad+` (coassoc/counit), the composition isos, and `+DyadicEchoBridge+`. diff --git a/docs/proof-witness-audit.adoc b/docs/proof-witness-audit.adoc new file mode 100644 index 0000000..d8368b3 --- /dev/null +++ b/docs/proof-witness-audit.adoc @@ -0,0 +1,64 @@ +// SPDX-License-Identifier: MPL-2.0 += Proof-witness audit: Echo Types and Mathesis + +Audit date: 2026-11-01. Echo Types source base: +`b0982c44f36133acd2d0e1d4e03cf031fff7a470` (working tree also has +uncommitted CI/documentation edits). This is a source and receipt inspection, +not a new theorem-checking receipt. No proof was translated or rewritten. + +== Policy and scope + +Mathesis `estate-mathematical-architecture` distinguishes a locally +checked Agda result (Grade 3), a witness in one alternative foundational +system (Grade 2i), translations in two distinct foundational families +(Grade 2ii), and checking translated witnesses through the specified +headless checker APIs (Grade 1). Agda, Lean and Rocq all belong to the DTT +family; Lean plus Rocq alone is not foundational diversity for Grade 2ii. +Grades attach to specific results and evidence, not entire repositories. +The original repositories own their proofs. Missing evidence remains missing. + +== Findings + +* This checkout contains no `.lean` or `.v` files. A filesystem search + does not rule out witnesses in other repositories. +* Candidate Rocq/Coq witness: ephapax + https://github.com/hyperpolymath/ephapax/blob/800030f3c92536cce57acb5e82da6cf27b942826/formal/Echo.v[`formal/Echo.v`] + declares `no_section_collapse_to_residue` and describes it as a mirror + of `proofs/agda/EchoResidue.agda`'s `no-section-collapse-to-residue`. + Both source statements concern nonexistence of a section after the + concrete Boolean collapse. The source also contains `weaken`, + `weaken_collapses_distinction`, `affine_canonical`, `mode_le_prop`, and + `degrade_mode_comp`. This is a candidate *single-system translation*, + not independent corroboration or a checked cross-language equivalence. + The source claims zero axioms and K-freedom; this audit did not run + `Print Assumptions` for these specific theorems and cannot certify that + claim from source inspection alone. +* Ephapax's `_CoqProject` at that revision includes `Echo.v`, but its + https://github.com/hyperpolymath/ephapax/actions/runs/40435929887[successful + workflow run] at the same revision skipped the actual Coq build job. + Its green aggregate is therefore not a compilation receipt. The + workflow's `Print Assumptions` step names four other preservation + theorems, not the Echo witness above. No coq-lsp REST API receipt + for this witness was located in this inspection. +* Eclexia + https://github.com/hyperpolymath/eclexia/blob/742cc99cca37f1bda84d8d9188cb4f61fff4341e/formal/coq/src/EchoThermo.v[`EchoThermo.v`] + contains a discrete thermodynamic model and explicitly claims to mirror + `EchoThermodynamics`; its scope excludes the real-valued energy scaling. + Treat this as an adjacent candidate correspondence, not automatically + the same theorem or a verified translation. No theorem-specific build, + assumptions, or checker-API receipt was examined for it. +* `docs/bridges/tropical-correspondence.adoc` describes Lean and Isabelle + neighbours, but explicitly notes different carriers, no shared definition + module and no cross-prover checker. Similar names or informal analogy + alone do not establish witness identity or a grade. + +== Disposition + +No Grade 1, Grade 2ii, or verified Grade 2i receipt is established by this +inspection. The ephapax source is a concrete Grade 2i *candidate*; its +translation correspondence, exact source commits, theorem assumptions and +successful checker receipt need review before recording a grade. Agda was unavailable when this witness audit was performed. A subsequent +local cold check is recorded in `PROOF-STATUS.adoc`; it does not by itself +prove a cross-language correspondence or provide a clean-commit receipt. In particular, these candidates do not cover the experimental +or bit-narrowing modules merely by existing elsewhere. Do not infer any +regression solely from an absent receipt. diff --git a/docs/receipts/agda-local-2026-11-01-sources.sha256 b/docs/receipts/agda-local-2026-11-01-sources.sha256 new file mode 100644 index 0000000..11ad442 --- /dev/null +++ b/docs/receipts/agda-local-2026-11-01-sources.sha256 @@ -0,0 +1,137 @@ +885cc7e3b6d9b9c56cec6c8ae687691eb34d5d7c8173a7d00af09f4669cd57eb proofs/agda/All.agda +c89bff3904801c3baa6c462a1ac4bc824fd88190a6e667b1f70bdd38d0e4b121 proofs/agda/AntiEcho.agda +5c007bcd5aa0bf34f42b824b3bdc78bf05b945bec54508e5ef300df1cd910ba2 proofs/agda/AntiEchoTropical.agda +e3759575ac76b6f1db2ede784bfa54df563e2501cd6ac9d0e5993ee9c4214f0b proofs/agda/AntiEchoTropicalGeneric.agda +652511ac4c8a5960e895e6e8596d8f52bff9605d6a95c15f47e422e0d6aa47cf proofs/agda/Dyadic.agda +6759cb47a5363391b3ed52910b0e4f0715ad17db9535b6e49b6ca269b2767e8b proofs/agda/DyadicEchoBridge.agda +a2f4f767af325f462329739a890274b151b487ef731be2ac859c69476bce47c5 proofs/agda/Echo.agda +695ed7c9a283d75db01b52e8436f1991baf37e93da16f31c85ded0d0078a4dd5 proofs/agda/Echo/Index/ThinPoset.agda +9d866db5c0370c901d8e3fac2e371d6f0d5ca997372bfc29d63065cf4767a70c proofs/agda/Echo/Measure/Examples.agda +6ad906f6f39c36282423cf7466990bdab1092356f584cd303a85727bc0489de5 proofs/agda/Echo/Measure/Interface.agda +4442eb4dd90da710981b0d4349b54a4792be137c720243ba81b2db990a0d1e6d proofs/agda/Echo/Modality/Core.agda +0010b589648862c05ee715bb2781f06863a0d313717d663f83c577fa192ae776 proofs/agda/Echo/Modality/Interface.agda +210f501927fa891639cb7259fdf630760525853a96f31cab8a29f49c6195edc1 proofs/agda/Echo/Separation/NotResourceInstance.agda +3d52cf86fbbf8b70b66d6af35936d9d28b925c3fd4e209ca1d7fac84a4f47a90 proofs/agda/EchoAbstractionBarrier.agda +240a43393b736ec9e3ed6a691af924e8759153a655212868b86b786225707639 proofs/agda/EchoAccess.agda +469b0966801870b71cc6a9cc4584b96c68b2cb5a31be8a3413826cac58c1103a proofs/agda/EchoAggregation.agda +f7cf6ec7d5f8e9445495f9291634912b9364b2ee2a5b7a39466e5e3771c0e5a5 proofs/agda/EchoApprox.agda +a23c769f3d4345db79a259019dc1c4bd6ceab909b983c4974e2890d962750e60 proofs/agda/EchoApproxInstance.agda +46f56be66ccf1f680641e22d8595c441aeaed903d2dd6f4a13df7fd3f6de5a9d proofs/agda/EchoBitNarrowingNumeric.agda +9c9b07d4f596ee7fe808419ac93d6712574de9eec9a9bcd169a0c110a3710e6c proofs/agda/EchoCNOBridge.agda +d3721efa1bc1d24be33b5cefa187224188283b70579e55549d262fa5d9f8c428 proofs/agda/EchoCanonicalIdentitySuite.agda +b18fcfd4a0eaf579c09563a2312f15e607a9c4c7f6f359f84ff63b0be20e0f0a proofs/agda/EchoCategorical.agda +20009f709cb4bc6fe16125e4bda62c35d79230536b5e5ddfa7444988ae2c3e2d proofs/agda/EchoCharacteristic.agda +510308dcf242b09aeb033cc6d00e158961756bcec71f5ca98a9616a86b408a79 proofs/agda/EchoChoreo.agda +233b45cc0a8f884ec31a6f665f37783f874bef885340dc1901ecfd1cfced4fc8 proofs/agda/EchoCost.agda +1369802200dbf064be4fc5a50e39fccb2ed58ba12046a3922a14ab98824929ed proofs/agda/EchoCostInstance.agda +11209741c3518652094bc9cd004e46ba3994dd482873b712c024e096ac6d2c77 proofs/agda/EchoDecidable.agda +4c571e208eab837d234d1d084c6cec7bf6dce2372fc9b1a7afbbc7286df81892 proofs/agda/EchoDecorationBridge.agda +72367d07f74a2c6f58df5bb4b869b3bcccb7df68574f18e0996c21e9c27d9f2b proofs/agda/EchoDecorationStructure.agda +bf5a0fc94f07df9a68f6848ab1ae71d43ed801075b51cfbdaa66fa767436d591 proofs/agda/EchoDeniability.agda +3e2b064248225235efd614041059687452f813fb89f7e1feb4fd7548aeecabf4 proofs/agda/EchoDifferential.agda +cfb72e2a33c5c44c5047d156ac69d3160f5ca61ce168db6cf925326daba10104 proofs/agda/EchoDisplayed.agda +6c0a17487c5afbdc0e840e1b2ef9c176ec8a54de68ad31fe0ae78d61be8d69c1 proofs/agda/EchoEntropy.agda +9a7e18925a783c31b15820435db3114127baf34e0dd9c0c64351a34cb1b4fccf proofs/agda/EchoEphapaxBridge.agda +8deea1087ebd00fb38e52cff2ab5ca8984c8cec53743fa82f3ec58dd60ede144 proofs/agda/EchoEpistemic.agda +26fd6cdb69b169a5ce244cc11ab28ff7ceba527b06d00786b1959eee8a68fa16 proofs/agda/EchoEpistemicResidue.agda +22366519de1ba707b1e4c2c8945159e13426b6e1809a6312f92d520032f150f6 proofs/agda/EchoExampleAbsInt.agda +6b3b8da29de140298d7ddd83b4a088d58d38dec25446225489bbf96d1e3dd81d proofs/agda/EchoExampleBitNarrowing.agda +ad7369b6f780b36a9d4efbf4df4322e524995063c317339754ebe6aa246eb318 proofs/agda/EchoExampleParser.agda +ec824eec8a2802b3dc4390e89d0150226d18fbd87afdbd4d1301db70e0e9b0f1 proofs/agda/EchoExampleProvenance.agda +08007b0a0ab1058d41402ddb375af4626d58640d7ed7cadde14137a4e6859f02 proofs/agda/EchoExampleSignAnalysis.agda +1900ff583823fdf359a37193a2b7425e930821863062e032e05b170b2a30ae10 proofs/agda/EchoExampleTruncation.agda +44f8d529757dc87f58e6c6885ed59d3fa72679a0ed0a2ce7d1ddee1226aadf6a proofs/agda/EchoExamples.agda +755bfdae4c3828f144a9906425e47efc62fbd6c4e333eaf7d71b41fd6045d0e3 proofs/agda/EchoFiberBridge.agda +46908dd3b1c21df579d19624146f57b1cde6f21347aadde500caabd001330503 proofs/agda/EchoFiberCount.agda +a6f9e138ced4dab8a734d0128727a9037d1ca13fdca98073a7f938ec5008f593 proofs/agda/EchoFiberTriangulation.agda +758731e3b80b93e6f6cc296409973005f19c9a91da62dcd490bbb2a28c8d1978 proofs/agda/EchoFidelity.agda +cbc82a8aed7b6f942db188df695f194e87be83e24e30cb1dd5b715c2ba7ddd8f proofs/agda/EchoGraded.agda +a6abbe9f58a5761d9d1600d63ad8710f2f90cf515e6581d459c6f729d350dc57 proofs/agda/EchoGradedComonad.agda +3e11360bc845e16be4dcd4cccd68669b59edac396ba5da17ab030cedf455e8fb proofs/agda/EchoGradedComonadF1.agda +16eedb7f4ef684d10df5b47d125dd43379733307778d4f4cc13bd62ebf194bf4 proofs/agda/EchoGradedComonadInstance1.agda +e70c0e9e34c693ebfb8107e653414060c52d56a0229bafd9cbd8cec813e2b710 proofs/agda/EchoGradedComonadInstance2.agda +741a1af82e224388098cb6b5e1ba212cf0a922c3c771a03f2d214c7c137a3dcf proofs/agda/EchoGradedComonadInterface.agda +36b26834d04bec7edc2cfbc283f76d50739ad289a3be9e3e39824950d8250dec proofs/agda/EchoHaplotypeCollapsing.agda +771fbef1edab2fe4a4d2310536102e06c480ff6db5597aadfe0f8563acb2b2fb proofs/agda/EchoImageFactorization.agda +ef30eb4ee184d8cb87de1eaa37457c2b520c224730b6bdd2d318a58460143319 proofs/agda/EchoImageFactorizationProp.agda +20f77384844fcf4e73e41877caa3e0742f4a9d3121ac91806c3141fbe793f6bf proofs/agda/EchoImageFactorizationPropCubical.agda +fc7526a59b28c57eda3543bdcfc7d76fc02f58b6b23580ef5a79af75c1eff4b6 proofs/agda/EchoImageFactorizationPropPostulated.agda +7a18619cefcebe55c36019329ca70c6eaa9c181f2cc564eaf3a37460a56a5da5 proofs/agda/EchoIndexed.agda +61d069a17113798bc4a735ac77ec0e006884b6825a6469ed94c85d1c9ae5e1c7 proofs/agda/EchoIntegration.agda +a30ce11a2266784bd048a5a921167c10549d1ebaef021232a1d7657e49e4f141 proofs/agda/EchoJanusBridge.agda +a8e6fc1d64ca476d235bd95e8430943f1b28a767886a6028b8e2fd0dac66d01a proofs/agda/EchoKernel.agda +219e5d7ee292b9e887c098a8d7fcecea97de162572d64b29a01f3d90c3068cfc proofs/agda/EchoLLEncoding.agda +7bacf8e414342f8416aa9fb772fb29d7d154a6f767d508de5cd730c0b8393938 proofs/agda/EchoLinear.agda +6bcbc110a3b7f142a0b237c10e9f15fe82b9ce6f2508d8ec154fbbb062d2a7b0 proofs/agda/EchoLossTaxonomy.agda +a92d77a66536d54a636a5cda5a87ede2640c29fda71ff610d24f92746d81481b proofs/agda/EchoNoSectionGeneric.agda +7fe2f8c6a8c426a2ec211c9097a04c75676bcee73fc5293653b8b393d2ebef3f proofs/agda/EchoOFSUnivF5.agda +2ac4bbe6bfd7fb37b8c887780037c0afc267599577b0e60e5ef5393a9d27ebff proofs/agda/EchoOFSUnivF5Diag.agda +5d30993e304f79651d28e4e36b3da062faf77286b9724256470b230b22ff1ff7 proofs/agda/EchoOFSUnivF5Iso.agda +d17f18d19c0d3db6b17d6005685143e296522ec9000b38a58ee8d9f2a16f6ba2 proofs/agda/EchoObservationalEquivalence.agda +3d9115914e79ee80eb1f8daddb7e71d79ad10cbdff2cda49811c059ce8597299 proofs/agda/EchoOrdinal.agda +6698d792ef33bf6ec47d6d5e057faf093d7f6acc3986938ac4790469731c194f proofs/agda/EchoOrthogonalFactorizationSystem.agda +18360a2c2271e1e943524f03ddb0771f71c5e6962508e9cc88f145779a77faa8 proofs/agda/EchoProbabilisticSupport.agda +37110ab8eed0ae2e6b847728262393dda84b3a0b1c684f80fc2099d85bdc477d proofs/agda/EchoProvenance.agda +850374cfd27157be3b9ccd3b1bc7f82fa776846836dd23a0b76fb8865d96e200 proofs/agda/EchoPullback.agda +f064f3fb328cb047674e2cfae52714649f4aee60786d7d54e96693289074be1f proofs/agda/EchoPullbackUnivF4.agda +bbf8584e0b84fdd56f13e9cb089498c699568fb22ef08f6b347b87f46cb7b5a9 proofs/agda/EchoRelModel.agda +1a3367099b69190a52ba91c675ffb2ec2ecd4f7d3d1c436316ec155e03fe23c8 proofs/agda/EchoRelational.agda +a3ee434b4326826ae1b3f7eb8bfd1635835041c5f3dd00fbcfc2955dbdef0c38 proofs/agda/EchoResidue.agda +247863bf07b3ff7c552551008dd801549343cd23d4709ec4c22f8ffe6436ad2a proofs/agda/EchoResidueCell.agda +ddc34d19f3cfe481a01e6ff6d02a8c3d4cb5fc214f39dee4f7d8c6dfeb0779e5 proofs/agda/EchoResidueTaxonomy.agda +710d209a7620f2dc752ec87d1de754088eda0a971d0ccc35687f4696c1392ce2 proofs/agda/EchoReversibilityBridge.agda +e009bf0b6274c5e6ea634189345ba9910210d9e95d7f38056aa730bdec92d1d1 proofs/agda/EchoScope.agda +6caf6e112ec0189539f5e91f9b9611d75a3d66517b2541cbc2e5eae1ca61fc2e proofs/agda/EchoSearch.agda +b73a9bb1fab531531f2442ea5f23cda74bd933e6e80e12e84986aa8ef716be33 proofs/agda/EchoSearchExample.agda +b53047cd1a66c864971a51be85b1b73760237bd35ca7f5f3eebe51e023dce7b9 proofs/agda/EchoSearchInstance.agda +09df9f53a719db6b69a31de0c227d90b913569fb3f671d636eabf7e05f59a7b3 proofs/agda/EchoSecurity.agda +57ffa504df57249feaf780c76e93cec430b4f3f98f0971b43d7271af5434b1dd proofs/agda/EchoSelectiveProjection.agda +922ca584f8e86d7e7c55fc253680f939212e4e351455999bead79f7af22ff5dd proofs/agda/EchoSeparating.agda +dcb524a97a4c139a7ecd1daf8b4572271851cca386121a12d885aabb5d8728be proofs/agda/EchoStabilityTests.agda +d68f3b396139e3e7435e5c64c9767c8ac695c2a26a3f24e8575373b0397b66dc proofs/agda/EchoStepNDModelF2.agda +ba1d4e5dbc1b6e5f40e6e10546143aa5af09f69ca1ab368c5a7601419c3f731e proofs/agda/EchoThermoCollapseImpossible.agda +1f283fbd545b1c0bc6110c8da41f574277220680e33bd5957a06e0eac4f50c96 proofs/agda/EchoThermodynamics.agda +38b769a7e42aafd778662118e77ae7dff0817509d5570e114366fd537a580c4a proofs/agda/EchoThermodynamicsArbitrary.agda +e377c7a672a823d9b7a4583b3c7f3a40f86e841ef427602801b0a58adf7cf50f proofs/agda/EchoThermodynamicsFinite.agda +119813085029e4bc80cb1a510d77aece558daa0bf65b5fcf327503b0a414cbfb proofs/agda/EchoTotalCompletion.agda +6f99ea70b0a3864d0a8250aabe16197481a0df4b8ffb1038a672d9feaf0d647c proofs/agda/EchoTransaction.agda +f47cb3185f214bfc5085e28fb62248cb33072dbd438c1ddba6f521e7a3d7c643 proofs/agda/EchoTropical.agda +28d0e1735cfdc6a450e0166c78f3bff32d1e6ab323dce4d31280db6835c79c38 proofs/agda/EchoTruncation.agda +d836dc04c3dbfae94874fce564a92b25390f7d737a24179917863693b7e825cc proofs/agda/EchoVariance.agda +424a7750261fc2283332acf0ed7251e99b62a302c6129a39018e399fb814cb8c proofs/agda/MinimalCNO.agda +e5972baa5b4809baebdd7f0eb4a7b4a098a6281066c475095469a21f2719d030 proofs/agda/NarrowingSmoke.agda +1e88cd46f23e14a85c10b5feaf200bbc5ab6b181097a093b9a2af1bc3e595f96 proofs/agda/Ordinal/Buchholz/Syntax.agda +e8adb2bb9c8c83a7ecbc71615b6616827201c5ea59a3cca4018a1119ccd82214 proofs/agda/Ordinal/OmegaMarkers.agda +608b8def844c5b66edcec4333be68d00696af7960b60490b3f1fb026dbcde96b proofs/agda/SimpleTest.agda +c7e670f9f0eb6452e2b3d5a413deebe1615db6da1f9e80ffb5eac063c420babe proofs/agda/Smoke.agda +ae969a48cf41c308e320b0a9b41531abf967f8e1c4f0bc6393a86a95f8e76cf4 proofs/agda/VecRotation.agda +8ad61854a72fcb3103d9bbec632835f20fc29a3a777b33f895bb4b6e2e027e3f proofs/agda/WorkingCNO.agda +5f3cf5564d712b10865df6f1e14343a9d69fea7cc2bd8639d08479813eb615ed proofs/agda/characteristic/All.agda +cf8c3687d32eb21109c66b30bba800b93460bce4e962554c660d4a736b5650e9 proofs/agda/characteristic/ChoreoInjective.agda +fab877c509885101609cff24fdfa1b66d75dff7885cffa3a6a4cef3375413c6f proofs/agda/characteristic/IntegrationAudit.agda +d59116cee9a88afaf2cc327220ddc5a1a51d51079a1e303659cbc9afb237a96e proofs/agda/characteristic/InteractionTest.agda +d2bf40f935272f02c74d7356653e0249bbe28cd7e5a33521b84a9796dbdea972 proofs/agda/characteristic/ModeGraded.agda +5feb850e9948e16b39f78affa52df434429105c62165122b18ffc90ad87242d2 proofs/agda/characteristic/N5Falsifier.agda +83052e53c1f0d1a30956ba74687cc23ff8cd1192bd81a7246be382103eb26a24 proofs/agda/characteristic/NonTruncatable.agda +233de144ba45c4ec48c094d0b4fb63cac2f0977ef94102971f9688bddf498697 proofs/agda/characteristic/RecipeNonTriviality.agda +6b575f81f56fcbe91025484f8186532c29ae56f5784725fa85b89b99e204432e proofs/agda/characteristic/RecipeSpec.agda +5d2bb23e27098487798aa098d7612485fa3ab3f55af6728777af49e7a83dfbbc proofs/agda/characteristic/RecipeTheorem.agda +a9f5f15d579865e2eb7079f6a784db8d00e80c20ada35c03191d5ba68d989c72 proofs/agda/characteristic/RoleGraded.agda +f5ebb0f3c1998cd786bd27690d2bff1b1f1b9d5b4a96d8305f2619d58053d7c2 proofs/agda/characteristic/RoleMode.agda +f86659403d7d32eb6725268500ca41c8534ea94e279718e39e066fcc590228c7 proofs/agda/characteristic/RoleModeGrade.agda +2108d5767315ec02b2e9e899df078dec76f65e0e22e6fc5925205978ebd6e747 proofs/agda/characteristic/RoleRole.agda +b430cb68a2a985db9035e0adfc8a9c08635894c4a01102277f2789458b2f9dd5 proofs/agda/characteristic/VisibleConstraintAudit.agda +af66e1db0382728c60992c4d47d1bf45260d8327f357b25b691e5162b8d8335d proofs/agda/examples/All.agda +227f0c29a703b7589d44452f53193fc6ddb2a7685946d95dca79171ac419d6a9 proofs/agda/examples/EchoVsSigma.agda +73926a9d02beb115065fd95df3ecb031a50e3dda54910064df957e529145f0df proofs/agda/examples/EpistemicUpdate.agda +0171680823dcd5bd28035cd262ec8956fe710393959ce0185b2d9ace004340a0 proofs/agda/examples/LinearErasure.agda +2ec39909dd798b3d4eb404be41545c54aacf877b904b65effa6071715844f969 proofs/agda/examples/Transport.agda +2f7bafb00d0bb0729c5cfcba23d60a79520ae8e13be99c62048f8518d48e116c proofs/agda/examples/TropicalArgmin.agda +df775a084b7eaf4e03b9cb76e401363204b7b8cbc445cb571a8b98befe51a9d8 proofs/agda/experimental/echo-additive/All.agda +c0e924e15cbf87c3ebd8922163f5e81cc1b36bf77e8d7f2e0c4d0e8876daf67d proofs/agda/experimental/echo-additive/Grade.agda +40f8b0f52f16ea48a9a5e5e4e38c70539a3b0f72f84f2b282dac2881ac095ea4 proofs/agda/experimental/echo-additive/GradedAdjunction.agda +6d1d5962525e4488f59d2cbeb21fde91344275be9f012f17432813400893afcf proofs/agda/experimental/echo-additive/GradedCarrier.agda +80122cbde4b5e7d8e3fbf972a6b3bb5532b3eee55fea0f416a362b26f52f7e68 proofs/agda/experimental/echo-additive/GradedCarrierFaithful.agda +6a68bef96d4234b4e14dbf405aef0c2b2eec9e873091401e739f034f69541793 proofs/agda/experimental/echo-additive/GradedComonad.agda +d4bc0e976c004ec73860e1271c6c342fa58249631292e3bb357cc618f8be36b7 proofs/agda/experimental/echo-additive/GradedMonad.agda +752dc6f79c57bf7fd0a08c9cd29b2ca80dbc0ca9ada2d59ef7a13a610a657a95 proofs/agda/experimental/echo-additive/VarianceGate.agda diff --git a/docs/receipts/agda-local-2026-11-01.log.gz b/docs/receipts/agda-local-2026-11-01.log.gz new file mode 100644 index 0000000..fe40573 Binary files /dev/null and b/docs/receipts/agda-local-2026-11-01.log.gz differ diff --git a/docs/receipts/agda-mutant-grade-2026-11-01.log.gz b/docs/receipts/agda-mutant-grade-2026-11-01.log.gz new file mode 100644 index 0000000..33c53cc Binary files /dev/null and b/docs/receipts/agda-mutant-grade-2026-11-01.log.gz differ diff --git a/docs/receipts/agda-mutant-grade-main-2026-11-01.log.gz b/docs/receipts/agda-mutant-grade-main-2026-11-01.log.gz new file mode 100644 index 0000000..640d27f Binary files /dev/null and b/docs/receipts/agda-mutant-grade-main-2026-11-01.log.gz differ diff --git a/docs/receipts/agda-mutant-narrow-2026-11-01.log.gz b/docs/receipts/agda-mutant-narrow-2026-11-01.log.gz new file mode 100644 index 0000000..e8b9a18 Binary files /dev/null and b/docs/receipts/agda-mutant-narrow-2026-11-01.log.gz differ diff --git a/docs/receipts/epistemic-current-local-2026-11-01.log.gz b/docs/receipts/epistemic-current-local-2026-11-01.log.gz new file mode 100644 index 0000000..8306b73 Binary files /dev/null and b/docs/receipts/epistemic-current-local-2026-11-01.log.gz differ diff --git a/docs/receipts/epistemic-pinned-local-2026-11-01.log.gz b/docs/receipts/epistemic-pinned-local-2026-11-01.log.gz new file mode 100644 index 0000000..3b31660 Binary files /dev/null and b/docs/receipts/epistemic-pinned-local-2026-11-01.log.gz differ diff --git a/docs/roadmap-gates.adoc b/docs/roadmap-gates.adoc index 1ff442f..f639957 100644 --- a/docs/roadmap-gates.adoc +++ b/docs/roadmap-gates.adoc @@ -36,13 +36,15 @@ falsifiable, not a failure of the repository. [#gate-1] === Gate 1 — Distinct phenomenon -Echo is not a renaming of an existing construction (quotient, Galois -connection, lens/optic, refinement type, modal/comonadic type, -provenance semiring). *Pass:* a distinctness witness that survives -reduction attempts to each neighbour. *Retract:* a neighbour -construction expresses the characteristic family without importing -echo-specific primitives. Living instances: `docs/next-questions.adoc` -Gate 1; `docs/adjacency/*`. +Bare Echo is definitionally the fibre, so novelty of the construction +is not claimed. The narrowed comparison concerns what specified +propositional or single-witness neighbours retain, and the quotient / +Galois 2-cell constructions. EI-2 terminated the proposed simultaneous +cross-axis integration distinctness argument negatively via PATH B; an +encoding of that recipe is a separate neighbour comparison, not a +standalone pass/fail test for these remaining arguments. Living scope: +`PROOF-STATUS.adoc` § Identity and adjacency, +`docs/next-questions.adoc` Gate 1, and `docs/adjacency/*`. [#gate-2] === Gate 2 — Characteristic theorems diff --git a/roadmap-gates.adoc b/roadmap-gates.adoc index 1e9de3a..3b204cd 100644 --- a/roadmap-gates.adoc +++ b/roadmap-gates.adoc @@ -48,9 +48,10 @@ toc::[] .Claim **** -Echo types name structured loss under non-injective computation as a -phenomenon distinct from existing treatments — refinement types, -lens/optic theory, HoTT fibers, setoid quotients, provenance semirings. +Echo names a proof-relevant fibre reading of structured loss under +non-injective computation. The fibre is not novel and coincides with +HoTT fibres and Σ-relevant refinement; comparisons with other treatments +are specific to the models and witness information they retain. Distinctness rests on two structural arguments: the *truncation argument* (echo types are non-truncatable for non-injective diff --git a/roadmap.adoc b/roadmap.adoc index 6d08339..87526c7 100644 --- a/roadmap.adoc +++ b/roadmap.adoc @@ -83,8 +83,14 @@ narrowing history and `roadmap-gates.adoc` for the test discipline. | Positive examples landed (`EchoExample*.agda`); matched-negative companions planned (Track C, Lane 2). |=== -No gate is currently FAILED. No gate is currently STABLE-ESTABLISHED; -re-assessment cadence is per tagged release. +EI-2's proposed simultaneous cross-axis integration route was +*closed negatively*, and Gate 1 narrowed; it is not an open route or +an unqualified Gate 1 pass. The Gate 2 row reports the historical +nominee-protocol pass, whereas README criterion 2 asks the stronger +question whether the family suffices for positive identity beyond +standard fibre lemmas and remains unestablished. No overall positive +identity is claimed; re-assessment cadence is per tagged release. +See `PROOF-STATUS.adoc` § Identity and adjacency. [NOTE] .Canonical identity layer (2026-05-27 advance) diff --git a/scripts/check-agda-invocations.py b/scripts/check-agda-invocations.py new file mode 100644 index 0000000..a694301 --- /dev/null +++ b/scripts/check-agda-invocations.py @@ -0,0 +1,42 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: MPL-2.0 +"""Check direct Agda proof commands in the maintained CI/local entrypoints. + +Static policy lint only: not an Agda typecheck or a parser for arbitrary shell. +The separately reviewed full-cubical profile is not implied by this check. +""" +import re +import sys +from pathlib import Path + +DEFAULTS = [".github/workflows/agda.yml", "scripts/check-grade3.sh", "scripts/verify.sh", "Justfile"] +PROFILE = {"--safe", "--without-K", "--cubical-compatible"} +CUBICAL = "proofs/agda/EchoImageFactorizationPropCubical.agda" +DENIED = {"--allow-unsolved-metas", "--with-K", "--no-without-K", "--type-in-type", "--no-termination-check", "--no-positivity-check"} +pattern = re.compile(r"^\s*(?:run:\s*)?agda\s+(.*)$") +failed = False +for filename in sys.argv[1:] or DEFAULTS: + path = Path(filename) + count = 0 + for line_no, line in enumerate(path.read_text().splitlines(), 1): + match = pattern.match(line) + if not match: + continue + args = set(match.group(1).split()) + if args == {"--version"}: + continue + count += 1 + required = {"--safe", "--cubical"} if CUBICAL in args else PROFILE + forbidden = args & DENIED + if CUBICAL not in args and "--cubical" in args: + forbidden.add("--cubical") + missing = required - args + if missing or forbidden: + print(f"{filename}:{line_no}: missing {sorted(missing)}, forbidden {sorted(forbidden)}", file=sys.stderr) + failed = True + if not count: + print(f"{filename}: no direct Agda proof command found", file=sys.stderr) + failed = True +if failed: + sys.exit(1) +print("Agda invocation lint: OK (static only; no proof was checked)") diff --git a/scripts/check-experimental-aggregate.sh b/scripts/check-experimental-aggregate.sh new file mode 100644 index 0000000..3e31f2d --- /dev/null +++ b/scripts/check-experimental-aggregate.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Every direct echo-additive source must be imported by the CI entrypoint. +# This checks wiring only; it is not a substitute for Agda typechecking. +set -euo pipefail +root="${1:-proofs/agda/experimental/echo-additive}" +aggregate="$root/All.agda" +test -f "$aggregate" || { echo "Missing $aggregate" >&2; exit 1; } +fail=0 +while IFS= read -r -d '' file; do + name="${file##*/}" + name="${name%.agda}" + [ "$name" = All ] && continue + if ! grep -Eq "^[[:space:]]*(open[[:space:]]+)?import[[:space:]]+experimental[.]echo-additive[.]${name}([[:space:];(]|$)" "$aggregate"; then + echo "Missing aggregate import: $name" >&2 + fail=1 + fi +done < <(find "$root" -maxdepth 1 -type f -name '*.agda' -print0) +if [ "$fail" -ne 0 ]; then exit 1; fi +echo 'Experimental aggregate wiring: OK (not a typecheck)' diff --git a/scripts/check-grade3.sh b/scripts/check-grade3.sh new file mode 100644 index 0000000..733a301 --- /dev/null +++ b/scripts/check-grade3.sh @@ -0,0 +1,40 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Local, uncached Agda checks for the CI roots and the narrowing exhibit. +# Run from any directory after registering the standard-library and +# absolute-zero libraries. Save stdout AND stderr if a receipt is needed. +# Successful checks apply only to the source and dependencies actually used; +# this script does not assign repository-wide Mathesis grades. +set -euo pipefail +cd "$(dirname "$0")/.." + +command -v agda >/dev/null || { echo 'ERROR: agda is not installed' >&2; exit 1; } +printf 'Source commit: '; git rev-parse HEAD +printf 'Working tree status (empty means clean):\n'; git status --short +printf 'Agda: '; agda --version +printf 'Library configuration (verify paths and revisions separately):\n' +for f in "${AGDA_DIR:-$HOME/.agda}/libraries" "${AGDA_DIR:-$HOME/.agda}/defaults"; do + if [ -f "$f" ]; then printf '%s:\n' "$f"; cat "$f"; else printf '%s: absent\n' "$f"; fi +done + +sh scripts/kernel-guard.sh +python3 scripts/check-agda-invocations.py +bash scripts/check-experimental-aggregate.sh +bash tools/check-guardrails.sh proofs/agda + +# Typecheck the given Agda entrypoint without cached interfaces using the +# standard profile. A failed check stops the script. +check() { + printf '\nChecking %s\n' "$1" + agda --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda "$1" +} +check proofs/agda/All.agda +check proofs/agda/Smoke.agda +check proofs/agda/characteristic/All.agda +check proofs/agda/examples/All.agda +check proofs/agda/experimental/echo-additive/All.agda +check proofs/agda/NarrowingSmoke.agda +# Cubical is a distinct --safe island: its source options govern its profile. +printf '\nChecking cubical island\n' +agda --ignore-interfaces --safe --cubical -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda +printf '\nAll requested checks exited successfully. Record dependency revisions and output before claiming a receipt.\n' diff --git a/scripts/verify.sh b/scripts/verify.sh index 6e0ba82..e8b4c1b 100644 --- a/scripts/verify.sh +++ b/scripts/verify.sh @@ -9,7 +9,7 @@ echo "1. Checking no unsafe constructs..." sh scripts/check-no-unsafe.sh echo "2. Building All.agda..." -agda -i proofs/agda proofs/agda/All.agda +agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/All.agda echo "3. Running just verify..." just verify