From 0bee69cbe83936072b44efc8a9087d9f3ae3cf8b Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 17:37:42 +0000 Subject: [PATCH 1/2] Reconcile identity evidence and record Agda proof checks Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/agda.yml | 38 ++-- AFFIRMATION.adoc | 3 + CLAUDE.md | 15 +- Justfile | 14 +- PROOF-STATUS.adoc | 166 +++++++++++++++++- README.adoc | 12 +- docs/EI2_REPORT.adoc | 24 +-- docs/adjacency/README.adoc | 8 +- docs/adjacency/information-flow.adoc | 29 +-- docs/adjacency/modal-type-theories.adoc | 40 +++-- docs/adjacency/provenance.adoc | 9 +- docs/adjacency/refinement-types.adoc | 20 ++- docs/bridges/cross-repo-bridge-status.adoc | 19 ++ docs/characteristic.adoc | 18 +- docs/estate-proof-followups.adoc | 63 +++++++ docs/gate-1-distinct-phenomenon.adoc | 88 +++------- docs/next-questions.adoc | 60 ++++--- docs/proof-debt.adoc | 6 +- docs/proof-witness-audit.adoc | 64 +++++++ .../agda-local-2026-11-01-sources.sha256 | 137 +++++++++++++++ docs/receipts/agda-local-2026-11-01.log.gz | Bin 0 -> 26047 bytes .../agda-mutant-grade-2026-11-01.log.gz | Bin 0 -> 5866 bytes .../agda-mutant-grade-main-2026-11-01.log.gz | Bin 0 -> 21042 bytes .../agda-mutant-narrow-2026-11-01.log.gz | Bin 0 -> 1703 bytes .../epistemic-current-local-2026-11-01.log.gz | Bin 0 -> 1586 bytes .../epistemic-pinned-local-2026-11-01.log.gz | Bin 0 -> 1590 bytes docs/roadmap-gates.adoc | 16 +- roadmap-gates.adoc | 7 +- roadmap.adoc | 10 +- scripts/check-agda-invocations.py | 42 +++++ scripts/check-experimental-aggregate.sh | 20 +++ scripts/check-grade3.sh | 38 ++++ scripts/verify.sh | 2 +- 33 files changed, 767 insertions(+), 201 deletions(-) create mode 100644 docs/estate-proof-followups.adoc create mode 100644 docs/proof-witness-audit.adoc create mode 100644 docs/receipts/agda-local-2026-11-01-sources.sha256 create mode 100644 docs/receipts/agda-local-2026-11-01.log.gz create mode 100644 docs/receipts/agda-mutant-grade-2026-11-01.log.gz create mode 100644 docs/receipts/agda-mutant-grade-main-2026-11-01.log.gz create mode 100644 docs/receipts/agda-mutant-narrow-2026-11-01.log.gz create mode 100644 docs/receipts/epistemic-current-local-2026-11-01.log.gz create mode 100644 docs/receipts/epistemic-pinned-local-2026-11-01.log.gz create mode 100644 scripts/check-agda-invocations.py create mode 100644 scripts/check-experimental-aggregate.sh create mode 100644 scripts/check-grade3.sh 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 0000000000000000000000000000000000000000..fe40573578c6f8c2b5bc92781432d4ba9e5bd957 GIT binary patch literal 26047 zcma&NV|b)ZwC~*=V`5FLiEUdG8xz~MF>xlgZQGjIwr$%vd7iz`IeYK-!+ZKeudY?= zs;+DGeOIme|L(^B0|of^1$vgTYQ6i@-S_exwf#&+Sl;B<3N$*eOuIo7b|aSq5|}_J zwK$7(Oe)cFBdMA$9r~}aH6!|00Pum7Ka&U{x?PA*yfiFdSYD*W)wYTH6ZXupsqa(n ze*SYYroe+On{+|Sg_Zb24x0sHkfv@Hv&m!J89PN~)O@RO{%=Ghhjo40?san%=lj6) zBklXo^w0yvaF$6i?=3T%E6WSIdQ8#Cq7>HG-SexTZPOQLt~jy1LprI_56%W$<{{ z=(0N7*g3jd)IQ?gw=pqPD||ZITzxzqt3Nnuz4=L<#{voC)V(CrYa~sE$SU(3vg$I^ zTF`5qd>95>`TA)|mPXwjW!A;c2nPFp$;xq)!e{CYVqhtzipHy3lMD<5dO4d#hl% zlxw)|Rr$zh8IDhB9UV*8@o-7X>N22I8@wT>WYVhH=#;9{} zSayREIV`{668Xafy(K|>i)4$cwt4HTSEi=lQ;%F*O~`X&sbHo zg%5!?`l8B*$DOFlJ`5Yh(xuO}sNO5P9kWkTyb2PqdcFnb!H6@nAXXP1zUmeVq2A2U z1NMUJ`UytdoAxQZ^rtkE)8xl9@kvj8o4y4S%{J^+=kWn4@X2ux+{#`YKC$PW&!HSi&!(RnJ5Z2Q30o@NE)7# z8HWv1mXAsOP4o_l%6^p|remL5F$WNx9~s%`Ao>^C!{6L?@<{kLxOh@rFY2PxR%!pB zC)GafI(f1Pp?D74lZxJ)*hVHDuH>zoZ@Wf(~b2_lw&N~>{ z&q;zb%^k$EslRRJI>#IkExc^h&55G&@j`K9t6fl2{Wp+gWHKh|q2LdH z8?FumHm}D^2SM5*QqJViLeiCh0?8%F>VZ?w3P;V<(7-)Y(m`Q$dHBza8YL53Cvgmg zGudA{ia6X!GV+_ue@hF6S9fN(q%}hb?UC*U?X{dF9?=Sx2BJb9xxv4c_ch5OD&K81 zU@#?36j|#2s%%A0Wi69Ya1fvEw_q@H{?q@etJ3Z&Pd)i`r z+g(Ll9Ea7^*U%SN6Cus#VjRbgNI3%457&G7^c3JDCw^^Ul_sK^FGt~fZpL$RERn!< zvNTgL&g?vK*pdrMEyG!xB3H05FrreS0NmH|M028^FW0`cAABnEwDy(Ujc#k2>GGG~ z+c(=%b9OT!Vrc`hT{nG)_bMH#{;NcR)%8e$od{9ynWLIoI{=fGbLpCl06l)Q5Z9{k zKmzY+I|7y;tzsb;3gH^%m87Oze=C=RM5(klb}9zY_etxIQ4lGBEf5tfQSV>V+iQV; zE%ffvb+|98t)#xk%;8 zh6;(tvXGe9{rO&!zZlI~z(~J(@+)w?c}?Jc!mBK6oYcC<)EU-5!IjSDy*T zplRj;UF%Uz)Z|QIW!}mHe|Z#szJmQ{T%S2onW0Q<1g{}Swe2^O+RaG%U+PqN(2@pi zSg$h+D{{J4nrchV3i~f|OnI*fT#A-Z1doCXub0(2q1zPyz2*J`{x95rOF!qc~7(nR|+nutEC^k~96t4snTqA|x}BNK^cVwUAY$wZB@Jmw({ z7?X@O5#{1zK_$q?OpOT%JVp&FoT25E@*KfGD=>Z~#;R;i>?D=~&jNTD0DWbcI7 zerCQ`^fl}DVpq;VC5*7GO@y*FO@mY|b|+>u75Hjy`kxY~O|DzEGvKe~vXGE2dP%;Q zaBWlASUui&Z$G;hnwym&5A$LrwfrEK>aCDdW`ag?(_?kfQ&zT-C{^ED7qz3(RJT6P z@Q4!W`k*;wFf->e_!CjDDSDq(k?|?7?48KT@ z9#bdI(z80m?abob-ggF323rdXf?uh+n$?L_%Gzx(jkFm~jO>$DnnUXpO3`bftu4Qw z)#)XFZUyAihE)#{G!G6H zgsdZitJZ_XrQuUaihE4AP(Le^h~GMRF(fvc5+r#6+ozK70I9$_ zdWMpJR`>`T#vEi~1syiN^^3@~$fJ#jVwxtSrS8|(pO06($)SK&0lh9{tvIRk1sDx3 zIOPm{#@$%rHy!EqPtUfL^(rKy0zFCw@l86e1 zaxc>0(^wiTwqFV{pZ6xZ7To(04ervNCnYa?h7@|GQ8s0!xBc~W6ZPT}s@26TRom=c zvMyZ%IUd9}YSzxZ8zFlnLMW~4 zG*Bm@a$lZJ3bil8?F+Y5HFOzuTRl_dgR%BB>H^lb01I2mZ~2GYZ$wh$%ogy@;nc&! ztUN>9{17MCoYB$o3YVz#1VU`Qc-~Xt>i(P_&aA@Pic46IGU+vFxm}0_uHNJ-=%-nj z@KtI}dhp9u?oKSIZZzS1{2Uo-5FM1hp_B!8 zdfC3lsOH?O2F0<=?#Q60An@72AD+DNJ0~44)AGp}K`RMW@|L#=0K4lUgg4DuVxQS= zT-dmFDDq{4NDYw|xIgU(i8PdC11Tcs`Kp(@ zu7Ip`e$wWKc*?~$;_pZ6&6)R_Q zM^YF*H%1djrN!EfLVNz4UU@vZL%!~xjK}G~3=#`=g}S=LMN4$<-5O&#=XB!tS|xfa zqc9y*au(tm#agVEl5om+tI!{K9rjNNi~Ve$$idV^$|)X4jJGa^jQ3P`ge5jj#ARA< zPn~lLs_X%64>hIS2bUOim=Cu)DI^T|Wg`ZieF@6Q2(=fb5-hKGfq8*g-Y=EY6@HC& z{bs|(tIbD_s_3ii+j1|?od_knXUpr`rGqr}t63+`buO=Q10iCf`B!kE;&GDFFhQ{R za=)%l#5wT=cYWvDkH2w5`pJ%H4qW9bxj>l0fR#=GTn-ij-j z!E@^G+;SF|m;UmbSm|_h1+sreCHE^aF-UZ8@sVaXwGMV)Nz#{F!{sst(C|02=`C3U zdNJ^VzHJX=Fk31WzB!O=&pwNCL8okIPp-X4j&-B|s zl|WF_yZ;JLwd$nbJgYaSS(^SvkrCQjVJdc;^htk<>kPsUI4tOC8N910m8S7^Xtw1X z#F1$N+Gf&J>~m~`S$0}(0n$JXXEA~^Uo+IP;dxZEW}6-URChYyx<1z1NF~G6kQN0Uub&ZzkU>5PE@H$ z-VQAvu?L(qTC}D{YM()Y`@mnJrUN8an>VL^36~?^vL+shtObpi_A%%muxwS`*YZuD zG(Z#9LpX;YbK$DL?vB{;r2-Vq`D0jqP(4sfU$}f`{<=fc$mdt)!NCS=&?%*?>0BMj z;d@%RDIh0Zyi9@_+!p^405`i1!;zo{h(p5eU-@+X7b0CP^4PP_ReM{QY!Z$Fa4<@{ z4oLHoGV_J#IY_AXs|GT+O);6_$)YOo`q*z0uWTCeMMQL;4xpU0`8N{) zFyDXE!UZUh(aTCEec+x~T-u(k%}NcQ@J4}+IO7iP7xMEwY+dXR8V@q%i%_Xp=X`sp zGvP}mrT?`wcL=1y1bCWtB{xpcxuAb%<Z*fVmN+D5de%k0YB(J5q^HaEg(0& zwMTz8LF8AEA2Vb&0M(Zg(tHZFYkIE2Ne4*YkQur|=~2K<#|ccK>+FYfeQ+9w96Gzz z#Xf2ej{(~LzBqK+^1Cq68RmZkT}QC}{pMV3NYEwV4Jv~uLKhD&jAZMsEprb1Ja3jM zx~FXP?_AOEIn?nMYPs+Lh;|BNW>2o0+{}wrUp>^ zf>#63yFt_dr(3#z)xo~Pd=Kw;{Ge$GK>i~%84dVff=K@UW+3>_uH32!C4VYWx^@0!gMWP20 zeH|@ck=EG)ONURKRn-ay=ub%kiFLugI>U*4QEY!t<01MFfyi`2GZG+z>hqVw=$m&> z)Eq1H-LJtOs?Cdb={c+!-=+GCRxCoeTikW-J878|5U9u@@%v5A@O{3qX+4!<+4v${ zbx3#`B*|1G+-Z~YK=F1%J`uQpbnxUAW%MIB{A?l?y_T2z_eAI>%<3#v-XZUwPD1yy ztAeaNgPnI9nKE_P#DIo_BxoGn=Q?*8YpxZ}RL_DY+(VfUF611g$or(#`6-K`wj*re z5>bedd>rY%zo<1(I-wkhI4WSM!$;S9zjlpVre;}Y9Cmd)-rn8S<|aCUW>>mY;aC0Tc3_OlqBFU&^(>zTh@p+36kk#)Z;2xAjni6%!MW1&-E)zC|iy zvAm5UKOUB}USe+HQhK5Iq-dx&kmkE!@L#7N5yRyj4jF%z*L32Uzn3l7r!cT;D zK^MW5TbT5s{sC7e+>fy=wC2^N$yW<^tgGM1?k`p|f*L++MD_LxKBxEPV-KM{A#<)F zf-({f7cyNEkz?nhL{^Bo+k1CUvNN5K>Q+Gwz2oW9E>$A=n4wGu#h_ES39@ zEhhaGuCojY+-9<*iYh=M!bAznBGHcb(^W(0obt(zpSiXO2caLMVuXy|} z?~tl`**eEMKHW#3we$05t4EDoQsa=)gsUy5kew&G;I|WWw z2;cnj7z%%9wNZyT$HVhl-8`3Ph>r7yn>bDe#caxSt|5dMx}N{8IznZ}O0d$hB@XDY z&`<&iKcjr7;p*3~Ypdi;_q%ozmqh~HB?Po1gnx33*Yl3i}^ z{ny3pAx>G=QuI-y!TI*;S4RLUCm=C6R!}ng%msYJyW$l_;RqIL)VTwCfWHiT^yc2NBWclXU&YB6$+-Ixam3TS)?_Pe|GbeI zD}nIp`JBC3(xCIVUqgpidAE7u-fyCG>~<)*rS=-609Pxi;N!!PI;ILbe=lgs>d@TqJRJhH&Ss65X2Syy}$6`T;S_O(g}`yYLJLkRMdV-VWu{IzH<-x@t=w)u`LNP)LXa(yLWf7uMdhQtk- zL%9P9IA_cDu3DIXeOHGBD0?OivSod~t1ciU^b%K&@?FfU+wL9y3R*@JLDF@{On!3S z&;E7V9oRBCg{{nb1R>>nOrl?E{*YSu<5vj}+}QD4gHP!u9S%OldKRXCxJZPYQfK`e zMBg8=2XwslvoK&*43T< zBj-zHP12I~Jgsvr!jiB>ijThUJKkittC6zn&w?DKy@Sd-2eBUc>9mHmlqxbuA@mSR zEnt{CMydC$v3hm$sE=Fq+WnysJX|Gc7vI_nF~?#IXq8;9fk&Bmi|*)|8R&=4pXXlV z_IvEH2RvDVgP3Vh3?FDC7k?D^l(8g@%+W?pdROp@p~(AaAuz=ml}b48^(;-=tY=kj z0S2r|ENQEF54?jsXPrX4!ysFH(9s0GPzYFO zf{oCZ9lAJ+?tJAzQ3Jp&+FzU#5C>a+-A2n(sc=h|ix=QIJy`a|^Fs@Zl&opu?j5}X z!AfcI=I4t|OA;yITtj{lxwf3?s>NdUU`1@Ptl{)^!QXZA`-ZE`iiK_vPtZjSKGb0E zP2NbnkKipA8>01K(lZBLqbOF{y88u|8xW}4*r6_wTl<_rNwvZpIsB(zN)dx;q+T9{ ziPU8n&sgfB1^w%d%`{N?uTSlQNp`T%0 zAUmC&spta2mBzSxBFR>Jx$~|#S>(_PvkS$AR?nt(qIqNFb3Fi|nOH~D zUVxR4Z4qckH?oLh7Iq3~<1Qk09X~$9b|Kt| zm}S)mYJQ}pR(NH205Lz+@vuH%c>R5%oz*(cTVs~aE9d|_%2lK1l>CiHwG;Bh=1Fba zBxi7*e`ZFFH3|0g8p&-4n)-T?YncJ3bf|_%M?Be-Gr&Po5J#tO4ZMDYLMr$Qv94Dl z%eAMtj#?&-A%1*U%)zQHKy)vim7X~~C%rMcaF=s0*{*}28jP+^+CPo*!8G$Qd?Aar zxTO^-J;QieBUNtX?`Q#8xz+f^3>PFG4d(9K{%^?t#0d~$W0(%;S%YdKiSZ#0I7{e z03J)8tEm4J_wYX{#Z?*t^L9w-j?Vi;x4+v4j<34&gSuWk!?L-CuKrGHmh02Q4`T;N zK*}M3kMN%hVUicSEuN&h$T8LKvk>QyTbKRW5mY{IR84>gP*>pQbB6-SP*tCH17FcN z*YKb+)ogO{TLZzH^0$pLXl|_uaIW-NoIrcgX&Q+Yq`GY~5KpK+Q>2E>_zN_gx$sku zEClRp$V-A#d+bHCA0cp&*$UNJK^C3b;0^7%VT13Oydvwre*g&=yoESZhp6!RmuZDc ze;Y*^zI}6_ov21oYviZtXQBp-b+cs>5 z!Hc2z-bAR$qfwLHRlE!XocmOY_qUW*WWmWb3KJ>S;E&qc|28vm15l^}ayBp^NXlP) z=QS8|0Q;*9IWTGurhZ8qW+vN!H;4j_}WLyJv?_M;J2Lwl)*s0UCE!aRDS6Y#Pj1?RH06Z__aiI!+V`2P4 zX&HnbHxI8te$EFkHU5r76Tnsd0t>)&h?ke+vbT zz)^hbcOKK_Y92Uq`yOyp=Q1we2wF>TQPXu0-9p3O6d42}Rkyrixl<_Nqew zdngQt*%f{w`}k(E>#rmJCxn z_IQ?lGQ`|L1gF8#@Dq%PJrQ+}d4$lm`3FExl2)@pj~(ROYHpChwt_7{Ph(yVUTEhv z3IU>beSy12xJEd)IGwKr&wf|Ccec1bClm&d!w$d5|AS;wnQ z{4Oqu0hD5qATpNZ;UmW1R5rwXmC-&QM0I&6i~ zD#}6w4D!T3%;`f5d-7+}z3SHHuQA;Fj|nzE-&`Zyz@8SHP?rmT%eg~jX^TP(#CxtR zv8Ke`&F^wF($B;p#V{e;Ll7pR<@kDi=S>3745!W3HuftL)w7D3ZlI=BJw2cbi7g_& z&4;b8;;{sut~&-(_%^eRMm|N+>U5rza9UBbu9RN+t>9*k!I*Yb-5b5ml8SwTmFju2 z*Pp7hIA8f@DS^2Zeh~SR3-zM$C7x5VMz9JqmV3qZ*4lFUJ4iqPd#RfK8#GNX-_*@B zL&HrGY;HE1uX!Ebxue7;u9anf)jng}Pfc>SeBw+@1$_%CC-Xqw=#Ku=WCK#8>l71M z(GOHNpj~zok+wt^MBdL41Z)$%GFX(D62)%r*QBX3ouQzcfwbQ%b3MnN7C!vmOB3XtRu8DGShA2JljitzI95Y|9?N%yi^2&io^2B0F-@X-ct2@IL$`M8WDlo)qvTO9+N%JU3e+j43kcu3(A}=VEj-t{3 zMKf~p{f{!LD(gjzsR^}${9Nf0B;Q#!-A*?%vKgY}G-*vcLLyxJLQeR7nS5M8T07~F zu@iKU9;!o_y*EL#jbE{Ds&RGiwSh4Xz$Jxh=TEE;_3x@DQsdspZ3K^*_m(WdLXHlh z8L=S|A$@1N!zmrY2$?Mzb>hP5X0SV5am?V;SLTv(TZ9g8KGr#IZ8D)o^uo@*8gYs69jH%S*bn}?a5t0?==qxyR|jSk9a*uWKr_}WIVDU?)p!}jaZj-a zIXwB74oSYXDOP1ytOyyNj+WOKwp+PFh8RwXU(`6X`JqkR+&uf)D?MhB#wv-VKMyLrrsR7nSr9m z3+7h#W2A_pkY`93-#Xw_8!UITy$t$XV3Q`9k#_iOD0sh(zrVRg^3Yr|W;fp5M~Y-Q zQoGm$(o8;e7fP^w3GA5O8;?LMTWZ!0Q8?!cWfS&JW=BWI|xBTAFAswP4tGkr8r zGW1mj$DuVp8wy_WwyW3B6mjCIr$b%ky zPUC<{Wjx)l8CZJ^!>wF<0^|8-*@^LwUKy2uEvBW2zj=SzZ2nlI<3*)Pn(xIXQ+;h> zW?M`mRUJ#skcy1j#d$O@huRn>!Uozd{oOLx>ocy4k)gLt5b>=1AHyGIM7Q^DJ^HQb zF{eE}qoeLih^Tp83* z{9WVN&GHt?4@}Tr%WxY@YlNu^z8A44L#{b^@Wl3d3(6vF6&$D)FV z90hrQecHQ^xAYB-9#bo$-qwg>jehqp8Z_);zT8HFxM1NzRRkmK2rikn!aB z60WT2^(Cpc<~)x2t5GtRzO&lStO2Y!TvjORo{xJke#Q4cy7rg0t1siobEJ~U6SMdy zaTjhQR+o?@Z~A(+-z?d7!pMUJLWO!Fe;enXnTna*c9i#@g-U2&q7|B-6J1qNpJ%;7+mp?ul9yQ@tZa zc=|o@`M5zSQ-1^!htY361eMKtP~XRdCJQ8j(eQX4HdYjVH*7#cM5X7ao>VFH>+-01 z;AB1L(qMjSwJJH~V6?BQbY=C~9}>R;bnhB0+k)JLFhnYItrAqb3^Xbc<%ClcZ;Je> ztEOJZ!Gth+^hPc30EW@AuuWI0Iw^8!`b79JvTwhpuTK!>Zmh;9%BOqG z@Sw5ogxmtKzk*GCa}NVypQ31iGq!@$D%U7u_Z`RXI|x{y=EigilB<*Jk|yry2)JD@ zHYVf;Lp)~_=A^;lcl?f+A!C;92@oM|I?(a?Jb&a65AlNV1rPwB0Paq{_4t7Rf~kKR z<_P?{JO8>t{^<=NeV>ht^xw{A0{S*$&w4kGU1VvE0+RuxzRP--8IdJ*u(Fj5+e~L!eTItH`(ahKC0QPpW`EXWdi0$>$1?=Sn{KRg0J1oX}F$v zpyUWFRjRp#X}jga6ht-9@&P$bY*B+qYZ(IoR}7~My5uVkYN`%D9^YP+BEz+d$Dg;E zOEVQa=9JgO>Fhwp#S$U;)L;67q5 zi3aIDV|4^ws-MmWGH0_w{{9-BUlCH;=O-0Z#7hPPYS2ca`0K~&<)~=Y2!N2^v>InzSe*Znh~Z1JU@8tCL0Drg2?8 zPdDTh&=Y{)eMoREFkuWn1z-li@!yhW|Lu82KVt(Rbmt*TRHuU#BlANO0$`j8d?B)d zrT{G4ZvZ@B$hSsN2$(ylEud@n7*Gy?3Mhb>Gs}7~#c~;d1jH{*>=9N6f zH3Ksn2Rs2OtX!+U6W*>6z9^P_!9WB{J}VK3M*Jmj09mz-4H{;(jqWCZY$}&W1hO8= zc7;}^S8;~Rni&hH&uOX*9HsN0<6!Xys4m#|a}Lo|S&^?9f?ff*&wWi`#fW^N2tYyr z{}^*wU0^pzHGmob`;RGSgGBEm`e({p9Gb3MzOaZuVF1$Cb^Esj>c570fxvq5|L;+b z8VErK|LZ9KIoN-g2bA(@L*edJ87{KjCWHkGB|^3A0ux%f#r(Prl3LJzvH{Njm6SOP zlPpkCU!<=YH((HVBz5|tY~2~#xzFo@5kRz|ez}2Py{<@KZm4iIK4pUywc1eW$l2q{bjt{dcCQJ}_jyrDx2e0t19(7A*;LmLh$F9%& z%{CK&OAe*Vd3o4!CQb{pElMA{Gq-4zf}@N@|i@mcT-XalTs@nQ{;gZ zMJ3`F*Ag)=wX2O?$mN6R;LLh(@YY$m6*AEH&oI(gP&*)9O#I=!n2^MM#IEm2?EX(p z6~-#6{Tqb{u^0oHcmz2UYV(5NpKpW|A27`fI(X5vh~za`s5fWVs5DpF1r~6kd*+FH z+5yYPB>k{ayD0C55QBUKkZ%7ftOvjT&cc8%XojH`8q=59RY29K4ySupALZ}7qedZU ze`&0I(X4vIb3sZG$)y6twU04%EXG&Tj<--gS|Z0-9_-SMd2i&b`woi;sWan|dWso@ zvuS)R1!?%oA{;BGX-JU}%1=s%7oux1KgIe`3kEu}5ZSyLPr^mF`VZS(iRQ0^Ba9%? z7mOAgdOvSXS2_#1WQT2keIQbvdz+<&v2{Ubl&`m!dEc-z4I>;%^+0sO#|$c^rpoj|n5P|t}cBksP5 zC@uhr2aQ#j!w=^Yx)NQ@PW10=4+W>zC`bepOx*TY4LPia&hN$RIx!x7d$qwY^PTrf?4JcfAx4b-f`_b0#rMp}@9>t&H!{GE8(4NrdYB!d^g5gb(iQn(xEcI2>IVO>MU6H*z z(&u!0(I)RYcwV^MR~0*qeG@EPj-wyQZ@)x1UVpN+N4yLTc*O5G)(;H5bU(rfC*;IL zqXJ>~JFL_RI0XdonUq_<#f(C2sP%e7Yk9UOa zCXpw1>o4cbK#z1AZy`5wSL5l#VOqoSn2vB18NgI>l2YTZ12chZWKhQT-T7{d$KtCN z8b}So28Qft2{4Yg1v3ITrV8dz3_JE0=(k*3!NgFz-f{|gmk<8GnGGq}?AP)Kl5{kW zdjG2PN#imOGS!LZL_;_VGoI1bXjSRu*rDFWYn3}q&8mtwS(4P+_y(we5&0U~EhJ6_SBBZ$czm5hyqDby z;$`K3p^m6KLe^iu@{BO~hV3i%*1vZt(u4#kr}0IzFs+nUP|#lMEF@k^gdz6YrIkbZ zI?w7@J$AA$+|C!5+{231Q22DFPIuwKVi-q3&P}ydOKlI2!IkECoVP^`?=YmhS!qtS zm&Up^(|&Q5a+_@@)Q?PuoS#Y~)H(u69F)h1nE}pEcgQ|4%3^ja;W?Ige5n?zB+Nv? zC4Tx0LH0Es^!U`+Trvxu=&6Aa8VJDW~NL(RS~f;F$Kgy^v#<0?)`Q^X64(yXUn9X2y@1VF!VZLotj zo!Y46^1@};*&Ip9=CN`_i#5O%q2$ea-K{AT;IM;5Yop|cP4z45P`cX9V?h1U=p6K3P>A}+ zpbwYmVCeCkfdwN@+k_q9kkcgf`gL!=KKgvD`g{!HQ_&ak{OarJNYA;UB9PqrlFrTV z<4(MTZJnBT1FvL1SBz*NKp<)cC9C95TgDJ4LN8_y5i%Rp!ti%?fa%}EnyRsc3-Yp< z^bfB$J+*TR+zj0Lh-HsjgqSCWB2jc6*QPJU@*NkS=qon^61lY-RxCF^-?MhkIeUyzRJ~scceT6H$3-xv~9x0iY1{SZIxC2pTQph{&R>U!x>B$ zSs6}Zz|Y&`o2bpt*Uc;5e2B^TGrn1I6M)EWG4)WpqkZUm#yisuC=d>fMcb%@2F%(_s z$FOGFW~%%+oc=6Np~cyEI@-g9`xx7qWPw4WTr3c2VxR;+A!3xA?Dm zFJ^LKmqIS`R$c4xDGqy$aC6<&VXoe$BPN#NyP>O2AR07P-Ty&WES(sY)A95nkOOy{ zUZ10v!+c`-Kl*!|rtl+)Ko9W=O=KiQ2@$X(&uo-GfK2Te#^2>Q0a+06_OG_l{>92= zc`AtaR&H|`l@01%72uCOR$UlhI4Sl6WH_$kXJ&x#A*&B~?9mX|h_fcXP2 z0;OPm0TGzeZ}+lV*y2Mp%ySYg`uU-Jq$?7d3?Q5hQnf8*LwhQ}mt6iAn`}++SQtvNXUbOP}ND z8~oOX9m1SFGdTHXm^!8IGO<~v|3|e0$nn{#vu*3gfgdVclRSaQds%GGBv)vMWT=igp^jbP^#-cmucE!)&b43@Lfr|JjeCY}J1(N*W0eP=Pu znq<46zsufL9NAL=@iu*7rMetBm>*=IOGp|yiT;Xad}!HUo8y-^d)Ut3&cqc!ssbg{ zvH12s$<$F@^ZzANHxx>Me>cNXMdSvK3};eA3>$xihx~IYz%p$@yx2{^+_0~?bSo^q z=KldxR4iX$D&}(C+khipCI$pY!-%Tiubtn4t=y9da;G%atD{F#P2;8fG;!dtH%PKb`h$__pK96` zY>e2L z4gVi(l$r?qZ`g=LgyR1J8+G)WlH71&&FuxiPMxW^0I;=|-omF^!Mmk~gP1a$2O#Bu zw*Mb;WcJZ9@m*>qk=su+2Ey04D3hPqGPfl1GQ^bTLA#6Tx2h>2x8VnK!?0spfLc-z zF4RwlZ7gl@=pHtd-3ciDl2(rtg#c4FMHobmaPM`1OobvTOSU_ zvRmL_1`@hn0@5|D>lgMB++3l@0R~yg_tw}#gZfrin3D$+UcV1Q`fppG%IW5+5y>k} zWN9L_*hQ6_&B5;>W{Sh+FbZwd(VE0UJt9xIJT5b~`8fA`WP?g2&}Z!8bESgF{zH8R z8NaAcC3j&jtbHDNcn-tEJUG;xhIel72Df_o9Q{Ycc=W;|J{%ye;#fM5OBi6%6h;guqd_HpH8u07$o|$xo)YC+cyIKx9P6ChSDJ*CH6xQ%7p21o z6Hl0_JmXY4KGtQIRcdrpQ239R%wY6u14}RI8D=_%pU76|ITp|Pw=cq%)u5GBMJoFH zcRg!|?+1n3Pl)dq^XF6ueYdVZ(VL#*j#C`CClm429CpVVDSjVE-SV*y@Ug$Nz3g`r zzCI3KM!LrL*8O!_Q&9RX=_lC3VC3dE9YVT(cS}vK#Vv0UfKk9SIHZ85#izEk;J@wR z;2+L9Wa=L-GmLTM^H*+YmMpLASf_Hq)oXaFkeJC4HlT{9J%5@>n@?eGcKa7PMO4%g z=CU-!tN`~98y*+G1_|$4Vvx1x&aiL6sKKtbe(r*A@XN+O*X*S(13kxA?n`=7ANCg` z%rwUBB15qV<^9Fu?@LTJsa-@CE*9bJqc45D+XuL--(6b@uojgNB__9K4QP7}C3vkY z)5gSKD&KHU8}AH-_re3x1%_&p%u0KkD&K4EJ6Ia~!(P&Jlr$}*&L?UU7w@Q7VIu3s zB|dJiw!-Krzy5TkFQK-OlJ+lfx_U`eOw{iW)Bky6y312qBf|g&1-<{ILjMtvxQ%c6 z{Fbc#JPR&A1;gJU5NcUI<03}d@YJAbj1j6q8s*r>BqU)OQ6f_@1zF36f$K1qPtAL4 z`FALb=nR?Ih<$0N;Ld_REdQc*UEQJhLHJ*>NAl^i) z;2+?`#Q6ULocu8UCvaN%AHYdD6PK1~#IL-E3^FtTS@N(2AD<8G6=^%JwykfYxlMk- zH>5a*m=Xd)5s#(~LXjM4uv~#LVwGKk|9ZSbLB?w!frfN&k2PLlwr~)=rX1bKDZHOD zjLKt2rk)ACgxq|-B+X}Q-etiEE0no5$23lD19B8X;#6+nWxiOvM_L;N+1Tk1&vt?X zxV?7{^Ck6gd)e@^_j1or3&4^>t<49{hbElLsnD1&R4dwJ(!DXYm$0>^Pe!~?R9OGv zdT&fS7jklKV)+NrL_PTRrg-XaQ`ZI(@~dbLZ`3Cx94>uhMqZJzz)P0Cx%~>MF@Kj3 ziW&v_EC#yFd&BY6S|o8Y`K2KGmeBx`ly*r%iJIQui9$*T)!nH;B!S{5rZ*iJZvk;E z!8xcrx2$E{M~x#A^(W0`>*t9M(0fORcQTp8S<-D*aS7Z5Y@B>(!40c zf07#a*CZ_vErdIrMyZ=7c8hzgLvuGPPdTU2us>BC!WQa-f24*^xFoR47)=6d(c~en zPY2=fAXexV{&_*4SV@EZ_SV=YmPzN)TPkc!)?Ln!cY&5JUEWIhAZdI92gvF>uC0H2 zs zFk>i??_vtVT3%%|`&yj6mXG{!3BaJvSp>hHpa6gYfc*dD?H?lt#~;XjCY9N0O6zR= zGj?4oL0tC3=WW$vZv}Dm0BywBR-XgvL{I_3!ndRYpRQr7sufIUm=45dmS zOh4(#-3+WxUQJ)q?SD0L76El_TNcIL-Q6!190CM)g1fuB6WqDDOK^7x8r5Gi^kN@|9R9{f99Seq=;o zu{QnuFQ9v11YWT@2eyp7UDyNd^F>Dh#9yi;0~&K+?fP==5VInhsQL~ z<)l+TN|>HZsY2IK4dq9&!#lzG-KaN88j8cQgjZXtR0rH^r>xXWZ7f=2&TROGsV~jB zaL*;0H8bL@WJ-_26{}!yz4)*m2A{50%o2$N<4$eY#!rBWfMvvLGg4_0XW)-u;w+v; zo8sc=TQ2p7<>9|INnGPCwEAg;#y>;v!ckHoYq>SMN3y8`_&*9-D0$h%Kf<_)@3Y*( zymz$9fp>6HMJzb#Ek;qJl&#-xLyRtW)Pj_i4e(6+U@_lDM)H9j zp=OgpZ%vX)Fut!gamH2CX&gsY4z;|A*sV4@6FXxY0?D<%fZrtU)xKLA9&R=)twMe# zpIyC+_{`C=6mh_#Ih|^y6Dn0}C@7Hu)P#W>l~0)XAQK(Tn6X8N{_5J{x!V5wwIdhl zTaoSIRU^A#=mNtzeI$q8!cDs;-DI5z$-6?SO?%gt8}W-c6(LHVt#~StkQa~Q(wTY# zCx&%-Z^(Bfb6Y|q<;=rGlSEw+Z60;U{!V|9Uup)@{^A@tf5;7pWG?_CLiU0bZ?c1r zl=;2UUvMz~aK*Tc^d)yr0s-$Jwty^6PDFZs`!!i+45EJrP?y(#%UJPBaPvhvE$p>6 zbyy+QLEsl1QgnJM=7{^95hn1d`{g}tE6G20%J#)_o9_r!GGY5Z?kc&J@Fo?Vu<@_8 zIPiSu+!hyXpZsa}iVs>J<@^)Zxt9|xs`}cyA-4Wr%Za$4s(#=c&kK^`I0KOg`0^5t zBeZ26)&0BSeBuM_3`fzRyeL=}7q@88K}xlqKKx8$CGq7`(kVIjfH`Zru_H{sum!|X z$k9anpJc9!#hw%*OYLcrWg zfJ1^=T6hUBwZ)K6C$p6h{rMJHSdqSrgg8X&nj+i)P?kVHo0~0X0 zbSLp#hVa|g0K{eS3iSRmJoJX(E+*%A+{%RD|37?IV)7azBOL>(b=HbeamSs-wE=O` zon|1^I!3u}j)MpjGnw}RlSZoI@oI>pA011a&d$EQuInB4_>MIlZa)CCpU!OIb;UvZ zN5sqeA4+eD7(|{qVPge6vjOJrpNGI)-`IRbDjupHx`z?ZG=_d^ub8n~QQa(_&?dF4 z?q_AOb&3eN+(D$lw_k0A7W1Ik|M+T5flNVmPgdGNy-IC_ z;fiuHIQ7Bklaat~!hs0sm5`CsdFWuJ?T}q_*v0;`{G*|8IJ~)Xjp|{6EkV?QD%SY6 zHisJF&~i%Rd538Jyw(XNnF(LRfY`}aUC4~dKm(T6h{iaj!#CL=$8*PfAO6)}*=Yvf zjyXa?7 zk;aCxszgqFRA~)jBsOJodA_ppY0)m z;iToUiYHxUdVP8?j=?i^`gwHOrrP>iL4W&*jTZS{4IpFQaF)OvmGDDZAj>B_G-KO?*Ek(Fp<153>%+__~h|xH5H}I@^=2F%ac2&Hcg`C%Y z{#^E#-HKHMOCaQSjkj-Pj=aa>NhQ2t`_UaW^Ym8&-;@C>vs{*%WF3dw!TpX&W&=05 zmX$qObK$f4VGWlj_tl+BDt+@P?`jkSH8#7>UR=sI$!nDQif&vFH&ee4hVxD_sBh;N z`V?#zRjp|etnHWQgZK8$8>^ME*HfRrEh03o4e2-SoR!t4NkyMEt$I_}pI20BWaQVB z=w}UN>}nhxtHnaw)fQ`D*D|@^?bL6`h}Mq9t*d=usX_Z}d8oz<-hO;Ah;4K_*}?F| zZ>_WA=S0i$Sf$p`s`}i5^}z>)ah~8Cd~xOq%UAI`=F3M(EV5}m3fNY{{cL^;>%9md z3`qutm9&NhaFI?go9Vm6M?6!3*d~&WvTrP<&ddR5+u-H&O132j+%97*MneM-7;Ts_ z=e2OyDb=SgM&~*7tZ(cNg5JAqge6 z83g$1ELP%I;37xO{gX)2{P*|k0nJccFSCh*e#0W3q!3&O9IZ{wgO=qf_8TmcHH*Gk zbo#)7Dx{CkHcwcVSQN4ftm2HW*E=oRGQ3Lpgt$r81O5;7+S?5+DDR)jC0?;}Zdk>B zcWsw@^_K5nn>Tf(ki;-B7#ts4Rto?^gHpC0e5JD1=PYg_TNP3MSa| zsrt0|GIJeGL+{6Z{CK+K4+4hO+fDXhNoTFi#=e9MQbor@C8<3pkj`@3Trdl$NZ`(Y zOC`$4)aa`CddJis%FOy45yyK&LW{3==xkq{ZI=-F9@c!8!H`~RoKh)qt6rzLf}k0+ zPTX4DyLaK(Crl4&YrT7F`jeW}Z}(L2m4Q1sK1x`vs!kLGP6y|;{D>iQMvZAbGm_Gn>yh%&K1mNH36KcihwJ3 zCfdhAJM>owiblD^&lpY?-74HN%MX*F$J4% zG*%~Vi)@A7<$`8%&zGuc z2B;50ON?!KZWgylU8V$Z2frzdITq5VaFuf*$p&0j}VFa9W#Qn4i=|0 zCt{Mbfb9f<9oWc>)zrN|1zs2n#fRp8ggFq0F#2&ZSFc?hZV4}_TJ95t+(Uf#wCUqY z**s(*K{@^o_i!A~j=J4GJsi_lPD4)K6N?Kz)57D49+*kpcb%W4_)fbljrn^aF8GH^ zHq@VnJDZ#??gUk%`AVFGKQvtjbjmjt^kMA^rzh=PYtwBbR#6Yyl_Z*Vr9*Q^vFLOhHtFuc_) z3AFxYF>qK4wN@1R;+QWy<6#)pLDm}es(%@XlzjBz>8RevlFLq<2LKC&@< zFy{0pKz>jt217hw?p}=S6_;Vh(S{f22w07`f>6#+4@Ig>{bl*iojM~#0suLk+BDP7 zAwv~P^%RIzIl~|oSrAX;@u<)QRHD+P7Jn5IOrUv&B!&PX)|kC`jewZ+9A`|T@K_yL zsUMH_t@@yv*vzQRW6tc#I z)Sc3KcWsE$s>ebz6^mVmiPGtMuL<3kRxh_0qVMry#d;BbBJLdgNq|U;Fll*LnaGP6 z390f`K2zS@6~HnoTT1gq2qfxa5G(wxzC_AoDiANjP1js|{9Zx*YR^7sI+lY3`kh|b z-Y0>4Yz4BOX@0gz!E6-176th<59azzIk~~Gs!7ADji+hH(&y~vdyTVGNLJt|r>0MS zt-nvh55n+hJduzEB#~p?3IlTEeeEua?{=-r!%ZQn}ko4LBi*}{`&|T`Vs>uiOM2*_#JlcGDqLd?aEN1{MPcdncmyG~E^d!c_Tvb5ym<><#K=P}#6K{LG6}1C`0gr#jQQy|Y4sSb9sJENS!%=m50uvoHrW`L|G%NUvSN5aj0%$o~@vf^xw!m^^PEp3eQvKd`}5Ki9rMN7G5X zn{UEr(6Ww#-!-Dm5|A(i)91|zs)i+zG+XtL=CNl&uwi8wBpjanuoQgfS$Ko(Db3C- zgwBBvwLrMCmGx~4Q24$m37_NC9qt<>Oqw@~7}NB)q|zVyXbpL_c(=<2rVEDKV0fEEO6YqUvnNNl_+4kY!4Lu<^1#YcA&cF@A+o?|d&)z35ZKQ^kwHTJLB;d|<_HItPa z!Egeg4bj8RfJXR1X;s9jZU@<4+sv!)d&%PUR37aT0~>mnU|cRyJ|(Dw-biAt$~G z{je{coC4i5YApquD)x%VM$^6$vBwjk-}_Tx)Y*Cdf!VGd73Cf`{&c_Qyt=rWuSp^< z3;Xi`)w}#dvRd28y*53?|5hmJjy4(S$UFkRQ4kI5coBue`Fy6la%^84Tho(LvN8f9 zn7TK8Za}=U^0KBX!n+g)e(Gst!GF2BDqci20LxMDCJg?Q_HzA>;kcRv0j}6*&LZ;* zOzuU=0QtnXxnYxbVc5>XSGTNtQ^q&28M@kD2c)cZp2BiWTDi>=1(Z$-l;)|dxvNT6 zs}QW zWF#V6@P*1%*rhi>YbTapU_^pvHRE%rxekeD3M}FWORpu;3JpS7u9om<*(TBkJX!V- zcr79D23m#3XGB4hyhlf~ua%$`LpFR7oO*jq=YPZW*4G-3<=4R4mcmV-P>>0}mb!rm zc77d2iv5!Amjg?^u9wHzCp(v6qD!AtL&|7-+I!X6Dh!HN>x5xS2UJch9xwzv4?whA z1DS&A<%B`zO@tI4Iy_|3h$BM-pGW7=7WyrjNdxFh(pmQU?}^31>3y5zYgCAT9)tJO zH=~kgJ|R;UDUtIJJ}$Z7YM$>o#lm6zm||-KMgy^uJRKv!J(jT4)tqj4Dx-Q|=7*Z$ zZxt-@-vcq+(K#tg)Fpm^?e1I0FjXM=xtiv<20k=}pL2V2A+i*U;}`W;3K}+Rjn)eD zr~i0IAQJpp!!#WfZGKJ1`V{0r;zeWXT0Pq#^}yXW;4rb%{|=MNBsv~p^}{o~r0?#k zx!REa$g_(i{Io}VY$ei>{P(O`^3PO=wVI~W`AhEe@mj)p8q%`<6E=DcD<`E!B({or zQ(PoTVW7F(qN7tvktxfi;*ne?YI9rb1O@;|Mi)%do?Sd5)TvG6^-U)+*y3BI#qR8o zVB2fGEG;?JfFuQH#=i=-hdb;^i!h9N{RXZn#&1vZ9OK$PZ7ehE+DAHG@U1)b0NJZS zrCC?Lwv#;}IkFoF=c^=vFGW=8gge~hdI|ftZox$VqymFrgsVE4^Rf~2 zrQ4(P9_dbA`P1{9Q5(U5ygKdT2JVIS8;$zB;axxz*HZ#aG0^Hdo`o%KPo=sJpYo=+ z50k07hMt^~ii#`l#GEx_i0_-GZZm-?9rNnn3XbQ`S{*|<6&ja0DO$)A4{ayQm`G=3h>_ldS_SdR#3PKBq#cDB!ye_1== z2|CM?V_^af8;agRC|c@BsI8gYUFk*9NzNv`+y^bwHXE@ravCG-Qqw+d=ClG=pJ*gs z@4U9{Rox9Aj@hZSlf?SOZ2*c+juqGz06=M-t<0PcM{t1S)>2~Z(Kyq2LHvp2oF-9o zf4^B3o?CQly>1&{4uh3CbXU`{I>i6q+JO+F+8?CkNmCo^>O!*oVn2>76i+(DA1|!jPD0ZxW!XSPbqtg1Ojd9c} zOm!v&(m8HJsNhoN?(nJ>AU^23fkihI8pK3V>kMC%hB@sHWNjP3_L7Go_&zX z*C&>j^;)p0XNEfuGzXtu7g@ay+5vGI;vj1$)r(7(ZB52p>weEb>~8T;Fke;RelRj3 zXOQ?K0%EUKc8|=Xu){@CEQUy_H-bWij0t~Vt~}E;xj}sX2(g~pHs_`fM>RKTB(>q% zPEbcqev?vXs3NODjNYUbcr&&dDJE%>0jyVFMNoo{%-;OF9X0?1TFah+N!ns5dsFv= z8$WgI#|H?hSDQMcerava+M^`M8=h}pBFRIIWK*7+$6YL_=4ZdGMI@DYS5HQ8c>SA< z=(uA1LdQ>6mX}I8Sm=u@7>h$q@Wx*PQ#-%*!bc49H8xqf6denjW&&2hxB`&VIReZP zXN2?`xt7HtLBpSb2rPnNGaiv5u@LOvMW-z~5#7|r+|D`}l4|1?scjy*m`y%-lNAeB z9v2w$U8r@Sbnuj3z>E<&)a2!V+83*wLidkwO4GQ3{^Gc=Jyn>KLbzoB!>r#EhY@u+))-Ve9An)eL?a(btyj}e z2axSzFbVc@(pWW(u#}c^YJPO-kaL4eOpG$~`t!!pP5VKVV4v{MjB+>sMPzDygGcl5 zs%`pReV>$=ko;GQMjhaH&sjJmFUJ`Ne5w<0`u?%d3+bmNMOz0TB=)Lc~q)vdjT`~W*`)OyY|PSB5y z<+|m*78xz=&2}>dz80(+ajaUg^h}HfMF$7H<);|*_64;1s)J(T{d&ErLD1Vcx-^Zw zrh4eVYp#l$vRK)=ICft`b>1ef{H+}BF)^56X-10g_qkn~nrA!1tJAgkHdWW%(_oyn z;W_O-3j5yPMzLZPe;!C zxYSz5eQ}9fP<|Cmc)Jfi>XO$Fs41q8d!gL}T!Csje&kA4RZ(aR-ebx)m;#nH$_BdpP)2O2gmnyc_l-iFFC&JS* zHiNMk7^k&JwOBzNRs3zCAhupc?MhfFH9$|mRDy`V(c$J>R0W3LRCEW$T~mce;><}H z0lNM_b^pjByj?qNvJWPixAP1yvvHp@gaj$Ol%%*968oD0#7}UM>fV0XmUhq#C|{d) zY|ZwuQst#H zVbwKIy=HaT$Q9VNUz6C@=33je?I7Cxr)S2ry)PuRYbKTkD0Fy@S{Vs_o$J!sZze#> zF2`C2O=#s$HnuOc{Rziq;%td(2~W@bMxXSiM%;|H_ss-s;efLSHdwL3od-E#UCFpLLH%z9(d*6nymM0KL2T`Z=znuL?OJZjPdi)Evf)=PYGb%U8>x z`=PdL(8KTq3na6Rf{?6&u+gy($dtoAQq`= zB5kQe3d?L}#DE8#@%D+pxsT1jz=KICS%}nQcA#;hw36o0tgHRTQ*Ez0(jgehVn2$- zZ_NJ*LXLyZ(A$i8HbolhhhH&T0;UtcQcx>Tir84j7Xs^` zA|;4dSkJZQvmWPIlh_vXD=G;P75-=_d4#En)MtCH1qhDkq^Oq=TOuaVeA^kvzLW k@|L1FG0^YXs(OSw^U=b^v^sd#bh zsbYO~PF0<%I_GYew7w3aPJ_JalO*VoDD%T6X?0`SZ?}UixFpRxVc7Uc>Bc>x3{sLP z{UnYrRxB3Rpgu zH>tt23itfXZ$9#~=9!36~o zIZyoN*&u3%ByB$RU*5EgkqBiZLZKoGCCwLgH%@N+9^*3Dvqj-k>0gjbQq~=oiscWL zR`w|g{Va&1=2;N=$?Hm$9?MX28A~e989zzl_MlaR^GLuf>taEl4Wd^5S``WzKRj2! z!d9!%t7aQ-LGLOl`_Ui_S>caJC;uO{*o~wqV`=jgXE5IH^|RNN`0*#Ni=L7FAW29_ zE~!BA-cZ>EGZY9gx_!JaNFW2TT7QBXsd*wZVG<~?!|(C^V+ z!MpfFzti)pTDF2LWh|?#?A%oNNkF?wbxXmYU#!P@KL|S2>_pxX=+pC*7Fr5wyZUj; z-`@}Ke>3ny_JR;rw^Z^nEuO7fflS@H6g$iU1(`Ktbq&`-C7H9APf088_351DJgjdn zi^68Bux1@#>~>LN3H9aGscvuQ>aoc7E^m#CkhHSu-EP_lxuC@)rY7@A9KP*Cet9$ai8>Ed^=+hD#^uM&x_p^*7 zk=$c{W^Z{x{A`fWzhqrMYxuNfqd054CfUhEV&nXE&dH z9%K!whO{LbRBRCaH&u$@l8y(B_<|SNrtLu`MroGNnRJ{q(m_kg3!ii#`o5zVXiQ$< z#M%R*|CH+VIWyl+*Ksmgt9w3Q-*`Dmc?O$EwVe&s-8D z$yf!e`tzqEN*z?Mg1E<)bKeX|MAG!}#RDoaqfPLHm2u-@xjbdDytSOctN9U9VwsTSouVeD*rZ{8x3WGLfg`^48c4tho`mbQ7?8 zj~|z^prwkYw;B%gxymr1N-lJn&OYSc&a_t*`uO>!T08j?fKrWREh0Z#c*Sy- zD{R4toCUO@E34~Nkdg~puN~`~!AUc&vWK(X7N8EZopx1S)~F2NX4|R`R%*(sc>X6g zY>}V8)IwjIu7a5AYZ6!0BcJO$Vv9CEyxWa~7O6dGeG5LvC3HN+AEgPCz;BYX=MdfHW}c0YeCVm)(tvclE`g#oHfn+<{%0#Xf0T&(ls~QgzOF7X%|V{ zld~J|BOoM%gpd%@ruPx(CxO{VKwPL(2nit}q&kpXP10o7L`V>jPL>>)m4oP#B$;lh zh!7DXLPWSn2)8%QN0#RR2W13{ z$GGT-`2C9u`u@#_)aKmysB-?S!k=AuR(n)He$Am`38Q-#D~hNTQF2s5Sxm{f0`9Pm z#Z2;L)fXv9SbUm%R2n~w9pCsK#i*pw(?Ex}ul1r^t|=L^Yf0vT9_!hrQSXwlPm0HZ*MkV23c3uOue%DVt)|R9|W8Z+NJKGX(kJSs5z3WVTagt17X1@EO{c)JSEPEOa=p+c2lZmx zmU6aN=h~nf)enUs`#rIVhquL)Y`)#Ow;|2k)9tP1v|JCC@bdamD+_j=gP2&YZ zO@*ex0%vDJ%V%XXkqhs|gF4Zh$|D!%LRTaNTu4g@ss)@@R!2zBndvrjwfTbD4_3OU zE~Z2p^`g5@dPU*wuM1vJmkaf}7trn%oDUeq(Vqb;S0a5ySm%-|!dI)bDr?n+ z^|cVZJ_V_(^S6y=GZkB9cK%Y{6syaH3|%{Jk;Rc~*QgI%T;Jt`@_Mxa%B!$!q+V8y zxgjYJyZQyWfDD~l5UnuLr8beS7YBJr%P&b7eiqX=xp~~_i4dhAq}(v-{ty}*0pQx0EAU%{j< z@>?yErU6|64uAWXn|f)G*$yxRnix*@6>U6z4S$wsc=bUJCJBZs`KP2o(1zQ+Yjw_#wU<-iKDSt^(^)ii2%bU+>zpzw@ z5@$`fWdvw7ltO8)7s%HUERqVJPm9h{S{1?w*lQ<(kkn z&zzN3sFD#}t5)-d_@-3@bRd@3@a8%8$}0-zSuC&TjnjvfR};wPSYF3vNiHW!Ij+}i zeXH7uiH?rzG+WoDwqjic8GA}cDU3yF%h+o=DrW7BT=Ryp;vUjkR<|UN;2LRsD`pd% zt7t>%hdl*9U#X0ppEn(0XfI`x2a$e#}1e1H1yzrCrPJAMw9 z>oHiKD%nSHIBv7Bn2&+3R)h3)4~~~-a9*Zl>BtM77q1c^Er-)`kK*X*TC~2UlZTyg z;UTllYnT9Jx@$A1D|*RCxM(w{Fu=Gdd0Z#~BW7?nxq(9%u!3oyM#HN=MR1%n7URy) zbezkBv!bLvXmmbLKi{jvw?DB@4UU}7$?23FZbk`Mg;98LtPIWyIl)giIH^AZl45)E zCXQP|H0saD>F78)X!(S3g0y?cX)icg%spsWwq$t73Vt^6_7B6WADIsxj+o7f*`|c6 zVfeF|{FWR$$x>+cJmik5n#gb;4*qQjp~LpU@D>920LT5k7a<%dS4U7nK>3jSl!$3h zFfl*8gQFHWCfJQ+!L;$weR3 zCOsPVjRPnmLu7bN3^(GHLWGF0fY8$LY@(R6iKik?CYl!8=`<}@vJNz}>-J`wz0+v; z=KJ2M_9@&6Mbk0xB&mqgiKmmZiEym)bJ}>UUWi^%RzCu=^0))vGY@v^vFQxg4Q}|j z0gQ%kf9g@y0yKjMk87LiC61e=syICq$&Ai7;b_?o(=wY*IV>awOzcy+#Zh(~G`!!grMzT0U@xZ?@0X1zFyR5ZNp;n^Y&-h_;1JwIqd+aEzU#`*l{bC%_E1=4?533&^?%KhN0pMw73U2$+z>v zA2vJufxyJZdSmJaN6xX>#9qhMw2<_|ANmRVG7v0XwOEuR1AY2AES47dw|}8cNBTex z$EiR8@$Ge$JNb3hQ6&?-jsg_!l+pvl<+wR6Pr~%;(6|=5JZ#O?ks&giGSppNvgj1W zHPGw7Ne{AZx-L@Oa}P2!L=7Q|GN-@%-;?N6`}7hJmt#u?;@X1cv>?Ynq=*y`lHx|j zKZJ-7uS4`q$)ONEOES?}y+M0wnUGUaq_`DT1cqoJL{aMr@YRIt^1%;bZQ5>XCQ?L- zNO1>7KZJM~5F3rV<45ney7A|U-=?qe(Hz<=j>A^h4sn$C*1To0=&iOYS$H8X z*Nr4^U9htb9hujw#GoN3~=;UNg=5tB?W2v5EQBul0s5@Lkf)_f~p0|<9BgYRWflYm6Q6K0NxPn$dm~} z+U*evIqiknLrkbnN6rb=2{Bd0G|En9YM7i%oY@VW(BGDkk z0|*L*@!1X_J{v+jgm{-2DtNC#1!H*bLkQ1}5cfY)KIW|0|C|+=>Sw=F{a|9PJx;8J zN$mD0i5=#O6iG~Iu1HMFx@T!w4?ExS7PSl$R3CSOYRh924*EeC+6M}27riBxp&`V* z_m%)tbRABSMW(<70Q5k2$_%JVf4==0a$e%_C4lAFl7rq6U}k(8=|?RR{`0T$@ajEc z6N&9xlEgqh5^>zPGm>)CB^U2=3sbj$y$8l-(H`39S&yJ#szj&Sdg+kPpWIBK2}> z0zd4X!;d#?hFne8wKliUm!aN@`uM`|B*FE4E1zWt{LP?#1v$D7kA6Y@` z6*MRA?Lhkn&dE<-!<`p391k%G!4xD3xd`Dv+1$lpn-aP?HaV?V;c{Rg!YxhfAsJen zp=C=3F3sSli^I2n7+(Fzf}z3@Gnl^-!w!pyr1?icPV8`wiI!0ar#}O7(omlSSwCQn z(m5$z$Dr$?;t0dB(l{%Pvck0(^e!d^HQC1;zWs@PYH;LK3-_J{P-7=MuKonKkE!S9 zIdC5nejk&G5)lO7<8d%O7i04Yam_OiRY)%VC_`lXaEVzMGkz`BGcnq%5H*9{SJ7M^ z`O;G*8#PP-Evi`oyBKd zxL7C$7SX|$44l`4@2CLGH;~$<6|EjL+U5h^7|NF<3_ptp^qcLGX*75yPQ%1(;$v!G zNngPXWPYnf(lj^^Nu3;kXMRd1DJ0l1hVj3kmtfIt?nsQI=Ls#+uYSA(Sqb<03P5G> zl`_r_q1EcPOga6UibF^{t51-Oc-9q6ZVHVkJxzzd`^PVThaiOMXN3@ATP2kkJtZN( zIIWxok)OOSEUJ_zaZ0lB(n`&vzaEAEeF|d@hOAc2vq2DMLDXdH()qev0E=LSMEb?gp1)*ZHK9_sXmM}shA9pVw`T6!%CgX#3~k=x`3dWa+thd>-DV)Q(9i z53k-Mvi=lq!y2~)($Y0JdDSNgt5@cS3ZV;f z*>AT47B@+`6Ncj$A3Q_S$-}rk2uY*mN31!{Nh9cuS~U%#7Gdw)_2~=KK0$jZW#i|q z+K=hK(vy!^?+n@`X|N*bOZ<=gtH$Fe&mTN~^sFJvei+6t@(&NQ{oVP^UqQ%U%2kjjRZ&KQbc`bMa8^xDwUVF(V_dlHcKa_cj8Ou2W03=jB A>i_@% literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..640d27f677fcc08fbe239487ea17d501699dddd0 GIT binary patch literal 21042 zcmagFWmsEX*DZ_`DHONjw8h=s3dP;sA-H>s6e%vngS)#0cZcBa4#l;&oV54-z0dQ0 z*SW5fUo+V|D|@fZHRf1j%uO1O2=(^`d%QYgzap7Ib^h%cC#465?ItPd#1oz z`MkE;YOqLG7AsBYt}JV~>2N-;nkS)cshzD0G%VO?lY|Qw`M4N4U@cvMo_WB^@YWvq zB*XcURYiJ8R?GP1V={S1r|cp_IEJhb>qno6{pZ}GS9*C=_fynhKHp_NX$d9!SP3or zwEP1<^}K^BU+jJM3|{PR1JctU!vizE^i+jRo8IcD z1uhPq7HaXzUuiy36A3&1hWC`{ss>~J8!!T0^innG>SWoIVV!!EoXU|5rHZ8oanDS)x^*vb*WGscoYAoIpU&X4> z1YC_&D*lZAHSOZTDqVY_v|@1O$dG@1noH;DG@_;98#c12AM=UHG(gHX(!Q79ue2RI zno`PF-A`@M)bZkxWOdC{^;z^hyi)Qt{V@9>={&t;)7xOs{n7{X_w*#Nf!MTu+9^y! zRguEoi8(S-%lzLTub`X>q*S&%;(yg_9u+)s^I9S@AZPWtz8{Y zmKuN?GTsm@{P(I!8T(D~Gr!wSjs%yiy*n=_g17LK3cQ}F417$s3YFB)pJrFqJRi)(zUHy~WahnK*;(EsF=dpSnY@oqn1ItZ!zZ8YIy_3I?fLer?7Trk3t3q6(j>qw9$4RAY@w zZ&%wVm9AukaE(GKSHma#3^&|8e0vMTxNbN5l2tp^)R;fg@Kr5y;_wBlxgu^#dh2P_ zX_U8^{(-s_mM$qff9Xu1Z->6&kYba*_SSoG{IVGxNjC(UZoe&Ur%&<9d-V;TU4b^D zq7R-~`Rlh!sv(b_!czLm(AlNb)p}A@`E}xj>*zPw9 zZl?-2+k&sgE4y4>cW2^!2v=xrDtUb4(OWN*^18>z5Ji_zWc}41@WTGyK{EpGLkt z%maSlW5o8jir{7yqG#BZ#sK?vvFt}T$~rJSV>}HR^jpc)FPA6)i*^)pq&&0=;Lq&7 zA;)-}g4_V~K(aSR0f$qgDj}ymEca2`D zz0vo#jXW?D1pMe4Kur#go=cheV%*r_AA@7cj_GzBXhJW&1c$jA7~V97C+)u{cpMBVt$cxs-m>Bw9Nf9@!&5fk3SEvG67?DY z*vSMN+Y@c=$Gto;JeJ{?;%?sdv^E|f<9|;*)H zqZOZM0}zGExKIlqe25fF7vmAR4=V*XwJ!WtTG1afKI;tywXOb8)sNWCI*_x)_Q;_* z_w;nb1~i&SCoIW1d(6NLT(l)Cl?9c8H}nd#H;LIa-g*Eemte4fcEdZ8lu1Tn2ui=m zT!mo?CceY7%djUhS=glWsPkDKBENO=G3nEb9YRvH@{grUge9mLCxVskbyk|5^hx`o zco-H-wLjsBdj)o*we^uW=Dw%*W|zu>O%FPn(ddCBtgVTN9s;o#uajB~#vQmHm1agw zmzPMk26f9F3ayyKvp}7bnCOb`(GkRRZu=@eQ^}I{Ib4 zVy7&ENUzBB`U_&-7@5|`OHPL9`rj)9DKU4iJ;kE(pt9@Z?~9s=636jTyK6bv0pAR* z;Nw173s70uu3LG_n!FfA2`2w+o$~+ZzB}JgGOHOn^%3p1;$d1 z8M6u?Gc{aGvuOBZL>RvL^j>dda0=GW6d$#g#qD#)ni*J#@9&(uN?M-8`PvcskeL%7 zfh`XTpj_>;hmA@Yt%6k8(qUwH7acyjr$l%zVWc(hm=avB&M_zdaM!sUotiR_V~KCh zF~!e_81(+KgA|2Fm_P8vl_ZUG!{uUd5pA0PmHvrRZfa60fz3Rrl1XUhMk;Mn*fa zw^6W;0H8m-k5yzm` zM%`*3lDwRAGxq&BsYSwsuaD*L1z#S&+A+1@Mea?*8#wgw*dT+v-rQj+a*+|AJh|Ar zBdNvj4B$C-EHuxNQJALbNI!<$Un5$vR`Wyypsi+{Hm+~2IJ*tH zA0`(Q_J=YG=^oy@3!#RuB3!VbrO06V`r=V^v~sn0(FDtA@rT8&DtNYFoBcp9jg16~ zIA!!YsqcHPK2yp|w4im+;HI8koCSb2${N#8`rUiV%);8jX>J(vG<~S{Gry__&E0{o z-c$?*uaAHC9hmp-zA}~0VAV5jUq>Nb?Fw}& z!BM6ixfCF;a19*~+R|0a0f%{kxZs4IYbX_XH#H(JcaQfc=9}7|&-o*fm2UHoZzyx? zYqsW-%vEB?Q?lCz!^q2+q<(?ShB*LtH6u)XujvQjXO>GqEo~WtudJ*Hrb&bP=&@~$ zx(W<92NG9ktwe16@=>`FLd%4>Ct}Jnt!?&A+EXK*%g8{Z zTo7gEc@tr%-Rfud_d&VOpNll~7ZI!W0-6%{jQsqynUM|k;I8iZate)f==%&gJE7p2 zzeCGH1N+K^o%xuj)aif-kPqG&LggaFsWi!XV0^m>oFmGo>$}|5{tRmkheKrL`e0B> zY5_+r42`7tz1ddN>2r(OHW=2a_#=)4)6@VCa{xZr5S|U#^$x(SVuZ_-O57JLp;Umf zHEI0eVvIZ#?M^R5cku_!fVpuN3{H_STuDl?jc2#N2{VGsL&$dc!I{tNJQs6-78RIN zpTZwWwY;#|QSQz*KK~0JBMizY9@r3653m>zhND&VE4fh3U@YPfSX_uw>SLZyf1^%Z z$I8G%v*rYxpL!nU(uX54J&+``d_s1RM5N&2Xpq}$s8gIp5L?&%jI2H3k6R}@pHOfk0)Ms7$hGUvK@TCr>C%XkD}Rs6=?rEwOMcs7Bo|=y*%+zMy!?jwP#0b(;ouG}tBSds%=kfhw2fbWjt-KIA?!bw=7;h(TN*hMuVmC8{ z)q!1@DERv;>ZNtEEYEAzE_=X}nUZf62@biWMezR&pw~q??&x9@t;KCCzgX(he@4cO ziq$N-zX8wH*o9(u=IFfp#$?{cR#SOA6%;maqv(gEngye#Q*0H*^8aP9=r3qUn*I6w zPpbZ}5JNFkrI}d4yaJ9Evt+T|?usY7(Ejtk=NzIYm`l;7Hi`2UTN&6oJ*bc51bi55 zmZhZovTn#ZmY&1!E-l#?V8JdQ9^zEP*SZ16{|K!zlbG6I0(b;li`ste z4+kLYZouIElM$than+mu+?#_aHw+|4{`;VwZiSr_qecTTQjR2KJ!wFTy%DzfR0>~t zxT?w#sY!LrzN}HlVtW1grP7{k&WOeFYm@aM*!2Tt-`$z4f!Fw0W1?tuYEI~W`$*>F z>6G*SwVa?XrO@m_WQ0|_RIOayE4!U*>eF$gP1}}wo58ohv-!V6Av9SJc`_uG za%eXZnZGyaAf9 zuG>**>iy0Z=T;+<6fPkxzBwn>p0Fy$r4=T#g_nZ=B|o8^_i)s9aFDq%tHv~rtDiA) zoXBWXIZhWY{^}WvOVF|U%>6-k6}5IR84j20%7v6zZU-R7`+O3Oe$)!w50lg8UpFp5 zV9{oIF%p!y7oERD+cn6Vv*j=V@7%Z|SY2CTT6fP- z+X(-Y`(&{AgTf$7R+(5W$}8=!B39m}?gdN+3JU9Cqa2(0V@J!>GM4HUP-Pg-2%T>V z=2)|vtP=6UaDbcxV} z(94RuI`SUqGi2k@V{HicWESC`cvoEz+GI>yb@mlpPbTi=h55=X5sihjdi6gm{-4Ev zc)Egs`*(>$BWrfTK*Cv9dIh}H@;Vn7wG;dP*PC(Qw2T)Pc)Z4?0W}SdKXCXTTKu_~ zSlU=cdfgdl4^k<)(a^Pxr!3|a@J43Of|eUfe5WX?1mV0Of^yJjdd)5*^(udyGIY~A zLKL`nf8!-13VESx?{qi@V##8m!C%2rLInPQ06~Xu;g^K^M$pzD@M6)iH4>`(gEJ5? zK;&xf4ibU?8<$TZ$!6m;(s$lN(RN2FQ2yvw5eoc+w=5x_-~9`{{|V>Fs=t2ygO`76 z8Vq(86eO(2qn&_7#d*(p_3S2M+m*`nTuk-63g4iO#WQPpQ7^b6%o&~ z_D0eASu*$7(9GkuQpMQ=(Ej~~PI}8?4@w{8j+X5}5BdvPaOG~++0t+RB3Elc*WW{; z8)$#;X5#QWZg-@3P4>_K8oy0p#3e8>pRLDfxwsxKyVXD7Jv0J$Cp4n1S%5xF*hD9zPGE~YI}2pF5{$+$Ekq6YLs|4% zury3vN{P4M5={_<>>a|4)K5`}o)Dl_2uA<<{eQ!(vg~dPcnT&{ z#RwK*%YE~p^o%`*xr#Rw=MB-wglqaDd|grfOSpR8w>XT(<{`6R6@4b}UV=yX3H7Ir zAhZ`_^nPWl>+BMtqvd)dbD%EH67VdH+!z{R2aXE-cb?9S*S!iBI z`58Y(VnrIwnXyfSzN{E8an>qoVWzG^YO#R8GoD59%me4Ja!LV;t{lDY#~+X3262-^ z14h-4WP&f$#K&t2_tW>wNE!T*YxI#BlA``Et9A+Y;#$%TuuV2=ra{Hq-#$OKdAJQU z;`p#gBTVB7`6Qn+4b?(Q`4y=u?don&1@m>XQ8IHLM=P1f!(8L<2tNJ0Nj6@I9xT|V zpnaBHTje1amqj| zCH!TvWcnme%$8GtaR0t~(|7`Y0lYOKDcZN zW9dcv%bCQdHD1~7YpD2aE2B~+MGAhKFY3u2f^^?b&2?2o`Z5$$zDSKV=^mx;*ZeFp z(vyv%utWBx$e3 zc^0+;HAAR|&x-QMS0x7#ZFo>}2}N``1zQ7IbfEX|&TURLt1#uU(sWe#WhAaQ7iYGH zc#_tndxh48q-&`eJaIgkE{}&3&PchMUfecD=YBM5!pgMWwT{=yA=##hT~PB!u)lyW zYvi^zW{sJ8FsC(9mQ4XN14DN7ZU%zp1hoff9cR{;ASk$^3Xv1BMaOsush`cVnXIHq z#*woW|euSY*ytnxAV|Klg2GPaZI?gXNCG=-`?fUW5BaqoHX> z_l*jd4&Q6@3()(ahxB2IJT%%5LJ^@$F*J87wL3+IAXOyg#}6y?f9eTbnQOJIim?`@ zvtK^w?3o+2zH+M3=FI*NF(g~IV^!;+{97ac7tSzvCbT!U-+!J_U~9@A&u9&hI#5qI z6JwCt^U54X#$P+R&E>C*9XKA&KVf3>{po>zidMSza=djoQqM%`xID4@MQ+tpk9*jD z1Y{Y~7|a>+u;kG#gwLGXD$yf0Qg0Qx9K^tB&$ja2lVNrKtbcUW@IsD?V4T;RP~G4Z zk?x;bHH%bAogDE;%J3^@lYQE|dVhjdB%Ggx{7HUnVy%l;2GL?!seQuuk8XH~jpdI7 zp^z5_Et87v5DuyO;}85EiXy*j+FCY}N0_LXk2S+Eqf>X)(51HZdQYk<_siX1Sp~*J zl7p$_JAO*3oeHG%`(vh*GW-;Ap5$jbqKq0*s-#ypH)5EA40`BGyGaeoYOB{PqmCryg6QAvFS zLZf?(;;(blJKA{eO6u|+)=wCBy|`$M9sA^*wR9UK9V1Ka2@5ojje*e4E?&q?UdVlV zCu^y_Js;)W&MqW)AICp)gF_#1dE|&3k!*PvRLrZN#c_v<}p zy&E9}^!4bq(YeokQ$q>UjEgCWE;jofKu_hi?BET!V3O>lCpAFdVj8sfof&Q?hY4u- zYTPRFV)bLm;^6YK?peV*mOvau+=8^vEqo64l=~ zl!DI~>&Z1Pll;Pas4*U9;PoNEHLmd_WK#;3BC~OaRBSVAr|qzxH{-a*54Bt#qhAz; zm_!vn#X4(~9D$(VpjK*e1sT0QTJoCo;(VG#_=^lSm2Q5c4pcFrWX4boe>e~4Pm7ou zi+B==KmGv-VF*W(#Cf7xDuNyVs?Ki)pPc2ZwM9^VZnqAzH=!BLDA`HF#T}QUwdL|;nAI1#lH0&1|9G^@7JLk@_IuPV{K$G$dH zG7*LveS`?yDLx}CWS4QFfQ5?zZ0^~SDS#sO*pc0KI42k6&p{-nmtocdbUJ?m(o)pYeo-#1-F%@p^33{p>NhwwS=slsW<&+p#|o03PTGBFP*WKeLQ=RX z9Suv=sK`(ieB7s+bl}u`xgrNcvK+P4`%SW@eT=38<=l3t9?NJe|Laa5^XrajB>tub z*SazRba!V+c7X@}THCdX;kHKRGHQw@s*r6s)m0pI{2wY-P_Mcina7I zjt^xmTDpa=B4&JXm(DF1|0=${xb9O#>t%^5=~cIet4u~XP1(Z752N9(mzwSE{K0M1 z;0KAL9Y>ZQrB2Cb=&Ay7o-n(f{9(7b$3DEppvCF?*;zMc8mVm%9j~`u>LM`^xy|fx zP;bj)ELUQbwe(p1?aXh*gPT|t^TQ!KOj*lMBkOc8e0DMmse} zxT70|Db<6$;n|Cfp)%BWTI|^=C>u-tR*50A&g7-@p`-K!inG;9|@#r)kTkK z%?NO>nAd7>`erFSHT;eeaUj>TdWdel>Zc^QIDUVIlI!o=mo@JyAfsNKI0QzeueKLf zIapwKrPXaHDJC~b_%^MD>dZG0JQ27>@Dn^5_|FhcDjph|)=`lKh4$A6BlA)vp|y=& z2!cB5C7_-sR2$TZ@BLG*md&>t&1#YPhHZ_~C&$!}_sxB@*0YR-O5T0imeRGO!~CgQ z3mFohXGs_`ns64f5eK{EO9haGVK~u)F0@_da^Zpg5 zlJF^#5nMN|FWisn*A&7DZqOdf{_d6n?wVhMEh$MQ5_VVilPWdMR}}_k=QP5RN2Z_1 z343vlvhVZv35n7uTJMq+#3zmJlz;-^HBSXR;OSosg-Ye^I>}SEIHc>W>?b@ z+p%!ANO-d@bSaN!#t4xks1}8Ot4;4z*7r80LB~b4-J;SfDH%wcPwt|j*epE9&&py$ z_#WJ!+>NBoMB&FjC_LxFTEewEVoV`0d`tP9o9l9Sa=Ip^9LTkH>+07mS->Sz&}#i8 z6f{I$*)DcEwYz&DL`3>y`#klKM^|!Vm7gRnFrd+QI?!CBTw2al=Ol>9z~Ds|V$anm z@p4ObE3I@~0J~af;@`>B-!!g0GYh<{ZR93UTRmxZPwXD{u4LM&{U$V8Ld@*?p*BOZ z;9b^G>FkkbF=Qe`>(W&hxwiYiVU;5EANB8m6QGB_? z)+wzTpV@&f)j-Rl57@RwI@3l>S+#G&*uMc~`sX+1;?6ll>*DVmd~aIJ1Q`Q6%Vc?1BquUONlx^nb8|SapA0tKzszl06 zj5C0xohELwTgqgKr*h(C)+CE1iobI$de_S@b3N!`ui2wD7^m6`E{ZEl_ z4&MnG$EbgP6HkG6=5_Em7Y~rC{^ z1<&5dUfK2nw!_Xf$9S}-GKYM)+bB&Upv7rYL^YmKtZ8j3cxq{oI`Ar#-^9FD>2nP;7Elpm? zbB?)(Ur#a(L{XhGykKu&((iwMO4>ea*A}7|gw)SmuZQQ3PKadRvU4*_&SU{#41fqa zcD4>z-jhOGkMPcXRT0*;%O|7FyBv-IRGHC2bUL|k^{B;g&0Pj-Fsr7FAdqU&4ViZa z|L_zCrK3m%hf~IaA=x?6p5aEaHls9Z_@|TgXBb_*-Al1`-;HlzjxMng4x|AB-+=Gx z8uc(*IPj=f%wNk3Xd|#HRLj_uFf15^*1R#2X`~hn@BzPT}g?D;2 z`0%(b)S;pf+1qk&91OFUodnsnZ|0K|LFcd@V8~l@{H4+m3 zL`n!?hy$s?%eBWP6tCm(czy)FCuGlJxcg^9aQVSjeO?cQTTE98^zFS{+5=7P1X{i zxsc~$BA~oAZMVmRYv!rbM6bLN|H@MmrVq$4Quy1mnp<) zL_id0?SyM_$=$9lvIVgOo4G||6ti=#5nuzD7eVrVwmp{0QbgyR3>1nOhdY|lhPyzy zH4@pMRAKkCJz@D29Fz2!zGz9ebpJ3>Vd&S`d%fs;pm^QTmc@iyY*%&0mL&MSW-Lop zawJ}-9Igb(&(7-mzL=EBOcwZGJ!=k**HV0*$+UmudyhQ6FZdq(?1;l;5e!Qkhyb6KABB{l{?gG;}1E4@25DT!DzXNZJS z?7-#w14!dc$l}hF;8ezD;2 zq)R{&SSV3jTZc$j(}l3Y@hxLDvkeaDKGbf8)_AG=p;rxFxEo?Weu?c~C-hsd_dtZ3 zAi|aAJ@suJ=r!@LLmx6&GDnZ6JhuHYkJK&HH6tDnR7R7 zWqqj47v^Ac;x^bipXW*#Su|rFhXQ_u_{BM}SjdD`u71YMyo`$$aNvHx?6nDuJ-2lI zr}x73i|y#zH0ztn?aNE}6dbq^AMELezc#vINmwF5B^fY1VASi_HGeCj!hZY0erpR+ zpZGT`U?i^Z(A1_j2gU|F>Y(bK0twHy2~AT<&&;3fpE?`DFQDpXr*m^7+c|98B{J&2p-=BX zeB+?9$4MYZz5hY@zsyTWcodj&gv2p#j;k)LbYjIU@EqWFl*swKdiGYKFbF#jBvvwZ zQU#e=yPw&Dfipq*JCcRFTAE*qwzw~xYcqZQwR%z*e{$rD1VS8Lh`3!&W2Un;!?w%{ z3@9$JawE;0q;&{Hm-Zd6b?FQur2TzQFkl)+qBFp*Gg60A-FtnlfF7V}-Dg#X z^sl2~Ez*QJY=SyRi7tu}H3#WG(&?&$W8rPxnAK)d4KQ4KA4d`3GGdGhuq`QhrrwX$ z+9Jaq;7o>W(25If#=4w*0^(~IjS5;L{^)YnM9C(|tOI81G6B)e#=SnkfBTvK5yMuy zcp$?XSGuVNR4kN@Im!X*uN#59$puX9!I1f@uUB@G)FcXpqJdLp`ZJrhrSU7!D;F>T zkZQ?`MhW|-!J80Q4e|i2TP-jLhnDq;Pvm1y=0WVx-8LB&bEXt z#U-V<2rLTxYgB3SC=hcnAhOjbkYEO2^%2*RnAmE#RI>XA#I}LBMyj(hibu^UCNdli z^)mVmSz+&Puh^Hz{pPZA#O?NmJJ;)zO*&BKJo0CjAl6=d44iRW zI3W-W5-y-NZFNP~N1--GYUI~T)7w5^4ATDV-17i_MXVD8N2)PiLHnx))-z;j%f)ISTh#BeA^b?~q8&{_BxHpD+@U?x4;pUIv zt`;`eX^LWqCJk*kN^K|F}pxK?d3fBUz1pwu}L6&U+Y(R4jL*?JnsHZ zKoYZxMsIwKXDrw}1C>>5dvqldWEGfv$YO5A%7Zm<p+fXYs^o6GKdNob2<+A;@=h@@^zSzoo>MT5tP#51p{Qe!8 zAa_U&HO*F)vZrRdj~J>F=E%3=o6bZ=CWTivC6?gYls1tEnWV}ok}+KG^I%%KJFEM6 za+Qqr_26wI?X-y8#{-A=QCDFJhElA%_p4}e>=<&p+kS@h@;8)@O2sSjg>_rSxRZC= z2sO0crs`iaM&8n2W=ZaWHt#>$UECcJgDxQG^E4g;kdu$Gy3afA)RnB)9!@H?he=;t z*oo1m#Ydz$A(N31L#it9)4TZkdr5q|J8a=xCR&=GC2hvOW ze8L@VnnP-ZV*Yu9U@hI>IHrGQF?#En`cd|&f7A56dZgsKTt0t;p4Ond=YhPS+*Q#O zvXnx>B%h3ln0zY|l38BI99~U>WWjBQ{kEsi?X=Bk*%u@_C#`FVbA%^HZT`?pm)PIA zeGP@mpna(u=~&(0mY$;n*6XgMr}PQ8Ld%|ZXdQ1Qwm(z?=7(%z23tH&BB#u`UdS$U zYU{?Z!f_V|S%GJL!MW!JmP}K>81kzJ4+9`HiTkl5y`^V!j7%=)wTjK&@G719pb+cA z(6guhspaU2^rL@)*c%VNrLR>9_7d;uExQfhQo^!#$!(fK$tv6Ik&Dr@Snpu6m37yrbZz9_M5H^?-&zv<*u9JJ^o(h1>V zbgn{|Qo=y~TP}>|@|4A+0FRh*5(v39{+uD6OBXNWLZ8c}#N^;oBSdWoZAy@r4c3Lr z{eDFL9K8@DK6u0HT!j)_g3dZVE!dl)IuSCoqv|z)41CMVVZy?H;v?BG4crd%@gDfC z(-IEQ3%795$Q)0zRH#nucbiAzzCUz%yiESuwuP?kPrr;tDB-?6?V_T7(Z)%`SbmSlII zaS(n23l=sP+*>YEkwL9D8Wy5WPkkpOOX36Jg}ZJyc*cAZU`Mv}@An>&>SlOoMYHsi z?a8?I>kdyC_oxTRAdJ^dM5|F+>m7@NGO|&qvpJ;jrDLYRZ1NdSoLKan1I);d`g+#_ z`4hbde!Xg_xKrV!o77p37HQ~&K6?2dES5L|Q5`^t?H`xg{t$d`px?eH6uf?eTQ66I zU!yUC2w~?Pf)wQh96+iR_8!q=Ni>kfOr0aQM>jI}suy|@jhBMTP=O3*0NgKMaz-0u zdbu^c!4$c(5A_A zECKx?Y{ff0_;6k{TnrEDA`B@R4Kf`jV&^?JkGUm(d-699Gf9s#R`WCHLw=b>j7n(8MEBh;_~77r)*u5jp;*ILNeO|#NtvrL z-bsn1U>jCeV1a-Robg4J=Pb{iNxu6y@AmviihCzB+g%78zPkrDhkk#6uV65gATxdT z@~#`u9|ctgdmhfTId3X7tO0|_=@@kww6fD#Z=0PN-gEULQ-V;oz9f~$S{4Ar>_|;$@f*|dXcI;hg*bLqsP;*G}PKun!c`yANSwbbX3H@iR zwzOQGTF+9F8#s;W-1{p9>nQyAo@77n8sIAi^E6Ca;I^+gyHcLVc?+bWgi+vbe+%1W z{@Rt9){Gx9*z=00JUMsN2Hdl3>bMh47{NdtRTou3M-18iBT8~<5}_=^n;?gMs?HT~ zt`i9IluD(KYTo^;Nnpu%a_SJd2GntnAnYCjn^O&B5RXB}A z5;UQz3A6>M93-IKib0VEoh{1@^genF^0<6@0Nux7Ena%~N<&xB|dpAB8OVD=2lDqAkMs?6A#7 zrz7kE6Gq&jl0{5`z43xWkS*QJ&Sc#aT0j#JDp#B#{0>EZ&CdSEvdvcP!b^XbPE%NV z*iIBJzmy33YBeAg$0#E!huFbF6l*n6r{Mt9M|7Q2bpDaiV6V(8+09zvu4tT2o?Fqe zVPkZWS|I9FS-xi$rRhVn-5aoIpX9rS^C?{aJcoyOV-_dcSq~eKY9M7a9l6NqMR|4J zEk}GQG4#Q=p}-s&rn;XTk!a5dDTaXk;eq8`EK_ph+d{gk)Csru?<6bpgLvzq^d6Y; zE~(>^u!WA?ovFSBi_TOQo1luKed(2rp@3`8OKKSj7pHcn9PxFo36vbw)2j<}n)H{&Lq72e9j|y*947B{(o>JZJlz?irI?v>4NpJw z5}7Umg+i(MqAq z2L5axGZeS~(# zMvnY_Y?5664ARWD!JBlTq9Dc6iD{Mlr87+;@hiCA;{8>0gXucJoG zE#*a3NZjhTCz|mW(S}6!lUu57=7UUGh4nu^m<`hl=hU6OaFd%^x0(Z?X+}AI6*0io z(5@#D7f_zL_k&Vi?YsR+J8f9CvSEv8=e&RV%gumZ%_nKWMrq-ZoP90bFF|S`_T+*c z?eFCnbE;6*!*D1CL-b$N3GJNFzA)#f&yG};uO?PCQ4Hus*bG&;jr3U_O4Dwo$0BqT z`L@+O$5g2P@n)pBkG)yLPK%*UitD5%$lzt77V0capbk- zP?9+W!?q5KYFVE0tFt$rDCLeRTLs^>Da33Uy{fvRyx&UXn_dsaTKQF^J4to)0DhC; zj}+6W+f?hvAUP=$iXVbtW)g!_yi-&?9hn^!85AUK{LZ2{l7-eWG^w!<-M0~#2LRt_ z_Tq*kfpFv@R+DV%@2}@niTmaf6Y5>xxFM$hmi@Xy4nK)(PJX_4#%kzknYFuj2vkfj zvo^mo12w3kpi`PHX!IUah`CDbcE=1M>dZ!(i7c5;AF4RpKorg#d8L0Gx(rKU z$NG`6wl~(>;dC*jEByLt@;gSVQmzhpyK&EHuWQV-CBHwl=9<4Jo?3nxo^!KAqR?z8 zt;u&vKo0M_5Z7C%D1h#(UwWrnW%tc7-;qO?t}VRol!@}x#q~WG1qT} zTXs?g2-W?)sN?}%%Ud;ic!Q_0y+^m#x%7QYdWXQ{@;lRB&bSXDQmMQ$0<3FG7;R+9 zKATLB2-6{lXY>xbyMfEDGWC#{e#L5NIW(w4q+YThxXY#Va9Vlh)}EJkyivQ&7qoeC zILqv{=aRL2rrpesaPh%{Y@YuUj7L53NulbPBTw2k3*kO89kt8Ru`XIe%5W+#yG;9M z7sK?0pgwpl-nlPMfdF#}RLvFek#MFCp>{o7N^bZP23=l5hm~%K7H&!ZNh!fD4+d%B zP|su|_rWUi)vg>Oy#Gm^dAFZwF(8J0RYE8ERSU(zz+}#XMS1m>80L zDy>|gEMQ|Kt{Y}=!#f;kNralw8!W*t>!fFF$cB&~3Jj$JUiaiI#f&8Zy@(tt{VgI@ zZW*CHol@b(%~6B+igSZ|=+h%;e(E|B{Ww?x!(lo~4c|xN;Go^M<(Y;xj~#Y?`H9j& zo8Qyr@UZm_^P|>JS!AUE%z}uZA%|TllGeGN3%(gyg+igHZI$=7?i<2EKKVi*VfR1ZR4EnBW<4%4J%m_ z_!2<9Nu9npnZn8>@t#X(=?i59Rynbo%Sc(p9I~>UMPt?skP}(es-&HMiI+krLwy@Q z9TDaTjaKsESIZA|4OQq8@jx6yD|y}OF~h540PXvMLIcoP#nlcai&O1DNt)-< zlrY_>(n?L~%Pt8jvn_jA(ebrW+7}~`X57v&hm_z}$PZPIPEroynIb20=t8>mpvw!J z)ah0_be%$K8igy#tz4H#3*%&&imOXvc9mh;j^Xl|r(!06@f#<~pe`GmRo*zv@z{PE zDUKK*CEqTbW{1uAVXFVAx*{*Q-(u%ogx!<0Rp<^tGw0jQ(OWR6`R8Qv$;Di$Zyi}2 z-^C#(#GC|y-6B6SX$^|%%gG>^2Oz{Icr2Z-ByJt3@=lYaEo<}7-(sI($(!?YwIJXs z#IGymKfem1hOfc;q7PjL4oROes~5L!#mz@ zyE-fX>gyrp2o=6(BsJjH!tcaLIG7~T7nloq{DAWHvT-S|OqpE<42?#gxrlh6mL(ux z2S-AjLQ^Uc-e8RjBd#V^PD=S~A^Cp-=MEV0+pZa68f0MdiqdRpEVB8iap6TDg|uI* z#`!;RYj*WW&!&q_5dy`XmX4a$SIGEx;Sf+w zDqpl>o-cRZ)LDQvPJ~5^zdGm%-LXB~8d)!@Vv}3bc@Fcj_KCJ~B!3ZWztt90 zjZkY~#i#&Hmm5pB6RfT(@!$UWkJHmX#!zZTu_EVk#h9k=ddzLF~`)meP*LSk$Ud-3~YM(rbxw~-~Au) z6FNF8kaRk;P}qp+6oJXw(K4CW(wMP^jb7xgapO$MnbOO&aiT4` z*DyX%F+afb#g3Z3?jW!yC*yzrEPXUdH2$ghUt+r8-g8BS==m1Z=+)*}+Ki7-&6Nj~ zcsh2#QWV#VGqv{PgsygUJ<(a^dM>ju>5W({i$?!>k{0x4j@)V837C(L4`Q>N-&k?C z(59z(V=)j@q0Bj=U?AIu7RNn*tWUBQ>x`bYjfd=K^UI2Uar=L z?Mg+;@I)+~b`6WU*i=|mk3VgVsY@~4!Zy(KlfbiRK-ZP*_+qAk6Bx|F2q>}CEVJq9 zTLtra+V8gUm_#X;C%Jrs*)5&vSSQyY8jaH;O6Ue`9J%<`@oa<~3aiB|IvCQC$vJb5 zr?+aTcTAnxINX4G+1Yt{qpv1g?^aKX z2Cb%5j!M~N*l3u{!w8I$H8J$`>(9i18QO zahQYg7bSfjvn=Vro>D%e6|294SBX7wF8?e?x)fjdt5wm=cnF!W71b~lApz_K*M%7)LOgIH-+FB48zg>AoK_i z)nSIGq1jRlMz863nnQoTQ@|tlGA19BaVut7N^o7&ped^33ch zdrD)*)(kmTa>*DGlQPtCRoriT6`1WZOA}`Z>m3Lc&lRqLC+=$Z-XtCtak6_aO^37p z@PCd7w@sY8EN`9oJT8v3zyx!h%m?8xZ=kc~b7v33Y%1$tZF*X5i_Dd14o5>=st~Q> zo~C<~Q5lv2EET65%+gvjFfAoBL8fNs=UG~7l6@Q&y$A8}N9mw>fv=xi+&~ zI%BTB7xqDXJbm$_HcFFJtGb^b&^A4L1ZvG0-&Sblw%lsV-`Bay?o4G@s?1*EtZJQ} zAl}M%^$i#sa;CXBkOTvMYN8wQqx^`FOqaz{_i%=cDl+~YiZH9To}<*vaCByAh8Xy3 z>*}c5(b9v1JSrZ3O{nI%Qq5yV7mkf-N|59D)#gsXxIs}4DRLlMOfkLF!hi&E(TX*QYI2^bcIDpC4mLeVUlvWM^gw|6$XZ5u%x zzxOSAjaN2z$t9P7kb_&~7zAyA0zEX4ZMqdelYu0s$gL>~#O|?4A0R=3=1`y?K!Fs! z<=UsHo}{}&e>HIdhyIT!QFDlO5oAX{&g|@b{Kq7@I6OF}+P`x;o8*Q>k0sp+9Gxe_T77ETyQ5kb)tx8wkWJK;)38V5XSIDiex4Uh_^h)Ek%0f3}8|2&^vrX5s|m>ibP7Mbd8a zhhVI1PwOO0X^M$$w<|&*E|V!@DLSpJP~-_=-uw&?Vw@3NU3gB1JpKe?N1hW&G0GYl zpe&d1N4V$we}>utProS58-|fu2NBW5G91ny|1fOZ{&qPo8%m~ePa6*2o7DXHh5vf} zS6AEz$u69KAYdcU+xT?WtO=1LkHOG9y8DyxW)!TH)|B~|Oe#WfVh0;RV7K<%4(Rph zb-Vt?%gHsJ3u)w};tD6XG4Qa0cG>|Bn56=_%}Ew4=B;af{Jj10l{Evl@U|^R zPShP_^H`d=7MLxuu@;CcpDh7XbToTmos*mw{-7HM2O9aGN3W4_Nk&%yo24p~>aMtW{WIhlN7Gq=B=fw9@f+^jb@$xJd}3p;SVtqqaL zbc4*OOfn=)$h@5ivZcOv^N`X_;#h~ou^eOQNPm9(vPqVF|D^KA7%*)t+&IHVR&crj zXOtDOD!jqHxX2B7y%uiF2FC`@P=QSwC!Uh?gnKI7R?Fb{z?lYIES{3{gnNpPOf;5b~dz;FS5 zLQUR@j}x6}7IP5`{lTvepef$|bL-%y%!td;`Z4JWW@*63PA?@{$n3@v)Pq@7L*1}? z24rQ!bW38L>~3bVE%J&$URr{~3#@!BHwA4N8BQ6bBa$faN}{;8Va77famG;!bdiFv ziz!Yh!#LNZ5ik6}0xlu*F`z#R$I7`LYZP=i-r`9O;jAp>@P!rHuF#w)+adlB&S^A# zi0c=Pvs^H-U>Z**#eRtcl~Rf$O_ZcL78%w@xE&aRu%oaZ$If-~i7EZqbIcc#cChrHfC_|)-5z%!n9bp_RO{}zM zC3i7&71M({t7FcOUWHeUBNthzJu^@XogK%&;_8^D>F1C-CccgtK8iyGKPMf`+=(_H zOKLu3sLJBOsKRaB6=a-pid@WSEH+O>ZI;E%uyqyfNcl34R4Nw6K+9X!7+GM^NvJLB zB$vRRXKT_we>`plYrC$?%ho1^AW^Q%=nBj5x+mAAxPp{JP;^LDEO9-&q5_CFgxaDF z?RwDscYa7;#@1&=S>CD-{X6$gTw_d|IO9aNiJwxtr|w}6veE8tF`bTg%HldZ0Jlfe z;%tRPIL1W(3w;HvZc-w#uI^6!uN<{+?+{k(SziWJG2N6UIz*e*&4K6ix&JtUw6ykw zWJFt6WVtCC(R4VSKlw{B5n+>6heTWSq>P9s2d(RjNdLHz+ zRLSDle{}la+PYm=pUx)Z-Pzr`dHrv4B~wlwgN{AG8LZ8BVKuGEX(|uI(mfE2eqkw| zh}4m&+FGoLU2zAY6C;nql06Pxx`*pL54R7?GCUBsi!YmBO7!zs#e+OiGW`rM#e7wi zJ_rgkUF literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..e8b9a18c48fd6d0e8cf2a94cfc694169889f3a23 GIT binary patch literal 1703 zcmV;Y23YwYiwFP!000001MOYWZre5#eb-kI=t~PkR+B7=n+^rqB*Ox%Nsy!%uwf6h zbZv2!NSCDSWWyfzH1u_UFknA1>}{WtFBvIIvTRe1Eh}m5GC%;wHqSY{hnJU>Mdv64 z|2?5SbcQ)+L-pt?X72$#^+Fbdmk8iqpEK5VC1a5vVnV$*k(f&1(X@$&dja+)o453H z&sq*bM>+l_L|76=Tklk}TLXRoeV_qQpMXd)T_J;rbUeX*FK_Lot;g_V{9`O}>m=^W zrLlEOFKt=EodQ1P93mK~Zr4H|H!o9+IlhAdM9U(ljVeR&juP2=gN4b;`vvRPo^D-< zf5BOh_$yFk0MjgEnr{;7rz55gMc#ORC$5sXeg{Q{#u6&00YZX~)9__F?h9|vFrROP|AtX#0@HfFpZ5`V=KQ$m`VOU>22OkTgz zmx&h*^fCA(Xl}d}aMOdWQ1CkHL5Hg{lF%Rm(YnOLWmz)_FN5$DgmEIxsp|AB=U8}_ zUZFqJv$U~amBgnC_XdL2w;+MD9#CM(%7r2W^(H_UDcMFfjnqq{q{?Bon63s(t6848 z;4Z21N^-TPOgKD{$T5C>joFxe7=d|i%_c*!oIcK2WL+i2+PXlRrM)-%8_N8JCYt@ch!laN>-Mh{nm!?wpuRt;q)UQ-yC~pK+ zu?R4d*IDuysb^O_rfjVp;!>WPV_ZFMF98ci)hjh4Jw0{{JY%>Q(s4^AzG+ZLinqLu z)Uzw~XocO^j2I2-jX>*f_Vu&CC0Tu@F>m?D_zO+CrMEXThQ@%VK{R&?PNy^VD9*dp z#9W+$dL_`hE6|d}Yfc6PFMTO+(FI^GI-{8yPt=eJNOMM*wbV;WvxvDh)JWe5Z%)|gz&zaF-P(0`4xAz8dU8HQ z?)N`Z_R~8ml763Y2|<=#Z?W`4=Q<<;`4Lw1Nc{@b$5Le-bz}Xq4nP<1XspQ)ON7<_ zjxvdEK{^E@>fEBEq(gi)EM6-STk5@lx>=`@WM~)?KSV^L4n&Oh1R9bkax~EBvK6Rz z07bapkBGukEhNWOXn4_boKdYg)BqeJT_Y51NO~b~Hy|-kF&dKzC0(ULvu@>_LhCIq zgDKsp(Cs)WtDk$VRR_gt1F6ZD{Olzh!(@w6|LTjP5@Y7oOLR+~1+*2j{5v~LhT!h^Lyo| z@1ZZwRpg=yO(%ZHPHu4AkKmdsn6%l_-=?%j`mOllO1-n%E|}`DN_JH~Qmudq>j-nfW>9 zWAhen^x+75Dr~LnT9>md>DSAh;nG){9&Yco)l|5%x0%K)okza_XU*gheYJh}$DfqZ z?5ixSSD)?ml83NrcUM`pZ7*##omQ`0<Sr!kAGKswDi9^INW}&r@Ec3-L~_V1xWh6*NIKn}owg2iqLFX6Or{`x^$aQfPv7wt#!J+{KZVXak zJ#l|aL#(`a;*|c`C;-A&G}B>Fql2f5Wfj7aid105$C`=IEuVsV(G9U8bzuPXWfA@b xeoAdw5WFn^JtR_p5DY>s=!I1Ak#&((uY@S}0j~beGmfKY&i^Vv+&$r9004L`PSF4W literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..8306b737ed8ee92a81732023ced8087efc214232 GIT binary patch literal 1586 zcmV-22F>{&iwFP!000001MOVPa@#f(-Rmo`Y-c1fPGVVhSGJtCo@rB$AJavr3y8du z&{6;cfVQ>EqMPj759mz4%wJM~FHs^yQ6yu>3TB)cMNUp%gaSaH?e4+UQCW!t>8So**K9P%E ziBnJ~26c>}OEF6|rw@e9`?r*Q2!VnSzf3L^hg45rM$YakB*JqxQgMb)lLn;=C-@`Qipq1*U zXvL~mbfHxP%DeSsq-#{~WMEsb?MAY5m=GEbfc2eDICD_d+E~-jR;r+Rh;JjtM&#;| zHw)9B0+)*a^T=D`Z}BKmc@|R7Z!RW**_ME-r2Q*=-x9H-pemAIORlD+A#YykCDNw3 zLNWEJ06isio3rP!*7ywqZfTQ*j7nE)P`L(p4U!SBjdmUbIx%2HpLKj9gVb;HG*j9L zdIaj^K&u7j3b0ViOFHdeFQ~*1O{HXbPK;+-)?~}X^8{JeP55lhm?4>Req-e?RFMbp z`agmM&ZcTj#KOiIkbpWXpw-MU>S<-vFp8=&F)LNp;xKL&SbcCW)!AO>YL>a7%iU3B zOM{+SVlgd>>6pq|ms@w=Bg@WI(z?{Ly^qb?4(;tY7(0pOCRW2f$u#>g^?|i>DA)UK zNt2ANekNpO+ZubuwK5f0nHSdP&O@$FH8%{uW-;}q0A>}Y(SHknE5s>dtGRG8c+-8; zdwtZo$6OEMC#d)9ZcqLch#ubH zCV=DSCTCb8tVS}*BwB#%WQb_IK%;Q1x46-%646!90-7Y1Mv|fX8F6QbNHhkY(WyZ9 z#P>TIC|=}(dIBiILEsaGr%FhUsnGDE-|572k`oQU!Pko%1v?|t8StJ*=0HWYX z1b2EGr{Wn!7)z`Wlcgi$3MGVY=1|@?YnRO_Ymzm|n)H+=4G+2pz2RGHQX3|9O3pF# z2)zR?Umw1*7Fr9fh1S9sWa0Bo^R1cIOlzj?T&;!HLTlmkT6nB29K5m?K9z;Tfwj322H)hETvkJYbn)Va&I##3^KFD0vUK__L|d<7>(uYY7e<=Av1ut3$|E<(z+=_-OL zYK>3iFN0Y5K)#W^&K-Xvck$&9m2Td(aw9Q!^Uf53DncUp*Xp+hmuw1ZG^i7Un%`b? z1%i0tDr3n@Y?8+fFK^M`j%Ju+S9P64$h9{_lwhuwGRREd(sQGW_jQpoPQ2;XFs;Ad zM~7+^%vpk&sa-DI(lWn;aG%Hya1 z9{>8M7pdAdzpP{3V5qGd9Cr_g*1C9MprhZ?G*h|vL+ah*$G@{5H7NON4ocxWlmuNM zWg-iy3Z$w`{@Er!w#B^U7Gpc=J?*INM!=W15nwH|`)&KY&29g5xKD0=9e=dg>r;yM k;P)Px`6cFK`xfr?9a4LF{zcjKY*&8&2VK#E8}?lQ0CMpXYybcN literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..3b31660b2bafb1909463006950c2b790f5f58e9d GIT binary patch literal 1590 zcmV-62Fdv!iwFP!000001MOVPa@#f(-Rmo`Y-dC{d~2f-#x-OLfv56G=6xaY==3}D|! z)YJVKoL~Xlf@Y0f-Pizrh9w?caOOvzY($^|+!SCP$t46h=>egb&oy7j1koQUQ9eXC zAacGfaR%xppso>gVa&ps;|IcKgBwadL_k4^U&iN(L#n4QVr92AB*t^s;}vW$xa55l z1llKO;1M6+1~52fd}|eQXQXg$4(DpPq6sV7pD-3Q7hbnsQN2u|T+?D~>DC)5-p#`8 zM^FqOw_Ju^!9M340=UCeHX>LwuTUX&(FF_UGseRy@mjj8fK+y!!E;6G=3Xq)Rxn;g zv*z7XjVpRoimK+?l_F}BjwS9(@YpPjWOqSbM68HwgC*ktJh}DEW-uTDS`&&T;`cB~ zKIo+T8CtpPHC56LbRA4DDY|LGRTuwFDEWc)Bnxz0{D@?2Z2L4WnGsaG1 z;b{1#|HgTJ(7VT6FXBhY`Smx-e!rn23PZ*v_-QQvjHNg2T~CQXUVs%nQvU=Bu~f4T zb!Pf&?SL`hWVp#GmI$krj53MlAbU9?x}Brb=vE(lqhn=6Up)(GoOT*XhVG}tn<667 zEd-2C1iB|d(9=N4CKuEbKoJhZfG9lGLUK%nh8KfgFUd)cGysP{Z*mmuluV|;9iPmA zieywql#G=Xnzf&C3T>mO zh}5gN$KVip2VB11e`O`K5?TqZgfB?K=S%agm{v?Hrkz}^gjPZ;;qyv(s3jb}vJyU( zgrlLA&`M|}v=Y7`3Af%}jBy~IZhv9bv}%5}YTD`5N@yjt5h1dzOvTuIGDgK$DgOr zF9kPVtk1q{c&|QfUVW{8g`-I=-wIDf4PQpqq(CQQSzm&ap*O#>pK+|K2rN;xs71)Q z)|Dcdyw>_g{=$j1FXS89o7DIlxyvtqs8xB_Nkw9z^3LReI)=pNU#Z_(6xo!l(V%Vu zYJQ{5B?#h28yTx!Y?DG5Ug)B~J)L5XJvE&YAveD@qKao3$h>K&b^?Sa9UcVJ*8v*&WVd>n57#JEdpejR_@ o*y-Dh_Ja5hiTNeQWA_s7bgii^vVT!>JzHt;|9cK$n=)Pi0QTet-~a#s literal 0 HcmV?d00001 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..a4675da --- /dev/null +++ b/scripts/check-grade3.sh @@ -0,0 +1,38 @@ +#!/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 + +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 From b6f08d797007cb97ebb957693de10446b603111b Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Sun, 1 Nov 2026 17:59:24 +0000 Subject: [PATCH 2/2] docs: document the Agda typecheck helper in check-grade3.sh --- scripts/check-grade3.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/check-grade3.sh b/scripts/check-grade3.sh index a4675da..733a301 100644 --- a/scripts/check-grade3.sh +++ b/scripts/check-grade3.sh @@ -22,6 +22,8 @@ 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"