feat: echo-approx-compose-lipschitz — Rung D (Lipschitz composition)

[hyperpolymath]

What

Closes Rung D (Lipschitz composition) that EchoApprox.agda deferred — generalising approximate-echo composition from a non-expansive outer leg (L = 1) to a Lipschitz leg with constant L.

How

The module's own note: "Rung D … requires multiplication on Tolerance, another interface call." Per your "do both", I resolved that interface call in favour of the repo's established pattern — a layered opt-in record, exactly like BalancedTolerance / Separated, leaving the base Tolerance minimal:

record LipschitzScale (T : Tolerance ℓ) where
  field _*_ : Tol → Tol → Tol
        *-monoʳ : ∀ {s a c} → a ≤ c → (s * a) ≤ (s * c)

Then, in a Lipschitz (S : LipschitzScale T) sub-module of Approx:

IsLipschitz L g = ∀ b₁ b₂ → dist (g b₁) (g b₂) ≤ (L * dist b₁ b₂)

echo-approx-compose-lipschitz :
  IsLipschitz L g → EchoR ε₁ f b → dist (g b) y ≤ ε₂ →
  EchoR ((L * ε₁) + ε₂) (g ∘ f) y

Same triangle + accumulate skeleton as echo-approx-compose; the non-expansive step dist (g·)(g·) ≤ dist · · becomes the Lipschitz step ≤ L * dist · ·, and *-monoʳ carries the inner bound dist (f x) b ≤ ε₁ through the constant to L * ε₁. It recovers echo-approx-compose at the corner L * ε ≡ ε.

Minimal by design: only _*_ + right-monotonicity are needed; associativity/identity/distributivity are left to richer carriers.

Discipline

• --safe --without-K, zero postulates.
• Trivial-⊤ LipschitzScale instance + 2 pins in EchoApproxInstance (the parameterised-module Smoke-pinning pattern); header "Rung D deferred" note flipped to LANDED.
• Verified on latest main: EchoApprox, EchoApproxInstance, Smoke.agda, All.agda all exit 0; kernel-guard.sh PASS (existing modules — no new module).

Context

This is gap 2-of-3 from the proof survey. Gap 3 (EchoSearch sequential composition) is next — it's a genuine product-search whose n₁ * n₂ bound provably requires a bound-dependent row-major pairing (DivMod), which I'm building now.

🤖 Generated with Claude Code

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 6 issues detected

Severity	Count
🔴 Critical	0
🟠 High	3
🟡 Medium	3

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": "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": "Repository has 6 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Scorecard): TokenPermissionsID -- Token-Permissions -- 18 day(s) old [STALE]",
    "type": "CSA001",
    "file": ".github/workflows/scorecard.yml",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code-scanning alert TokenPermissionsID (high) at .github/workflows/scorecard.yml is 18 days old (threshold: 7 days) -- overdue for remediation",
    "type": "CSA003",
    "file": ".github/workflows/scorecard.yml",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code-scanning alert hypatia/code_safety/agda_postulate dismissed as 'false positive' -- ensure dismissal is documented and justified",
    "type": "CSA004",
    "file": "proofs/agda/EchoImageFactorizationPropPostulated.agda",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence