From 59beaab25ad45d5b76d0ad238b203f7567b815b0 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 15:47:44 +0100 Subject: [PATCH] proof: WfCNF wrap of the RankMonoUnion umbrella MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Mirrors `RankMonoUmbrellaSlice4._<ᵇ⁻ⁿ_`'s WfCNF-bundling pattern over `RankMonoUnion._<ᵇᵘ_` (PR #168). Provides the canonical-form invariant downstream Buchholz consumers need alongside the rank- relation. Zero new proof obligations; the rank-mono closure forwards through the bundled `_<ᵇᵘ_` derivation. `--safe --without-K`, no postulates, no funext. `record _<ᵇᵘⁿ_ (x y : BT) : Set` bundling: * `wf-x : WfCNF x` — source-side canonical-form witness * `wf-y : WfCNF y` — target-side canonical-form witness * `<ᵇᵘ-d : x <ᵇᵘ y` — the union derivation from `RankMonoUnion` Three constructor-level embeddings: `<ᵇᵘⁿ-from-<ᵇ⁰` (10 inherited cases), `<ᵇᵘⁿ-from-<ᵇ¹` (Slice 3 strict-head joint- bplus), `<ᵇᵘⁿ-from-<ᵇ⁺²` (Path-3 same-left joint-bplus). `rank-pow-mono-<ᵇᵘⁿ : ∀ {x y} → x <ᵇᵘⁿ y → rank-pow x <′ rank-pow y` forwards directly to `rank-pow-mono-<ᵇᵘ` via the bundled derivation. ONE LINE — same shape as Slice 4's `rank-pow-mono-<ᵇ⁻ⁿ`. 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. - 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`. Co-Authored-By: Claude Opus 4.7 (1M context) --- proofs/agda/All.agda | 1 + .../Ordinal/Buchholz/RankMonoUnionWfCNF.agda | 125 ++++++++++++++++++ proofs/agda/Ordinal/Buchholz/Smoke.agda | 17 +++ 3 files changed, 143 insertions(+) create mode 100644 proofs/agda/Ordinal/Buchholz/RankMonoUnionWfCNF.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 410ab44..f934171 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -152,6 +152,7 @@ open import Ordinal.Buchholz.RankMonoUmbrellaSlice4 open import Ordinal.Buchholz.RankMonoSameLeft open import Ordinal.Buchholz.RankMonoUnion open import Ordinal.Buchholz.RankMonoUnionWF +open import Ordinal.Buchholz.RankMonoUnionWfCNF open import Ordinal.Buchholz.RecursiveSurfaceOrder open import Ordinal.Buchholz.RecursiveSurfaceBudget open import Ordinal.Buchholz.SurfaceOrder diff --git a/proofs/agda/Ordinal/Buchholz/RankMonoUnionWfCNF.agda b/proofs/agda/Ordinal/Buchholz/RankMonoUnionWfCNF.agda new file mode 100644 index 0000000..f12f18b --- /dev/null +++ b/proofs/agda/Ordinal/Buchholz/RankMonoUnionWfCNF.agda @@ -0,0 +1,125 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell + +-- WfCNF-wrapped variant of the union rank-mono umbrella (2026-05-30). +-- +-- ## What this lands +-- +-- Mirrors `Ordinal.Buchholz.RankMonoUmbrellaSlice4._<ᵇ⁻ⁿ_`'s +-- WfCNF-bundling pattern over the union umbrella's `_<ᵇᵘ_` from +-- `Ordinal.Buchholz.RankMonoUnion`. The narrowed relation +-- `_<ᵇᵘⁿ_` bundles: +-- +-- * `wf-x : WfCNF x` — source-side canonical-form witness +-- * `wf-y : WfCNF y` — target-side canonical-form witness +-- * `<ᵇᵘ-d : x <ᵇᵘ y` — the union derivation +-- +-- The narrowed relation's `rank-pow-mono-<ᵇᵘⁿ` discharges via +-- `rank-pow-mono-<ᵇᵘ` on the bundled derivation. +-- +-- ## Why this exists +-- +-- Downstream Buchholz consumers (e.g., the surface-route well- +-- foundedness work in `Ordinal.Buchholz.RecursiveSurfaceOrder`) +-- need the WfCNF invariant carried alongside the rank-relation +-- so they don't have to re-discover it via separate proof +-- structure. Slice 4's `_<ᵇ⁻ⁿ_` provides this for the strict- +-- head joint-bplus extension; this module provides the +-- analogous wrap for the full union umbrella. +-- +-- ## Mechanical extension +-- +-- This module is the WfCNF-wrap template for any future union +-- extension that adds new source-rule slots. The recipe: +-- +-- 1. Add the new disjunct to `_<ᵇᵘ_` in `RankMonoUnion`. +-- 2. The mediator `rank-pow-mono-<ᵇᵘ` extends with the new +-- case via `[_,_]`. +-- 3. THIS MODULE updates AUTOMATICALLY because the record +-- embeds the union's relation — no edit needed here. +-- +-- The architectural payoff documented in `RankMonoUnion`'s +-- preamble holds across the WfCNF wrap as well: per-extension +-- proof work + structural composition. + +module Ordinal.Buchholz.RankMonoUnionWfCNF where + +open import Ordinal.Brouwer.Phase13 using (_<′_) +open import Ordinal.Buchholz.Syntax using (BT) +open import Ordinal.Buchholz.RankPow using (rank-pow) +open import Ordinal.Buchholz.WellFormedCNF using (WfCNF) +open import Ordinal.Buchholz.RankMonoUmbrella using (_<ᵇ⁰_) +open import Ordinal.Buchholz.RankMonoUmbrellaSlice3 using (_<ᵇ¹_) +open import Ordinal.Buchholz.RankMonoSameLeft using (_<ᵇ⁺²_) +open import Ordinal.Buchholz.RankMonoUnion using + ( _<ᵇᵘ_ + ; rank-pow-mono-<ᵇᵘ + ; <ᵇᵘ-from-<ᵇ¹ + ; <ᵇᵘ-from-<ᵇ⁺² + ; <ᵇᵘ-from-<ᵇ⁰ + ) + +---------------------------------------------------------------------- +-- The WfCNF-narrowed union relation `_<ᵇᵘⁿ_` +---------------------------------------------------------------------- + +-- Bundles WfCNF endpoints together with a `_<ᵇᵘ_` derivation. +-- Same shape as `RankMonoUmbrellaSlice4._<ᵇ⁻ⁿ_` but over the +-- union umbrella. The WfCNF fields are unused inside the +-- rank-pow-mono closure but available to consumers reasoning +-- about the canonical-form invariant of the endpoints (e.g., +-- downstream well-foundedness work). + +record _<ᵇᵘⁿ_ (x y : BT) : Set where + constructor mk<ᵇᵘⁿ + field + wf-x : WfCNF x + wf-y : WfCNF y + <ᵇᵘ-d : x <ᵇᵘ y + +open _<ᵇᵘⁿ_ public + +infix 4 _<ᵇᵘⁿ_ + +---------------------------------------------------------------------- +-- Constructor-level embeddings +---------------------------------------------------------------------- + +-- Inherit any `_<ᵇ⁰_` derivation as a narrowed `_<ᵇᵘⁿ_` +-- derivation under WfCNF endpoints. Forwards through the +-- canonical `<ᵇ¹` embedding path of `_<ᵇᵘ_`. + +<ᵇᵘⁿ-from-<ᵇ⁰ : + ∀ {x y} → WfCNF x → WfCNF y → x <ᵇ⁰ y → x <ᵇᵘⁿ y +<ᵇᵘⁿ-from-<ᵇ⁰ wf-x wf-y p = + mk<ᵇᵘⁿ wf-x wf-y (<ᵇᵘ-from-<ᵇ⁰ p) + +-- Embed an `_<ᵇ¹_` derivation as a narrowed `_<ᵇᵘⁿ_` derivation. +-- Covers the strict-head joint-bplus case via `<ᵇ¹-+1-+`. + +<ᵇᵘⁿ-from-<ᵇ¹ : + ∀ {x y} → WfCNF x → WfCNF y → x <ᵇ¹ y → x <ᵇᵘⁿ y +<ᵇᵘⁿ-from-<ᵇ¹ wf-x wf-y p = + mk<ᵇᵘⁿ wf-x wf-y (<ᵇᵘ-from-<ᵇ¹ p) + +-- Embed an `_<ᵇ⁺²_` derivation as a narrowed `_<ᵇᵘⁿ_` derivation. +-- Covers the Path-3 same-left joint-bplus case via +-- `<ᵇ⁺²-same-left`. + +<ᵇᵘⁿ-from-<ᵇ⁺² : + ∀ {x y} → WfCNF x → WfCNF y → x <ᵇ⁺² y → x <ᵇᵘⁿ y +<ᵇᵘⁿ-from-<ᵇ⁺² wf-x wf-y p = + mk<ᵇᵘⁿ wf-x wf-y (<ᵇᵘ-from-<ᵇ⁺² p) + +---------------------------------------------------------------------- +-- Rank-pow monotonicity +---------------------------------------------------------------------- + +-- Forwards directly to `rank-pow-mono-<ᵇᵘ` via the bundled +-- derivation. The WfCNF fields are unused inside the proof +-- but available to consumers reasoning about the endpoints. +-- Same shape as `RankMonoUmbrellaSlice4.rank-pow-mono-<ᵇ⁻ⁿ`. + +rank-pow-mono-<ᵇᵘⁿ : ∀ {x y} → x <ᵇᵘⁿ y → rank-pow x <′ rank-pow y +rank-pow-mono-<ᵇᵘⁿ p = rank-pow-mono-<ᵇᵘ (<ᵇᵘ-d p) diff --git a/proofs/agda/Ordinal/Buchholz/Smoke.agda b/proofs/agda/Ordinal/Buchholz/Smoke.agda index 0c7af78..ed40701 100644 --- a/proofs/agda/Ordinal/Buchholz/Smoke.agda +++ b/proofs/agda/Ordinal/Buchholz/Smoke.agda @@ -617,3 +617,20 @@ open import Ordinal.Buchholz.RankMonoUnionWF using ( wf-rank-pow-pullback ; wf-<ᵇᵘ ) + +-- WfCNF wrap of the union umbrella 2026-05-30 (own block per +-- CLAUDE.md Working rules): mirrors `RankMonoUmbrellaSlice4._<ᵇ⁻ⁿ_`'s +-- WfCNF-bundling pattern over the union umbrella's `_<ᵇᵘ_`. +-- Downstream Buchholz consumers needing the canonical-form +-- invariant alongside the rank-relation use this narrowed form. +-- The architectural-extension recipe documented in +-- `RankMonoUnion`'s preamble automatically extends through this +-- WfCNF wrap — new union disjuncts don't require edits here. +open import Ordinal.Buchholz.RankMonoUnionWfCNF using + ( _<ᵇᵘⁿ_ + ; mk<ᵇᵘⁿ + ; <ᵇᵘⁿ-from-<ᵇ⁰ + ; <ᵇᵘⁿ-from-<ᵇ¹ + ; <ᵇᵘⁿ-from-<ᵇ⁺² + ; rank-pow-mono-<ᵇᵘⁿ + )