|
| 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)) |
0 commit comments