theory: EchoApprox composition rung — first slice (retract direction)

[hyperpolymath]

Summary

Extends proofs/agda/EchoApprox.agda with the first slice of the
axis-2 composition rung from the design note (drafted in
/tmp/echo-types-exploration/axis2-approximate.md, §7 obligations
2 + 6, plus the canonical-split retract direction). Refs
docs/echo-types/roadmap.md Axis 2 entry and docs/echo-types/composition.md
§Q3 — does not close either.

Obligations landed

• echo-strict→approx (§7 Claude/add ordinal notation layer 9qh sf #2). General strict ⇒ zero-tolerance
  approximate. Generalises echo-approx-intro from own-fibre points
  to arbitrary y via the codomain equation p : f x ≡ y. One
  extra subst along p.

• echo-approx-comp-sound (§7 E5: make ν operational and add Buchholz example/smoke modules #6). Sound RHS-to-LHS direction
  of the retract shape from composition.md §Q3 / 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, original bound for
  the outer.

• echo-approx-comp-retract-A. A-component round-trip
  proj₁ ∘ sound ∘ retract-to ≡ proj₁, proved by refl. The
  retraction direction holds definitionally on the A-component as
  the design note (§5) predicts.

Obligations deferred (out of this rung)

• §7 E5: add index monotonicity/inversion and psi0(Omega1) path #7 separated zero-collapse — needs a separation predicate on
  the PseudoMetric record.
• §7 E6/E7: add Buchholz well-formed targets and EchoOrdinal bridge #8 axis-1 shadow agreement — cross-axis classification.
• Full retract B-component and tolerance-budget round-trip — needs a
  +-left-identity axiom on Tolerance (zero + ε ≡ ε) not in the
  current record. Adding it commits the carrier to a left-unital
  monoid; deferred as a separate decision.
• 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 deferred items called out.
• docs/echo-types/roadmap.md adds a "landed" entry for the
  composition rung first slice.

Invariants preserved

• --safe --without-K
• No postulates
• No escape pragmas
• Funext untouched

Test plan

• LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda exits 0
• LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/Smoke.agda exits 0
• No new postulate, no escape pragmas, funext not imported
• Smoke.agda already pins module Approx following project
  convention (per-lemma pins inside parameterised modules require
  instantiation, which the project does not do for EchoApprox).

[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