Skip to content

Commit 3890530

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proof(ordinal): doubled-ladder bzero- + plus-source rank2-mono primitives (#206)
## What New module `Ordinal/Buchholz/RankDoubledLadderMonoPlus.agda` — the per-constructor `rank2`-mono primitives for the `_<ᵇ_` constructors whose monotonicity is pure `⊕`-weakening / positivity (no admissibility, no additive-principality): ```agda rank2-pos-bOmega : oz <′ rank2 (bOmega μ) -- <ᵇ-0-Ω rank2-pos-bpsi : oz <′ rank2 (bpsi ν α) -- <ᵇ-0-ψ rank2-mono-0-+ : oz <′ rank2 x → oz <′ rank2 (bplus x y) -- <ᵇ-0-+ rank2-mono-Ω+ : rank2 (bOmega μ) <′ rank2 x → rank2 (bOmega μ) <′ rank2 (bplus x y) -- <ᵇ-Ω+ rank2-mono-ψ+ : rank2 (bpsi ν α) <′ rank2 x → rank2 (bpsi ν α) <′ rank2 (bplus x y) -- <ᵇ-ψ+ ``` ## How - **bzero-source positivity**: the Ω-block / ψ-block leading rank is positive (`ω-rank-pow-pos`), chained up to the target via `ω-rank-pow-<-succ` / `⊕-left-≤-sum`. - **plus-source** (`<ᵇ-Ω+`, `<ᵇ-ψ+`): the constructor recurses on a sub-derivation `atom <ᵇ x`; given the recursive result (the IH, taken as the premise), the bplus target only adds on the right, so `⊕-left-≤-sum` finishes. Stated relation-agnostically, mirroring RankPow's per-constructor family — the consumer pattern-matches on its constructor, recurses, applies the matching primitive. ## Progress With #205's four atomic-boundary primitives, **9 of the 12** core `_<ᵇ_` constructors now have `rank2`-mono. **Remaining** (final umbrella slice): the three bplus-on-left cases `<ᵇ-+Ω/+ψ/+1`, which need additive-principality of the `rank2` target (`additive-principal-ω-rank-pow-succ`) + the joint-bplus tail bound `y ≤ᵇ x` — the same shape that made the single-ladder `<ᵇ-+1` Gate 1's last residual — then the full `rank2-mono` umbrella + the `wf-<′`-transport headline `wf-<ᵇ`. ## Verification - `agda -i proofs/agda proofs/agda/All.agda` exits 0 under `--safe --without-K`. - Five headlines pinned in the Buchholz `Smoke.agda` (own block). - Zero postulates / escape pragmas. https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE --- _Generated by [Claude Code](https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent c2c6a44 commit 3890530

3 files changed

Lines changed: 130 additions & 0 deletions

File tree

‎proofs/agda/All.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -154,6 +154,7 @@ open import Ordinal.Buchholz.RankPowSlice3
154154
open import Ordinal.Buchholz.RankPowSlice3Headline
155155
open import Ordinal.Buchholz.RankDoubledLadder
156156
open import Ordinal.Buchholz.RankDoubledLadderMono
157+
open import Ordinal.Buchholz.RankDoubledLadderMonoPlus
157158
open import Ordinal.Buchholz.RankMonoUmbrella
158159
open import Ordinal.Buchholz.RankMonoUmbrellaSlice3
159160
open import Ordinal.Buchholz.RankMonoUmbrellaSlice4

‎proofs/agda/Ordinal/Buchholz/RankDoubledLadderMonoPlus.agda‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
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+
-- Doubled-ladder rank monotonicity — bzero-source + plus-source slice
6+
-- (2026-06-14).
7+
--
8+
-- ## Why this exists
9+
--
10+
-- `RankDoubledLadderMono` discharged the four ATOMIC-vs-atomic
11+
-- `_<ᵇ_` constructors (`<ᵇ-ΩΩ/Ωψ/ψΩ/ψΩ≤`). This slice adds the
12+
-- per-constructor `rank2`-mono primitives for the constructors whose
13+
-- monotonicity is pure `⊕`-weakening / positivity — no admissibility
14+
-- and no additive-principality needed:
15+
--
16+
-- * bzero-source (`<ᵇ-0-Ω/0-ψ/0-+`) — positivity of the target rank;
17+
-- * plus-source with an ATOMIC left witness (`<ᵇ-Ω+`, `<ᵇ-ψ+`) —
18+
-- the constructor recurses on a sub-derivation `bOmega μ <ᵇ x` /
19+
-- `bpsi ν α <ᵇ x`; given the recursive result `rank2 atom <′
20+
-- rank2 x` (the IH), the bplus target only ADDS on the right, so
21+
-- `⊕-left-≤-sum` finishes.
22+
--
23+
-- These mirror the `<ᵇ-0-*` / `<ᵇ-Ω+` / `<ᵇ-ψ+` primitives RankPow
24+
-- shipped for the single ladder: each is stated relation-agnostically
25+
-- (the recursive case takes the IH as its premise), so a `_<ᵇ_`
26+
-- consumer pattern-matches on its own constructor, recurses, and
27+
-- applies the matching primitive.
28+
--
29+
-- ## Honest scope
30+
--
31+
-- NOT in this slice (the genuinely-recursive bplus-ON-LEFT cases,
32+
-- deferred to the final umbrella slice): `<ᵇ-+Ω`, `<ᵇ-+ψ`, `<ᵇ-+1`.
33+
-- Those need additive-principality of the `rank2` TARGET
34+
-- (`additive-principal-ω-rank-pow-succ` for `<ᵇ-+Ω`; the joint-bplus
35+
-- tail bound `y ≤ᵇ x` for `<ᵇ-+1`) — the same shape that made the
36+
-- single-ladder `<ᵇ-+1` Gate 1's last residual. With those three the
37+
-- full `rank2-mono : WfAdm x → WfAdm y → x <ᵇ y → rank2 x <′ rank2 y`
38+
-- umbrella + the `wf-<′`-transport headline `wf-<ᵇ` close.
39+
--
40+
-- ## Headlines (pin in `Ordinal/Buchholz/Smoke.agda`)
41+
--
42+
-- * `rank2-pos-bOmega` (`<ᵇ-0-Ω`)
43+
-- * `rank2-pos-bpsi` (`<ᵇ-0-ψ`)
44+
-- * `rank2-mono-0-+` (`<ᵇ-0-+`)
45+
-- * `rank2-mono-Ω+` (`<ᵇ-Ω+`)
46+
-- * `rank2-mono-ψ+` (`<ᵇ-ψ+`)
47+
48+
module Ordinal.Buchholz.RankDoubledLadderMonoPlus where
49+
50+
open import Ordinal.Brouwer using (Ord; oz)
51+
open import Ordinal.Brouwer.Phase13 using (_<′_; ⊕-left-≤-sum)
52+
open import Ordinal.Brouwer.Arithmetic using (_⊕_)
53+
open import Ordinal.OmegaMarkers using (OmegaIndex)
54+
open import Ordinal.Buchholz.Syntax using (BT; bOmega; bpsi; bplus)
55+
open import Ordinal.Buchholz.RankPow using
56+
( ω-rank-pow
57+
; ω-rank-pow-succ
58+
; ω-rank-pow-pos
59+
; ω-rank-pow-<-succ
60+
)
61+
open import Ordinal.Buchholz.RankDoubledLadder using (rank2; double)
62+
open import Ordinal.Buchholz.RankDoubledLadderMono using (<′-trans; <′-≤′-trans)
63+
64+
----------------------------------------------------------------------
65+
-- bzero-source positivity (`<ᵇ-0-Ω`, `<ᵇ-0-ψ`)
66+
----------------------------------------------------------------------
67+
68+
-- `<ᵇ-0-Ω` — `oz <′ rank2 (bOmega μ)`. The Ω-block rank is `oz <′
69+
-- ω-rank-pow (double μ) <′ ω-rank-pow-succ (double μ)`.
70+
rank2-pos-bOmega : ∀ μ → oz <′ rank2 (bOmega μ)
71+
rank2-pos-bOmega μ =
72+
<′-trans {oz} {ω-rank-pow (double μ)} {ω-rank-pow-succ (double μ)}
73+
(ω-rank-pow-pos (double μ))
74+
(ω-rank-pow-<-succ (double μ))
75+
76+
-- `<ᵇ-0-ψ` — `oz <′ rank2 (bpsi ν α)`. The ψ-rank's leading block is
77+
-- positive and the ψ-argument only adds (`⊕-left-≤-sum`).
78+
rank2-pos-bpsi : ∀ ν α → oz <′ rank2 (bpsi ν α)
79+
rank2-pos-bpsi ν α =
80+
<′-≤′-trans {oz} {ω-rank-pow (double ν)} {ω-rank-pow (double ν) ⊕ rank2 α}
81+
(ω-rank-pow-pos (double ν))
82+
(⊕-left-≤-sum {ω-rank-pow (double ν)} (rank2 α))
83+
84+
----------------------------------------------------------------------
85+
-- plus-source primitives (`<ᵇ-0-+`, `<ᵇ-Ω+`, `<ᵇ-ψ+`)
86+
----------------------------------------------------------------------
87+
88+
-- `<ᵇ-0-+` — `oz <′ rank2 (bplus x y)` from left-positivity. The
89+
-- consumer supplies `oz <′ rank2 x` (from well-formedness of the
90+
-- bplus head); the right summand only adds.
91+
rank2-mono-0-+ : ∀ {x y}
92+
→ oz <′ rank2 x
93+
→ oz <′ rank2 (bplus x y)
94+
rank2-mono-0-+ {x} {y} p =
95+
<′-≤′-trans {oz} {rank2 x} {rank2 x ⊕ rank2 y}
96+
p
97+
(⊕-left-≤-sum {rank2 x} (rank2 y))
98+
99+
-- `<ᵇ-Ω+` — `bOmega μ <ᵇ x → bOmega μ <ᵇ bplus x y`. Premise is the
100+
-- recursive result `rank2 (bOmega μ) <′ rank2 x`; the bplus target
101+
-- adds on the right.
102+
rank2-mono-Ω+ : ∀ {μ x y}
103+
→ rank2 (bOmega μ) <′ rank2 x
104+
→ rank2 (bOmega μ) <′ rank2 (bplus x y)
105+
rank2-mono-Ω+ {μ} {x} {y} p =
106+
<′-≤′-trans {rank2 (bOmega μ)} {rank2 x} {rank2 x ⊕ rank2 y}
107+
p
108+
(⊕-left-≤-sum {rank2 x} (rank2 y))
109+
110+
-- `<ᵇ-ψ+` — `bpsi ν α <ᵇ x → bpsi ν α <ᵇ bplus x y`. Same shape as
111+
-- `<ᵇ-Ω+`, premise = the recursive result `rank2 (bpsi ν α) <′
112+
-- rank2 x`.
113+
rank2-mono-ψ+ : ∀ {ν α x y}
114+
→ rank2 (bpsi ν α) <′ rank2 x
115+
→ rank2 (bpsi ν α) <′ rank2 (bplus x y)
116+
rank2-mono-ψ+ {ν} {α} {x} {y} p =
117+
<′-≤′-trans {rank2 (bpsi ν α)} {rank2 x} {rank2 x ⊕ rank2 y}
118+
p
119+
(⊕-left-≤-sum {rank2 x} (rank2 y))

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -486,6 +486,16 @@ open import Ordinal.Buchholz.RankDoubledLadderMono using
486486
; rank2-mono-ψΩ≤
487487
)
488488

489+
-- Doubled-ladder bzero-source + plus-source rank2-mono primitives
490+
-- (own block per CLAUDE.md Working rules).
491+
open import Ordinal.Buchholz.RankDoubledLadderMonoPlus using
492+
( rank2-pos-bOmega
493+
; rank2-pos-bpsi
494+
; rank2-mono-0-+
495+
; rank2-mono-Ω+
496+
; rank2-mono-ψ+
497+
)
498+
489499
-- Slice 3 prerequisites (own block per CLAUDE.md Working rules):
490500
-- the left-spine NonBzero predicate, the strict-jump bridge from
491501
-- `μ <Ω ν` to `ω-rank-pow-succ μ ≤′ ω-rank-pow ν`, and the head-Ω

0 commit comments

Comments
 (0)