|
26 | 26 | -- preserves the A-witness up to `refl`, |
27 | 27 | -- witnessing the retraction direction |
28 | 28 | -- definitionally |
| 29 | +-- * Separated -- separation predicate on a pseudo-metric: |
| 30 | +-- `dist b₁ b₂ ≤ zero → b₁ ≡ b₂` |
| 31 | +-- * echo-approx-zero-collapses-strict -- §7 #7: under separation, an |
| 32 | +-- ε≡zero approximate echo IS a |
| 33 | +-- strict echo |
| 34 | +-- * echo-shadow-A -- §7 #8 axis-1 shadow: the underlying |
| 35 | +-- A-witness of an approximate echo; |
| 36 | +-- `echo-strict→approx` agrees with the |
| 37 | +-- strict A-witness on the nose |
| 38 | +-- * echo-shadow-iso-to / -from -- §7 #8 trivial repackaging of `EchoR` |
| 39 | +-- as an existential `Σ A (λ x → dist |
| 40 | +-- (f x) y ≤ ε)` (definitional both ways) |
| 41 | +-- * echo-strict→approx-shadow-A -- the A-component of `echo-strict→approx` |
| 42 | +-- equals the strict A-component (refl) |
29 | 43 | -- |
30 | 44 | -- The non-expansiveness side condition on the outer leg is the |
31 | 45 | -- minimal hypothesis under which tolerances accumulate additively; |
|
41 | 55 | -- the canonical-split forward section, and an A-component round-trip |
42 | 56 | -- witness. The B-component round-trip and the full tolerance round-trip |
43 | 57 | -- need a `+`-left-identity axiom on `Tolerance` (`zero + ε ≡ ε`, not |
44 | | --- currently in the record); §7 obligations 7 (zero-collapse under |
45 | | --- separation) and 8 (axis-1 shadow agreement) are deferred to |
46 | | --- subsequent rungs. |
| 58 | +-- currently in the record); see the `Tolerance` design-decision note |
| 59 | +-- in the PR body for two options (interface extension vs. additive |
| 60 | +-- `BalancedTolerance` record). §7 obligations 7 (separated zero-collapse) |
| 61 | +-- and 8 (axis-1 shadow agreement) are now landed below. Rung C |
| 62 | +-- (full B-component + tolerance round-trip) is deferred pending the |
| 63 | +-- design call. Rung D (Lipschitz `L_g ≠ 1`) is deferred — it requires |
| 64 | +-- multiplication on `Tolerance`, another interface call. |
47 | 65 |
|
48 | 66 | module EchoApprox where |
49 | 67 |
|
@@ -261,3 +279,104 @@ module Approx |
261 | 279 | (echo-approx-comp-retract-to f g e)) |
262 | 280 | ≡ proj₁ e |
263 | 281 | echo-approx-comp-retract-A f g g-nonexp (x , _) = refl |
| 282 | + |
| 283 | + ---------------------------------------------------------------------- |
| 284 | + -- §7 obligation 7: separated zero-collapse. |
| 285 | + -- |
| 286 | + -- A pseudo-metric is *separated* when zero distance implies |
| 287 | + -- propositional equality on the carrier. Pseudo-metrics in general |
| 288 | + -- only guarantee `dist y y ≡ zero`; the converse (a metric proper) |
| 289 | + -- is an extra hypothesis the `PseudoMetric` record deliberately |
| 290 | + -- does not bake in. Callers who need the converse supply a |
| 291 | + -- `Separated` witness explicitly at the lemma site. |
| 292 | + -- |
| 293 | + -- Under that hypothesis, the strict-vs-approximate gap closes at |
| 294 | + -- ε = zero: any zero-tolerance approximate echo IS a strict echo, |
| 295 | + -- with the same A-witness on the nose. This realises §7 #7 of the |
| 296 | + -- axis-2 design note and the §4 "Approximate → strict (only when |
| 297 | + -- separated, at ε = 0)" statement. |
| 298 | + -- |
| 299 | + -- Without separation the converse fails by design — multiple `x`s |
| 300 | + -- may share zero distance to `y` without `f x ≡ y` on the nose. |
| 301 | + -- That is the point of an approximate echo. |
| 302 | + ---------------------------------------------------------------------- |
| 303 | + |
| 304 | + Separated : Set (b ⊔ ℓ) |
| 305 | + Separated = ∀ b₁ b₂ → dist b₁ b₂ ≤ zero → b₁ ≡ b₂ |
| 306 | + |
| 307 | + echo-approx-zero-collapses-strict : |
| 308 | + Separated → |
| 309 | + ∀ {f : A → B} {y : B} → EchoR zero f y → Echo f y |
| 310 | + echo-approx-zero-collapses-strict sep {f = f} {y = y} (x , dfx≤0) = |
| 311 | + x , sep (f x) y dfx≤0 |
| 312 | + |
| 313 | + ---------------------------------------------------------------------- |
| 314 | + -- §7 obligation 8: axis-1 shadow agreement. |
| 315 | + -- |
| 316 | + -- The "shadow" of an approximate echo is its underlying A-witness — |
| 317 | + -- the projection that forgets the metric-bound proof. Two flavours: |
| 318 | + -- |
| 319 | + -- * `echo-shadow-A` — extracts the A-witness from an |
| 320 | + -- approximate echo (definitional, |
| 321 | + -- the existing `proj₁`). |
| 322 | + -- |
| 323 | + -- * `echo-shadow-iso-{to,from}` — the trivial repackaging of |
| 324 | + -- `EchoR ε f y` as the existential |
| 325 | + -- `Σ A (λ x → dist (f x) y ≤ ε)`. |
| 326 | + -- Both directions are `id` because |
| 327 | + -- the two shapes are definitionally |
| 328 | + -- equal; the iso lemma here pins |
| 329 | + -- the §7 #8 obligation explicitly. |
| 330 | + -- |
| 331 | + -- * `echo-strict→approx-shadow-A` — axis-1 / axis-2 cross-check: |
| 332 | + -- `echo-strict→approx` preserves |
| 333 | + -- the A-component on the nose |
| 334 | + -- (`refl`). This is the |
| 335 | + -- definitional version of "the |
| 336 | + -- strict→approx inclusion and the |
| 337 | + -- A-shadow projection cohere" |
| 338 | + -- from the user-prompt framing. |
| 339 | + -- |
| 340 | + -- Together these say: the A-component is a genuine axis-1 invariant |
| 341 | + -- of approximate echoes — every move in the axis-2 calculus that |
| 342 | + -- keeps the A-witness fixed (intro, strict→approx, relax, |
| 343 | + -- canonical-split retract section) preserves the axis-1 shadow |
| 344 | + -- definitionally. |
| 345 | + ---------------------------------------------------------------------- |
| 346 | + |
| 347 | + echo-shadow-A : |
| 348 | + ∀ {ε : Tol} {f : A → B} {y : B} → EchoR ε f y → A |
| 349 | + echo-shadow-A = proj₁ |
| 350 | + |
| 351 | + -- Forward: an approximate echo IS an existential with metric bound. |
| 352 | + -- Definitionally `id`; the lemma pins the axis-1 shadow obligation. |
| 353 | + echo-shadow-iso-to : |
| 354 | + ∀ {ε : Tol} {f : A → B} {y : B} → |
| 355 | + EchoR ε f y → Σ A (λ x → dist (f x) y ≤ ε) |
| 356 | + echo-shadow-iso-to e = e |
| 357 | + |
| 358 | + echo-shadow-iso-from : |
| 359 | + ∀ {ε : Tol} {f : A → B} {y : B} → |
| 360 | + Σ A (λ x → dist (f x) y ≤ ε) → EchoR ε f y |
| 361 | + echo-shadow-iso-from e = e |
| 362 | + |
| 363 | + -- A-component of `echo-strict→approx` agrees with the strict |
| 364 | + -- A-component on the nose. The transport in `echo-strict→approx` |
| 365 | + -- only touches the bound proof, never the A-witness. |
| 366 | + echo-strict→approx-shadow-A : |
| 367 | + ∀ {f : A → B} {y : B} (e : Echo f y) → |
| 368 | + echo-shadow-A (echo-strict→approx e) ≡ proj₁ e |
| 369 | + echo-strict→approx-shadow-A (x , _) = refl |
| 370 | + |
| 371 | + -- Round-trip: under separation, `echo-approx-zero-collapses-strict` |
| 372 | + -- and `echo-strict→approx` are mutually A-inverse at ε = zero, |
| 373 | + -- definitionally on the A-component. This closes the §4 statement |
| 374 | + -- "Approximate → strict (only when separated, at ε = 0)" with a |
| 375 | + -- definitional witness on the axis-1 shadow. |
| 376 | + echo-strict→approx-collapse-shadow-A : |
| 377 | + (sep : Separated) → |
| 378 | + ∀ {f : A → B} {y : B} (e : Echo f y) → |
| 379 | + proj₁ (echo-approx-zero-collapses-strict sep |
| 380 | + (echo-strict→approx e)) |
| 381 | + ≡ proj₁ e |
| 382 | + echo-strict→approx-collapse-shadow-A sep (x , _) = refl |
0 commit comments