From eca73c7deae919471d41c916f52c70db0e66d6ad Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 14:53:11 +0100 Subject: [PATCH] =?UTF-8?q?theory:=20EchoApprox=20composition=20rung=20?= =?UTF-8?q?=E2=80=94=20first=20slice=20(retract=20direction)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extends `proofs/agda/EchoApprox.agda` with the first slice of the axis-2 composition rung from the design note (§7 obligations 2 + 6, plus the canonical-split retract direction). Obligations landed: * `echo-strict→approx` (§7 #2) — general strict ⇒ zero-tolerance approximate. Generalises `echo-approx-intro` from own-fibre points (`f x`) to arbitrary `y` reached via a strict echo `(x, p : f x ≡ y)`. One extra `subst` along `p` over the existing `dist-self` path. * `echo-approx-comp-sound` (§7 #6) — sound RHS-to-LHS direction of the retract shape from `composition.md` §Q3 / axis-2 design note §5. Unpacks the existential and calls `echo-approx-compose`. * `echo-approx-comp-retract-to` — canonical-split LHS → RHS-Σ section of the retract: picks `b := f x`, `ε₁ := zero`, `ε₂ := ε`. Uses `echo-approx-intro` for the inner echo and the original bound for the outer. * `echo-approx-comp-retract-A` — A-component round-trip `proj₁ ∘ sound ∘ retract-to ≡ proj₁`, proved by `refl`. Witnesses the retraction direction holding definitionally on the A-component, as the design note (§5) predicts. Obligations deferred (out of scope for this rung): * §7 #7 zero-collapse under separation (`Separated → EchoR zero f y → Echo f y`) — needs a separation predicate on the pseudo-metric record that callers can opt into. * §7 #8 axis-1 shadow agreement — cross-axis classification, separate rung. * Full retract B-component and tolerance-budget round-trip — needs a `+`-left-identity axiom on `Tolerance` (`zero + ε ≡ ε`) which the current record does not supply. Adding it is a separate decision (it commits the carrier to a left-unital monoid, not just an ordered-+-monotone-monoid). * Lipschitz generalisation (`L_g ≠ 1`) — needs scalar multiplication on `Tol`. Docs updated: * `docs/echo-types/composition.md` §Q3 — promoted from "entirely speculative" to landed-retract-shape with the deferred items called out. * `docs/echo-types/roadmap.md` — new "landed" entry for the composition rung first slice. Invariants preserved: `--safe --without-K`, no postulates, no escape pragmas, funext untouched. `Smoke.agda` already pins `module Approx` following the existing convention (per-lemma pins inside parameterised modules require instantiation, which the project does not do for EchoApprox). Build: `LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda` and `... Smoke.agda` both exit 0. Refs `docs/echo-types/roadmap.md` Axis 2 entry. Refs `docs/echo-types/composition.md` §Q3. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/echo-types/composition.md | 23 +++++- docs/echo-types/roadmap.md | 16 ++++ proofs/agda/EchoApprox.agda | 132 +++++++++++++++++++++++++++++++-- 3 files changed, 164 insertions(+), 7 deletions(-) diff --git a/docs/echo-types/composition.md b/docs/echo-types/composition.md index 89de929..f95f600 100644 --- a/docs/echo-types/composition.md +++ b/docs/echo-types/composition.md @@ -150,8 +150,27 @@ is a Lipschitz constant of `g`. This is a crude first guess — the right form may involve sup-norms, dilation-operators, or coarser bounds. -*Status.* Entirely speculative. Requires a formal definition of -approximate echo first. +*Status (updated).* No longer entirely speculative. The +non-expansive case (`L_g = 1`) is landed as +`EchoApprox.Approx.echo-approx-compose` in additive form +`(ε₁ + ε₂)-echo(g ∘ f)`. The compositional *shape* — whether the +forward/backward maps form a strict iso analogous to +`Echo-comp-iso` — is settled in the negative: it is a *retract*, +not an iso, because the RHS Σ admits multiple splits of the budget +and the chosen intermediate `b` is not pinned by the input. The +axis-2 design note (`/tmp/echo-types-exploration/axis2-approximate.md` +§5) gives the full discussion. + +First slice of the retract landed in `EchoApprox.agda`: +`echo-approx-comp-sound` (RHS-Σ → LHS via `echo-approx-compose`), +`echo-approx-comp-retract-to` (canonical-split LHS → RHS-Σ section +at `b := f x`, `ε₁ := zero`, `ε₂ := ε`), and +`echo-approx-comp-retract-A` (A-component round-trip preserves the +witness up to `refl`). The B-component round-trip and the +tolerance-budget round-trip need a `+`-left-identity axiom on +`Tolerance` (`zero + ε ≡ ε`) — not in the current record. The full +retract proof and the Lipschitz generalisation (`L_g ≠ 1`) are +deferred to subsequent rungs. ### Q4. Associativity — landed diff --git a/docs/echo-types/roadmap.md b/docs/echo-types/roadmap.md index fec174e..5de5624 100644 --- a/docs/echo-types/roadmap.md +++ b/docs/echo-types/roadmap.md @@ -92,6 +92,22 @@ Paths marked **[unblocked]** can proceed today. Paths marked (monotone in ε), and `echo-approx-compose` (additive composition under a non-expansive outer leg, realising the taxonomy §2 conjecture). Wired into `All.agda` and `Smoke.agda`. +- **[landed]** Composition rung first slice (Axis 2): the §Q3 + retract-shape. `EchoApprox.agda` now also ships + `echo-strict→approx` (general strict ⇒ zero-tolerance, generalises + `echo-approx-intro` from own-fibre to arbitrary `y` via the + codomain equation), `echo-approx-comp-sound` (RHS-Σ → LHS via + `echo-approx-compose`), `echo-approx-comp-retract-to` + (canonical-split LHS → RHS-Σ section, picking `b := f x`, + `ε₁ := zero`, `ε₂ := ε`), and `echo-approx-comp-retract-A` (the + A-component round-trip `proj₁ ∘ sound ∘ retract-to ≡ proj₁`, + proved by `refl`). The retraction direction on the A-witness holds + definitionally as the design note (§5) predicts. The B-component + and tolerance-budget round-trips are deferred to a subsequent + rung — they need a `+`-left-identity axiom on `Tolerance` + (`zero + ε ≡ ε`) which the current record does not supply. + §7 obligations 7 (separated zero-collapse) and 8 (axis-1 shadow + agreement) likewise deferred. - **[landed]** Per-decoration composition lemmas across the five-decoration family — **sweep complete** (2026-04-28): `EchoGraded.degrade-compose`, `EchoLinear.degradeMode-compose`, diff --git a/proofs/agda/EchoApprox.agda b/proofs/agda/EchoApprox.agda index 342456a..9cfff76 100644 --- a/proofs/agda/EchoApprox.agda +++ b/proofs/agda/EchoApprox.agda @@ -12,23 +12,48 @@ -- -- Headline lemmas: -- --- * echo-approx-intro -- exact match is a zero-tolerance approximate echo --- * echo-approx-relax -- ε is monotone: ε₁ ≤ ε₂ ⇒ EchoR ε₁ ⊑ EchoR ε₂ --- * echo-approx-compose -- non-expansive composition with additive error, --- realising the taxonomy §2 conjecture +-- * echo-approx-intro -- exact own-fibre match is zero-tolerance +-- * echo-strict→approx -- general strict ⇒ zero-tolerance (any y) +-- * echo-approx-relax -- ε is monotone: ε₁ ≤ ε₂ ⇒ EchoR ε₁ ⊑ EchoR ε₂ +-- * echo-approx-compose -- non-expansive composition with additive +-- error, realising the taxonomy §2 conjecture +-- * echo-approx-comp-sound -- repackages compose into the retract RHS-Σ +-- shape from `composition.md` §Q3 (§5 of the +-- axis-2 design note) +-- * echo-approx-comp-retract-to -- canonical-split LHS → RHS section: +-- picks b := f x, ε₁ := zero, ε₂ := ε +-- * echo-approx-comp-retract-A -- A-component round-trip (sound ∘ retract-to) +-- preserves the A-witness up to `refl`, +-- witnessing the retraction direction +-- definitionally -- -- The non-expansiveness side condition on the outer leg is the -- minimal hypothesis under which tolerances accumulate additively; -- without it the conjecture has no general proof (an amplifying -- second leg can blow ε₁ up arbitrarily on the way through). +-- +-- Composition-track context (§5 of the axis-2 design note, +-- `/tmp/echo-types-exploration/axis2-approximate.md`). The approximate +-- analogue of `Echo-comp-iso` is a *retraction*, not a strict +-- isomorphism: the RHS Σ-shape admits multiple splits of the ε +-- budget and the chosen intermediate `b` is not pinned by the input. +-- This module ships the first slice of that retract — soundness (#6), +-- the canonical-split forward section, and an A-component round-trip +-- witness. The B-component round-trip and the full tolerance round-trip +-- need a `+`-left-identity axiom on `Tolerance` (`zero + ε ≡ ε`, not +-- currently in the record); §7 obligations 7 (zero-collapse under +-- separation) and 8 (axis-1 shadow agreement) are deferred to +-- subsequent rungs. module EchoApprox where open import Level using (Level; _⊔_; suc) open import Function.Base using (_∘_; id) -open import Data.Product.Base using (Σ; _,_; proj₁; proj₂) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst) +open import Echo using (Echo) + ---------------------------------------------------------------------- -- Tolerance carrier and pseudo-metric structure ---------------------------------------------------------------------- @@ -89,6 +114,28 @@ module Approx echo-approx-intro f x = x , subst (_≤ zero) (sym (dist-self (f x))) ≤-refl + ---------------------------------------------------------------------- + -- Headline 1ʹ: general strict ⇒ zero-tolerance approximate. + -- + -- Realises §7 obligation 2 of the axis-2 design note: every strict + -- echo `Echo f y` lifts to a zero-tolerance approximate echo + -- `EchoR zero f y` (any y, not just own-fibre points). When `y ≡ f x` + -- with `p ≡ refl` this collapses to `echo-approx-intro`; otherwise + -- the codomain equation `p : f x ≡ y` is used to transport the + -- self-distance bound from `(f x, f x)` to `(f x, y)`. + -- + -- This generalises `echo-approx-intro` from own-fibre points + -- `(f x)` to arbitrary `y` reached via a strict echo. The cost of + -- the generalisation is one extra `subst` along `p`. + ---------------------------------------------------------------------- + + echo-strict→approx : + ∀ {f : A → B} {y : B} → Echo f y → EchoR zero f y + echo-strict→approx {f = f} (x , p) = + x , subst (λ z → dist (f x) z ≤ zero) + p + (subst (_≤ zero) (sym (dist-self (f x))) ≤-refl) + ---------------------------------------------------------------------- -- Headline 2: tolerance is monotone in `ε`. A tighter approximation -- is also a looser one. The proof is one transitivity step. @@ -139,3 +186,78 @@ module Approx bound : dist (g (f x)) y ≤ (ε₁ + ε₂) bound = ≤-trans leg contract + + ---------------------------------------------------------------------- + -- Retraction-shaped composition (composition.md §Q3 / design-note §5). + -- + -- The approximate analogue of `Echo-comp-iso` is *retract-shaped*: + -- + -- LHS := EchoR ε (g ∘ f) y + -- RHS := Σ B (λ b → EchoR ε₁ f b × dist (g b) y ≤ ε₂) + -- + -- with the budget split `ε = ε₁ + ε₂`. The RHS admits multiple + -- splits of the budget and the chosen intermediate `b` is not + -- pinned by the input, so a full iso fails by design. What does + -- hold is a retraction: a forward section that picks a canonical + -- representative on the RHS and a backward map (`echo-approx-comp-sound`, + -- a thin repackaging of `echo-approx-compose`) that round-trips + -- the A-witness definitionally. + -- + -- This block lands the first slice: soundness (#6), the canonical- + -- split forward section, and the A-component round-trip. The + -- B-component and tolerance-budget round-trips need a `+`-left- + -- identity axiom on `Tolerance` (`zero + ε ≡ ε`, not in the record). + ---------------------------------------------------------------------- + + -- §7 obligation 6: sound RHS-to-LHS direction. + -- Unpacks the existential and calls `echo-approx-compose`. + echo-approx-comp-sound : + ∀ {ε₁ ε₂ : Tol} + (f : A → B) (g : B → B) → + NonExpansive g → + ∀ {y : B} → + Σ B (λ b → EchoR ε₁ f b × dist (g b) y ≤ ε₂) → + EchoR (ε₁ + ε₂) (g ∘ f) y + echo-approx-comp-sound f g g-nonexp (b , ef , dgby≤ε₂) = + echo-approx-compose f g g-nonexp {b = b} ef dgby≤ε₂ + + -- Canonical-split LHS-to-RHS section of the retract. + -- + -- Given an `EchoR ε (g ∘ f) y` witness `(x , p : dist (g (f x)) y ≤ ε)`, + -- produce the RHS Σ-shape at the canonical split `(ε₁, ε₂) := (zero, ε)`: + -- + -- * intermediate `b := f x` (the canonical lift), + -- * inner echo `EchoR zero f (f x)` via `echo-approx-intro`, + -- * outer bound is just the original `p`. + -- + -- This is the "section" half of the retract: a one-sided splitting + -- of the §Q3 conjecture that always exists, with no extra hypothesis + -- beyond what `EchoR ε (g ∘ f) y` already supplies. The "wrong" + -- intermediates are not enumerable, which is precisely why the + -- approximate analogue is a retract and not a full iso. + echo-approx-comp-retract-to : + ∀ {ε : Tol} (f : A → B) (g : B → B) {y : B} → + EchoR ε (g ∘ f) y → + Σ B (λ b → EchoR zero f b × dist (g b) y ≤ ε) + echo-approx-comp-retract-to f g (x , dgfx≤ε) = + f x , echo-approx-intro f x , dgfx≤ε + + -- A-component round-trip. Starting from an `EchoR ε (g ∘ f) y`, + -- pushing through the canonical-split section then through + -- soundness lands back on the *same A-witness `x`* (the tolerance + -- budget weakens from `ε` to `zero + ε`, which is why this is a + -- retraction in the A-component rather than a full equality of + -- echoes). The proof is `refl` — the A-component is preserved + -- definitionally because every step of the round-trip keeps + -- `proj₁` pinned to the original `x`. + -- + -- This pins the "retract direction holds definitionally" promise + -- of the design note: the witness-on-A round-trips on the nose, + -- even though the tolerance and intermediate-B components do not. + echo-approx-comp-retract-A : + ∀ {ε : Tol} (f : A → B) (g : B → B) (g-nonexp : NonExpansive g) + {y : B} (e : EchoR ε (g ∘ f) y) → + proj₁ (echo-approx-comp-sound f g g-nonexp + (echo-approx-comp-retract-to f g e)) + ≡ proj₁ e + echo-approx-comp-retract-A f g g-nonexp (x , _) = refl