proof: well-foundedness of _<ᵇᵘ_ via rank-embedding transport

[hyperpolymath]

Summary

Closes Gate 2 of the Slice 3+4 Route A session arc. Derives `WellFounded <ᵇᵘ` mechanically from `rank-pow-mono-<ᵇᵘ` (#168) and the existing `wf-<′` via the standard Subrelation + InverseImage transport pattern documented in `Ordinal.Buchholz.RankBrouwer`'s preamble. Zero new proof obligations; purely structural. `--safe --without-K`, no postulates, no funext.

The rank-embedding recipe

wf-rank-pow-pullback : WellFounded (λ x y → rank-pow x <′ rank-pow y)
wf-rank-pow-pullback = On.wellFounded rank-pow wf-<′

wf-<ᵇᵘ : WellFounded _<ᵇᵘ_
wf-<ᵇᵘ = Subrelation.wellFounded rank-pow-mono-<ᵇᵘ wf-rank-pow-pullback

Two steps:

1. `On.wellFounded` (= `InverseImage.wellFounded`) lifts well-foundedness of `<′` on `Ord` to the pullback `<′ on rank-pow` on `BT`.
2. `Subrelation.wellFounded` transports well-foundedness from the pullback to `<ᵇᵘ`, consuming `rank-pow-mono-<ᵇᵘ` as the witness that `<ᵇᵘ` is a sub-relation of the pullback.

The pattern is documented at `RankBrouwer.agda:55-56`.

Slice 3+4 Route A gate status after this PR

Gate	Status
1 — tail-rank-equality discharge (cross-head rank-equal case)	open (structural blocker)
2 — well-foundedness of `<ᵇᵘ`	CLOSED HERE
3 — Path-4 + further source-rule extensions	open (future-work, mechanical)

What this does NOT do

• Does NOT prove well-foundedness of the WfCNF-narrowed `<ᵇᵘⁿ` (proof: WfCNF wrap of the RankMonoUnion umbrella #169) separately — follows by the same Subrelation transport from `wf-<ᵇᵘ` via the canonical `<ᵇᵘⁿ → <ᵇᵘ` projection. Left for a thin follow-on if specifically needed.
• Does NOT add a Brouwer-rank embedding stronger than `rank-pow` — `rank-pow` is K-free + lands in `Ord` + already discharges the WF transport.

Local verification

• All four Agda lanes typecheck clean, exit 0.
• `bash tools/check-guardrails.sh proofs/agda` — 163 modules pass.
• `sh scripts/kernel-guard.sh` — PASS.

Two new names pinned in `Ordinal/Buchholz/Smoke.agda`: `wf-rank-pow-pullback`, `wf-<ᵇᵘ`.

Slice 3+4 Route A session arc (6 PRs)

PR	Layer
#165	rank-lex-jb (b) primitive
#166	rank-lex-jb (c) trichotomy + first-eq
#167	Path-3 same-left source-rule extension
#168	RankMonoUnion architecture
#169	WfCNF wrap of the union
THIS PR	WF of the union (Gate 2 closure)

Test plan

• Module typechecks under `--safe --without-K` with zero postulates.
• Full suite + Smoke remain green with the new module wired in.
• CI: `check` + `cold-check` + governance lanes green.
• Auto-merge on green.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 58 issues detected

Severity	Count
🔴 Critical	17
🟠 High	22
🟡 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 codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action rpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "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 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"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence