Skip to content

Commit ed347df

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proof: WfCNF wrap of the RankMonoUnion umbrella (#169)
## 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 - [x] Module typechecks under \`--safe --without-K\` with zero postulates. - [x] Full suite + Smoke remain green with the new module wired in. - [ ] CI: \`check\` + \`cold-check\` + governance lanes green. - [ ] Auto-merge on green AFTER #168 merges (stacked). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 6e4a67a commit ed347df

3 files changed

Lines changed: 143 additions & 0 deletions

File tree

‎proofs/agda/All.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -152,6 +152,7 @@ open import Ordinal.Buchholz.RankMonoUmbrellaSlice4
152152
open import Ordinal.Buchholz.RankMonoSameLeft
153153
open import Ordinal.Buchholz.RankMonoUnion
154154
open import Ordinal.Buchholz.RankMonoUnionWF
155+
open import Ordinal.Buchholz.RankMonoUnionWfCNF
155156
open import Ordinal.Buchholz.RecursiveSurfaceOrder
156157
open import Ordinal.Buchholz.RecursiveSurfaceBudget
157158
open import Ordinal.Buchholz.SurfaceOrder

‎proofs/agda/Ordinal/Buchholz/RankMonoUnionWfCNF.agda‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
-- SPDX-License-Identifier: MPL-2.0
3+
-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
5+
-- WfCNF-wrapped variant of the union rank-mono umbrella (2026-05-30).
6+
--
7+
-- ## What this lands
8+
--
9+
-- Mirrors `Ordinal.Buchholz.RankMonoUmbrellaSlice4._<ᵇ⁻ⁿ_`'s
10+
-- WfCNF-bundling pattern over the union umbrella's `_<ᵇᵘ_` from
11+
-- `Ordinal.Buchholz.RankMonoUnion`. The narrowed relation
12+
-- `_<ᵇᵘⁿ_` bundles:
13+
--
14+
-- * `wf-x : WfCNF x` — source-side canonical-form witness
15+
-- * `wf-y : WfCNF y` — target-side canonical-form witness
16+
-- * `<ᵇᵘ-d : x <ᵇᵘ y` — the union derivation
17+
--
18+
-- The narrowed relation's `rank-pow-mono-<ᵇᵘⁿ` discharges via
19+
-- `rank-pow-mono-<ᵇᵘ` on the bundled derivation.
20+
--
21+
-- ## Why this exists
22+
--
23+
-- Downstream Buchholz consumers (e.g., the surface-route well-
24+
-- foundedness work in `Ordinal.Buchholz.RecursiveSurfaceOrder`)
25+
-- need the WfCNF invariant carried alongside the rank-relation
26+
-- so they don't have to re-discover it via separate proof
27+
-- structure. Slice 4's `_<ᵇ⁻ⁿ_` provides this for the strict-
28+
-- head joint-bplus extension; this module provides the
29+
-- analogous wrap for the full union umbrella.
30+
--
31+
-- ## Mechanical extension
32+
--
33+
-- This module is the WfCNF-wrap template for any future union
34+
-- extension that adds new source-rule slots. The recipe:
35+
--
36+
-- 1. Add the new disjunct to `_<ᵇᵘ_` in `RankMonoUnion`.
37+
-- 2. The mediator `rank-pow-mono-<ᵇᵘ` extends with the new
38+
-- case via `[_,_]`.
39+
-- 3. THIS MODULE updates AUTOMATICALLY because the record
40+
-- embeds the union's relation — no edit needed here.
41+
--
42+
-- The architectural payoff documented in `RankMonoUnion`'s
43+
-- preamble holds across the WfCNF wrap as well: per-extension
44+
-- proof work + structural composition.
45+
46+
module Ordinal.Buchholz.RankMonoUnionWfCNF where
47+
48+
open import Ordinal.Brouwer.Phase13 using (_<′_)
49+
open import Ordinal.Buchholz.Syntax using (BT)
50+
open import Ordinal.Buchholz.RankPow using (rank-pow)
51+
open import Ordinal.Buchholz.WellFormedCNF using (WfCNF)
52+
open import Ordinal.Buchholz.RankMonoUmbrella using (_<ᵇ⁰_)
53+
open import Ordinal.Buchholz.RankMonoUmbrellaSlice3 using (_<ᵇ¹_)
54+
open import Ordinal.Buchholz.RankMonoSameLeft using (_<ᵇ⁺²_)
55+
open import Ordinal.Buchholz.RankMonoUnion using
56+
( _<ᵇᵘ_
57+
; rank-pow-mono-<ᵇᵘ
58+
; <ᵇᵘ-from-<ᵇ¹
59+
; <ᵇᵘ-from-<ᵇ⁺²
60+
; <ᵇᵘ-from-<ᵇ⁰
61+
)
62+
63+
----------------------------------------------------------------------
64+
-- The WfCNF-narrowed union relation `_<ᵇᵘⁿ_`
65+
----------------------------------------------------------------------
66+
67+
-- Bundles WfCNF endpoints together with a `_<ᵇᵘ_` derivation.
68+
-- Same shape as `RankMonoUmbrellaSlice4._<ᵇ⁻ⁿ_` but over the
69+
-- union umbrella. The WfCNF fields are unused inside the
70+
-- rank-pow-mono closure but available to consumers reasoning
71+
-- about the canonical-form invariant of the endpoints (e.g.,
72+
-- downstream well-foundedness work).
73+
74+
record _<ᵇᵘⁿ_ (x y : BT) : Set where
75+
constructor mk<ᵇᵘⁿ
76+
field
77+
wf-x : WfCNF x
78+
wf-y : WfCNF y
79+
<ᵇᵘ-d : x <ᵇᵘ y
80+
81+
open _<ᵇᵘⁿ_ public
82+
83+
infix 4 _<ᵇᵘⁿ_
84+
85+
----------------------------------------------------------------------
86+
-- Constructor-level embeddings
87+
----------------------------------------------------------------------
88+
89+
-- Inherit any `_<ᵇ⁰_` derivation as a narrowed `_<ᵇᵘⁿ_`
90+
-- derivation under WfCNF endpoints. Forwards through the
91+
-- canonical `<ᵇ¹` embedding path of `_<ᵇᵘ_`.
92+
93+
<ᵇᵘⁿ-from-<ᵇ⁰ :
94+
∀ {x y} → WfCNF x → WfCNF y → x <ᵇ⁰ y → x <ᵇᵘⁿ y
95+
<ᵇᵘⁿ-from-<ᵇ⁰ wf-x wf-y p =
96+
mk<ᵇᵘⁿ wf-x wf-y (<ᵇᵘ-from-<ᵇ⁰ p)
97+
98+
-- Embed an `_<ᵇ¹_` derivation as a narrowed `_<ᵇᵘⁿ_` derivation.
99+
-- Covers the strict-head joint-bplus case via `<ᵇ¹-+1-+`.
100+
101+
<ᵇᵘⁿ-from-<ᵇ¹ :
102+
∀ {x y} → WfCNF x → WfCNF y → x <ᵇ¹ y → x <ᵇᵘⁿ y
103+
<ᵇᵘⁿ-from-<ᵇ¹ wf-x wf-y p =
104+
mk<ᵇᵘⁿ wf-x wf-y (<ᵇᵘ-from-<ᵇ¹ p)
105+
106+
-- Embed an `_<ᵇ⁺²_` derivation as a narrowed `_<ᵇᵘⁿ_` derivation.
107+
-- Covers the Path-3 same-left joint-bplus case via
108+
-- `<ᵇ⁺²-same-left`.
109+
110+
<ᵇᵘⁿ-from-<ᵇ⁺² :
111+
∀ {x y} → WfCNF x → WfCNF y → x <ᵇ⁺² y → x <ᵇᵘⁿ y
112+
<ᵇᵘⁿ-from-<ᵇ⁺² wf-x wf-y p =
113+
mk<ᵇᵘⁿ wf-x wf-y (<ᵇᵘ-from-<ᵇ⁺² p)
114+
115+
----------------------------------------------------------------------
116+
-- Rank-pow monotonicity
117+
----------------------------------------------------------------------
118+
119+
-- Forwards directly to `rank-pow-mono-<ᵇᵘ` via the bundled
120+
-- derivation. The WfCNF fields are unused inside the proof
121+
-- but available to consumers reasoning about the endpoints.
122+
-- Same shape as `RankMonoUmbrellaSlice4.rank-pow-mono-<ᵇ⁻ⁿ`.
123+
124+
rank-pow-mono-<ᵇᵘⁿ : ∀ {x y} → x <ᵇᵘⁿ y → rank-pow x <′ rank-pow y
125+
rank-pow-mono-<ᵇᵘⁿ p = rank-pow-mono-<ᵇᵘ (<ᵇᵘ-d p)

‎proofs/agda/Ordinal/Buchholz/Smoke.agda‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -617,3 +617,20 @@ open import Ordinal.Buchholz.RankMonoUnionWF using
617617
( wf-rank-pow-pullback
618618
; wf-<ᵇᵘ
619619
)
620+
621+
-- WfCNF wrap of the union umbrella 2026-05-30 (own block per
622+
-- CLAUDE.md Working rules): mirrors `RankMonoUmbrellaSlice4._<ᵇ⁻ⁿ_`'s
623+
-- WfCNF-bundling pattern over the union umbrella's `_<ᵇᵘ_`.
624+
-- Downstream Buchholz consumers needing the canonical-form
625+
-- invariant alongside the rank-relation use this narrowed form.
626+
-- The architectural-extension recipe documented in
627+
-- `RankMonoUnion`'s preamble automatically extends through this
628+
-- WfCNF wrap — new union disjuncts don't require edits here.
629+
open import Ordinal.Buchholz.RankMonoUnionWfCNF using
630+
( _<ᵇᵘⁿ_
631+
; mk<ᵇᵘⁿ
632+
; <ᵇᵘⁿ-from-<ᵇ⁰
633+
; <ᵇᵘⁿ-from-<ᵇ¹
634+
; <ᵇᵘⁿ-from-<ᵇ⁺²
635+
; rank-pow-mono-<ᵇᵘⁿ
636+
)

0 commit comments

Comments
 (0)