proof: WfCNF wrap of the RankMonoUnion umbrella

[hyperpolymath]

Summary

Stacked on #168. Mirrors `RankMonoUmbrellaSlice4.<ᵇ⁻ⁿ`'s WfCNF-bundling pattern over `RankMonoUnion.<ᵇᵘ` from #168. Provides the canonical-form invariant downstream Buchholz consumers need alongside the rank-relation. Zero new proof obligations; `--safe --without-K`, no postulates, no funext.

What ships

Name	Type	Role
`<ᵇᵘⁿ`	record (WfCNF + WfCNF + `<ᵇᵘ`)	WfCNF-narrowed union relation
`mk<ᵇᵘⁿ`	record constructor	Bundling combinator
`<ᵇᵘⁿ-from-<ᵇ⁰` / `<ᵇᵘⁿ-from-<ᵇ¹` / `<ᵇᵘⁿ-from-<ᵇ⁺²`	embeddings	Constructor-level uplifts under WfCNF endpoints
`rank-pow-mono-<ᵇᵘⁿ`	rank-mono theorem	One-liner forwarding through bundled `<ᵇᵘ-d`

Architectural payoff preserved

The "union of extensions" pattern from #168 extends through the WfCNF wrap automatically. Future contributors adding a new source-rule extension `<ᵇⁿ`:

1. Edit `RankMonoUnion` to extend `<ᵇᵘ` with the new disjunct + `rank-pow-mono-<ᵇᵘ` with the new case.
2. This module updates AUTOMATICALLY — no edit needed.

Per-extension proof work + structural composition. No proof obligations multiply across the WfCNF boundary either.

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

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

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.

Six new names pinned in `Ordinal/Buchholz/Smoke.agda`.

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 AFTER proof(architecture): RankMonoUnion umbrella over source-rule extensions #168 merges (stacked).

🤖 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