proof(architecture): RankMonoUnion umbrella over source-rule extensions

[hyperpolymath]

Summary

Realises the architectural recommendation from PR #167's closing note: the future bplus-chain rank-mono umbrella shipped as a UNION OF SOURCE-RULE EXTENSIONS rather than a single enriched rank function. Zero new proof obligations; purely structural composition via Sum + `[,]` mediator. `--safe --without-K`, no postulates, no funext.

What the union umbrella ships

Name	Type	Role
`<ᵇᵘ`	`BT → BT → Set`	Disjoint sum of `<ᵇ¹` (Slice 3) and `<ᵇ⁺²` (Path-3)
`rank-pow-mono-<ᵇᵘ`	`∀ {x y} → x <ᵇᵘ y → rank-pow x <′ rank-pow y`	Coproduct mediator via `[,]` — ONE LINE
`<ᵇᵘ-from-<ᵇ¹` / `<ᵇᵘ-from-<ᵇ⁺²` / `<ᵇᵘ-from-<ᵇ⁰` (+symmetric)	embeddings	Convenience injections

The architectural design

PR #167's closing observation:

The future bplus-chain rank-mono umbrella may want to be designed as a UNION OF SOURCE-RULE EXTENSIONS (Path-3 style for cleanly-decomposable cases) rather than a single enriched rank function (rank-lex-jb style for cross-head cases).

This PR mechanises that recommendation. Each contributing extension keeps its own proof obligation local; the union dispatches via case analysis on which extension witnesses the relation. The mediator is `[ rank-pow-mono-<ᵇ¹ , rank-pow-mono-<ᵇ⁺² ]` — a single `[,]` over the existing per-extension umbrellas.

Why this architectural shape (three observations)

1. Different sub-cases prefer different rank-mono machinery. Strict-head joint-bplus closes via head-Ω + `ω-rank-pow-succ`; same-left closes via `rank-pow-bplus-right-mono`; cross-head rank-equal closes at LEX-RANK via rank-lex-jb. No single rank function dominates.

2. Source-rule enrichment is structurally simpler than rank-function enrichment (Path-3 verdict, PR proof(Path-3 prototype): same-left joint-bplus rank-mono extension #167). The consumer-side first-eq derivation that rank-lex-jb requires (PR proof(Slice 3+4 Route A): (c) trichotomy + consumer-side first-eq derivation #166 (c) trichotomy + first-eq) gets bypassed entirely when the source rule carries the discriminator.

3. Union of extensions scales. Every new sub-case ships as its own extension module with its own rank-mono theorem, then unions in mechanically. No interference between extensions; closure is local.

Extension recipe (for future contributors)

Documented in the module preamble. To add a new source-rule extension:

1. Define the relation + rank-pow-mono in its own module (use `RankMonoSameLeft` as canonical template).
2. Re-export through `Ordinal/Buchholz/Smoke.agda` with its own `using` block.
3. Update this module to extend `<ᵇᵘ` with the new disjunct and extend `rank-pow-mono-<ᵇᵘ` with the new case via `[,]`.

Both edits mechanical; no new proof obligations.

Honest scope (preserved in module preamble)

• Does NOT wrap with WfCNF endpoints (à la `RankMonoUmbrellaSlice4.<ᵇ⁻ⁿ`).
• Does NOT include rank-lex-jb discharge — cross-head rank-equal case lives at LEX-RANK level, different rank-relation. Union is over `rank-pow <′` discharges only.
• Does NOT prove well-foundedness of the union — orthogonal to rank-mono.

Slice 3+4 Route A arc summary (4 PRs total)

After this PR the session arc is closed:

PR	Role
#165	(b) `<lex-first` primitive + bpsi sub-case discharge
#166	(c) trichotomy data type + first-eq derivation
#167	Path-3 prototype (same-left source-rule extension)
THIS PR	RankMonoUnion (architectural realisation)

The full bplus-chain rank-mono umbrella over all 13 `<ᵇ` constructors is still gated on (i) tail-rank-equality discharge for the bpsi-source-at-equal-head case AND (ii) the cross-head rank-equal case via rank-lex-jb's structural research; neither is closed by this PR. The architecture is now in place for those closures to plug in mechanically.

Local verification

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

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

Test plan

• All Agda lanes typecheck under `--safe --without-K` with zero postulates.
• Foundation guardrail + kernel-guard pass with 162 modules.
• 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