ordinal(buchholz): head-Ω Slice 2 — ω-rank-pow-succ + fin-branch dominance

[hyperpolymath]

Summary

• Adds Slice 2 of the head-Ω domination route (Lane 3, follow-on to PR docs: refresh CHANGELOG/MAP/EXPLAINME/roadmap for 2026-05-27 work #124's Slice 1):
  • ω-rank-pow-succ : OmegaIndex → Ord — the per-marker "next ω-power up" target.
  • ω-rank-pow-succ-fin — definitional sanity at the fin branch.
  • ω-rank-pow-<-succ-fin — per-marker strict dominance at fin via ω^-strict-mono-suc (suc n).
  • rank-pow-bOmega-via-head-Ω, rank-pow-bpsi-via-head-Ω — atomic-rank refl-shape primitives factoring rank-pow through head-Ω.
• All five headlines pinned in Ordinal/Buchholz/Smoke.agda under their own using block with a header comment, per CLAUDE.md Working rules.

Obstruction note (inline in RankPow.agda)

The originally-proposed shape ω-rank-pow-succ ω = olim (λ n → ω^(suc(suc n))) (per CLAUDE.md §"Session arc 2026-05-27 late evening") represents the same ordinal as ω-rank-pow ω = olim (λ n → ω^(suc n)) — both are sup{ω^(n+1) : n ∈ ℕ} = ω^ω, with different ℕ-indexings of the same tail. Strict dominance at the ω branch therefore cannot hold under that shape.

Two follow-on slices are documented inline:

• Slice 2-omega. Replace the ω branch with a genuinely strictly-larger ordinal. Candidate: ω^(ω+1) = olim (λ n → (ω-rank-pow ω) ·ℕ n). Three cross-checks documented inline before committing the candidate — including a sanity check on the indexing's leading oz ⊕ (NOT definitionally ω-rank-pow ω under Brouwer's right-recursing _⊕_), which is the same hazard class as the original "same ordinal under different ℕ-indexing" issue.
• Slice 2-bplus (TODO(slice-2-bplus) marker inline). Prove the full rank-pow-dominated-by-head-Ω : (t : BT) → NonBzero t → WfCNF t → rank-pow t <′ ω-rank-pow-succ (head-Ω t) by structural recursion on WfCNF. The bplus case needs a rank-pow-mono-≤ᵇ companion for the original _<ᵇ_ (the WfCNF tail bound is _≤ᵇ_, not _≤ᵇ⁰_). Two options sketched; option (b) — head-Ω inversion that does not transitively depend on rank-mono — is preferred because it keeps rank-pow-dominated-by-head-Ω independent of the companion so a future signature change to one doesn't silently break the other.

Invariants held

• No postulates introduced.
• --safe --without-K throughout.
• scripts/kernel-guard.sh: PASS (funext-free certificate + classification-drift lint both clean).
• Branch state: 2 files changed (RankPow.agda, Buchholz/Smoke.agda).

Verification stance

CI is authoritative; inspection is auxiliary.agda is not available in this container, so I traced each addition by hand against the existing source (ω-rank-pow-succ-fin is refl over equal definitional unfoldings; ω-rank-pow-<-succ-fin n = ω^-strict-mono-suc (suc n) matches the lemma's signature directly; both *-via-head-Ω lemmas are refl over the existing provisional rank-pow (bpsi ν _) = ω-rank-pow ν shape). Lane 3 has burned this branch before with subtle definitional differences (the same-binder shapes, the blocked self-lift counterexample), so a CI red light must not be overridden by "but inspection passed".

Test plan

• CI Agda job typechecks All.agda + Smoke.agda clean under --safe --without-K.
• CI governance jobs pass.
• No regressions in pre-existing RankPow / HeadOmega consumers (RankMonoUmbrella, RankAdm, RankLex).

https://claude.ai/code/session_013nLEeKZXpvHnrDZMgRm19S

[github-actions]

🔍 Hypatia Security Scan

Findings: 56 issues detected

Severity	Count
🔴 Critical	10
🟠 High	27
🟡 Medium	19

⚠️Action Required: Critical security issues found!

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 secret-scanner.yml",
"type": "missing_workflow",
"file": "secret-scanner.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in governance.yml",
"type": "unknown",
"file": "governance.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in hypatia-scan.yml",
"type": "unknown",
"file": "hypatia-scan.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in mirror.yml",
"type": "unknown",
"file": "mirror.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard.yml",
"type": "unknown",
"file": "scorecard.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/provenance_debugging/ProvenanceDebugging.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/epistemic_erasure/EpistemicErasure.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
}
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence