theory: EchoApprox deeper rung — separated zero-collapse + axis-1 shadow

[hyperpolymath]

Summary

Picks up two of three §7 deferrals from PR #70 in
/tmp/echo-types-exploration/axis2-approximate.md. Refs not Closes
because §7 is multi-rung and one rung (B-component +
tolerance-budget retract round-trip) stays deferred pending a
Tolerance interface design call (see below).

Rungs landed

Rung A — separated zero-collapse (§7 #7)

• Separated : Set — separation predicate on the pseudo-metric:
  ∀ b₁ b₂ → dist b₁ b₂ ≤ zero → b₁ ≡ b₂. Kept out of the
  PseudoMetric record; supplied as an explicit hypothesis at the
  lemma site (pseudo-metrics in general only guarantee dist y y ≡ zero, not the converse — making them a metric proper is an
  optional refinement the record deliberately does not bake in).
• echo-approx-zero-collapses-strict : Separated → EchoR zero f y → Echo f y
  formalises the §4 "Approximate → strict (only when separated, at
  ε = 0)" statement.

Rung B — axis-1 shadow agreement (§7 #8)

• echo-shadow-A — A-component projection (axis-1 shadow of an
  approximate echo).
• echo-shadow-iso-{to,from} — pins the §7 E6/E7: add Buchholz well-formed targets and EchoOrdinal bridge #8 obligation
  explicitly (definitional both ways: EchoR ε f y IS the
  existential Σ A (λ x → dist (f x) y ≤ ε)).
• echo-strict→approx-shadow-A — cross-axis cohere: the
  A-component of echo-strict→approx agrees with the strict
  A-component on the nose (refl).
• echo-strict→approx-collapse-shadow-A — round-trip under
  separation: zero-collapses-strict ∘ strict→approx ≡ id on the
  A-component, definitionally.

DESIGN-DECISION STOP — Rung C deferred

The full B-component + tolerance-budget retract round-trip
(echo-approx-comp-retract-from-to and friends) requires a
+-left-identity axiom on Tolerance (zero + ε ≡ ε, plus
right-identity for the symmetric variants).

Current shape of Tolerance

record Tolerance ℓ : Set (suc ℓ) where
  field
    Tol      : Set ℓ
    zero     : Tol
    _+_      : Tol → Tol → Tol
    _≤_      : Tol → Tol → Set ℓ
    ≤-refl   : ∀ {ε}             → ε ≤ ε
    ≤-trans  : ∀ {ε₁ ε₂ ε₃}      → ε₁ ≤ ε₂ → ε₂ ≤ ε₃ → ε₁ ≤ ε₃
    +-mono-≤ : ∀ {a b c d}       → a ≤ b → c ≤ d → (a + c) ≤ (b + d)

No identity laws on +. Minimal interface, lets us state
echo-approx-compose; that's all it currently does.

What needs to be added

For the symmetric retract round-trip:

+-identityˡ : ∀ {ε} → (zero + ε) ≡ ε
+-identityʳ : ∀ {ε} → (ε + zero) ≡ ε

(≡, not ≤ — the round-trip is a definitional retract on the
tolerance budget, so we need a propositional equality, not just
mutual ≤.)

Two options

(a) Extend Tolerance with the two identity-law fields.

• Pro: minimal scaffolding; one type to thread through.
• Con: ripples to every Tolerance instance — currently just
  EchoApproxInstance.trivialTolerance (trivial discharge), but
  consumers may grow. Makes Tolerance strictly stronger than
  the "ordered commutative-monoid-flavoured" framing in §3 of the
  axis-2 design note.

(b) Add a separate BalancedTolerance record on top of
Tolerance carrying just the identity laws.

• Pro: additive; no interface breakage; layered/opt-in. Matches
  the design pattern of PseudoMetric (which is separately
  refined to a metric by adding Separated, not by widening the
  base record). Keeps the §3 "minimal moving parts" promise.
• Con: an extra record name to thread through retract-round-trip
  lemmas.

Recommendation

(b). The current Tolerance is deliberately the minimal
interface that lets us state echo-approx-compose (triangle +
additive monotonicity, nothing else). Identity laws are needed
only by the retract round-trip, which is a downstream refinement
— keeping them out of the core interface preserves the "minimal
moving parts" design from §3 of the axis-2 design note. The
analogue is PseudoMetric vs. (PseudoMetric + Separated):
the refinement lives outside the base record.

Rung C is deferred pending owner decision.

Rung D — also deferred

The Lipschitz generalisation L_g ≠ 1 would need scalar
multiplication on Tolerance — a third interface call (whether
to add it to the core record, or layer a ScalableTolerance
refinement). Deferred alongside Rung C; same recommendation shape
applies.

Hygiene

All new headlines pinned via the per-lemma proof-of-life pattern
from PR #71: EchoApproxInstance.agda adds top-level identifiers
at the trivial-pseudometric-on-⊤ instance, Smoke.agda
enumerates them in its using clause.

Verification

$ agda -i proofs/agda proofs/agda/All.agda     # exit 0
$ agda -i proofs/agda proofs/agda/Smoke.agda   # exit 0

--safe --without-K throughout. No postulates. No escape pragmas.
No funext.

Refs

• PR theory: EchoApprox composition rung — first slice (retract direction) #70 (retract direction)
• /tmp/echo-types-exploration/axis2-approximate.md §7

Refs not Closes — §7 obligations 7 and 8 are landed, but
obligation 6's "full retract round-trip" (Rung C) and the
Lipschitz generalisation remain.

Test plan

• agda proofs/agda/All.agda exits 0
• agda proofs/agda/Smoke.agda exits 0
• No postulates / escape pragmas / funext introduced
• All new headlines pinned in Smoke.agda via EchoApproxInstance
• Owner decides Rung C Tolerance interface question (a vs. b)
• After decision: implement chosen option, land full retract
  round-trip

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 10 issues detected

Severity	Count
🔴 Critical	0
🟠 High	5
🟡 Medium	5

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/cache@v4 needs attention",
    "type": "unpinned_action",
    "file": "agda.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "No dependabot.yml or renovate.json found in echo-types",
    "type": "DependencyUpdate",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "high",
    "remediation": "Add .github/dependabot.yml or renovate.json configuration.",
    "scorecard_check": "Dependency-Update-Tool"
  },
  {
    "reason": "Nominal-only SAST in echo-types: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "1 workflow(s) with tag-pinned (not SHA-pinned) actions in echo-types",
    "type": "DependencyPinning",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Pin GitHub Actions and Docker base images by SHA hash.",
    "scorecard_check": "Pinned-Dependencies"
  },
  {
    "reason": "Repository has 1 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence