proofs: db-theory carriers (#174, #176) + Veblen least-fixed-point rung

[hyperpolymath]

Summary

Three verified proof rungs (all --safe --without-K, zero postulates; All.agda + Smoke.agda exit 0; kernel-guard PASS).

db-theory consumer carriers

• Closes Add TransactionMutations module — instantiate no-section-of-collapsing-map for SQL transaction rollback safety (consumer: affinescript db-theory #2) #174 — EchoTransaction: SQL transaction rollback safety as a Security instance reducing to no-section-of-collapsing-map. A staged WriteSet is an affine resource; rollback collapses it to an information-free RollbackLog, so no pure function recovers the discarded writes (#DB-2.1). Honest matched-negatives (NOT durability / isolation / commit-dual / savepoint / runtime-memory).
• Closes Add EchoSelectiveProjection module — column-monotone predicate carrier for σ-π commutativity (consumer: affinescript db-theory #4) #176 — EchoSelectiveProjection: relational-algebra σ–π commutativity (Codd, subset case) as an Echo-fibre set-equality (_⇔_ of the two result relations per projected value). select-project-commute (column-safe ⇒ commute) + no-column-safe-lift (a projected-away-column predicate admits no column-restricted lift ⇒ σ/π don't commute). The issue's ↔/p (proj₁ e) sketch is corrected to the honest _⇔_ set-equality level.

Ordinal track — Bachmann–Howard climb, rung 7

• Ordinal.Brouwer.VeblenBinaryLeast: nextFix-least — the generic Veblen fixed-point engine is minimal (nextFix g x is the LEAST pre-fixed point of g strictly above x), the missing half of its correctness (the engine already had "is a fixed point" + "above x"). Payoff: Γ₀-fixed-from-closure reduces the open reverse direction φ_Γ₀(0) ≤′ Γ₀ to a single closure obligation commonStep (n ↦ φ_{Γ-tower n}) Γ₀ ≤′ Γ₀; combined with VeblenBinaryMono.Γ₀-prefixed (the ≤′ direction) that closure would yield the full bi-≤′ fixed point Γ₀ ≃ φ_Γ₀(0).

Honest scope

nextFix-least is unconditional. Γ₀-fixed-from-closure is conditional — it does not prove φ_Γ₀(0) ≤′ Γ₀, it reduces it to the still-open closure (needs general first-argument monotonicity / closure-from-above). Order-type fidelity ψ₀(Ω_ω) REMAINS OPEN (D-2026-06-14); no postulate is closed. (Note: #175, general aggregation, was found already landed upstream as EchoAggregation.)

Wiring / discipline

All three modules wired into All.agda and headline-pinned in Smoke.agda; the two Echo* modules classified in echo-kernel-note.adoc + MAP.adoc (kernel-guard Check B). Toolchain provisioned via scripts/provision-agda.sh (Agda 2.6.3 + stdlib 2.3 + absolute-zero); baseline All.agda confirmed green before and after.

🤖 Generated with Claude Code

https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs

---

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 8 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