|
| 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 | +-- Checked refutation: the provisional `rank-pow` is NOT a monotone |
| 6 | +-- order-embedding of `_<ᵇ_` — not even restricted to WfCNF terms. It |
| 7 | +-- STRICTLY REVERSES a concrete `<ᵇ` step at the `<ᵇ-+1` joint-bplus |
| 8 | +-- ψ/Ω equal-marker boundary. |
| 9 | +-- |
| 10 | +-- ## Why this matters (sharpening the Slice 3 "open" verdict) |
| 11 | +-- |
| 12 | +-- `Ordinal.Buchholz.RankPowSlice3Headline.rank-mono-<ᵇ-+1-via-head-Ω` |
| 13 | +-- closes the joint-bplus rank-mono case only UNDER A STRICT-HEAD |
| 14 | +-- PREMISE `head-Ω x₁ <Ω head-Ω y₁`, and |
| 15 | +-- `Ordinal.Buchholz.RankMonoUmbrellaSlice3._<ᵇ¹_` bakes that premise |
| 16 | +-- into its joint-bplus constructor `<ᵇ¹-+1-+`. The equal-head |
| 17 | +-- remainder (`head-Ω x₁ ≡ head-Ω y₁`) is documented in |
| 18 | +-- `Ordinal.Buchholz.RankLexSlice3`'s design note as "CLOSED at the |
| 19 | +-- ψ-rank level, OPEN at the bplus-chain level pending one of |
| 20 | +-- (a)/(b)/(c)". |
| 21 | +-- |
| 22 | +-- This module sharpens that verdict from "open / unproven" to |
| 23 | +-- "FALSE". The equal-head joint-bplus rank-mono statement does not |
| 24 | +-- merely lack a proof for the current `rank-pow`: it has a |
| 25 | +-- counterexample. No strengthening of the proof effort closes it. |
| 26 | +-- The defect is structural — `rank-pow (bpsi ν _) = ω-rank-pow ν = |
| 27 | +-- rank-pow (bOmega ν)` (`RankPow.agda:163,165`) gives ψ_ν(α) and Ω_ν |
| 28 | +-- the SAME rank, so `rank-pow` cannot see the strict gap ψ_ν(α) < Ω_ν |
| 29 | +-- that the intended ordinal semantics has. Closing the equal-head |
| 30 | +-- case REQUIRES a different rank: one that places ψ_ν(α) strictly |
| 31 | +-- below Ω_ν at a shared marker (option (c) of the RankLexSlice3 |
| 32 | +-- design note — the non-local rank redesign). |
| 33 | +-- |
| 34 | +-- This is the `rank-pow`-level companion to the two Brouwer-arithmetic |
| 35 | +-- refutations the closure routes lean on: |
| 36 | +-- * `Ordinal.Brouwer.StrictLeftMonoRefuted` (route (b)), |
| 37 | +-- * `Ordinal.Brouwer.AdditivePrincipalGenericRefuted` (route (a)). |
| 38 | +-- Those refute the arithmetic lemmas a `rank-pow`-level closure would |
| 39 | +-- have to consume. This module is more direct: it refutes the |
| 40 | +-- rank-monotonicity GOAL itself, so a future session sees immediately |
| 41 | +-- that the equal-head case is unreachable with this rank and does not |
| 42 | +-- re-attempt it. Concretely it UPGRADES the placeholder matched- |
| 43 | +-- negative `Ordinal.Buchholz.RankMonoUmbrellaSlice4. |
| 44 | +-- <ᵇ⁻ⁿ-shortfall-equal-head` (a bare `⊤`-alias) to a checked |
| 45 | +-- counterexample, in the same "promote a placeholder to a theorem" |
| 46 | +-- spirit as `StrictLeftMonoRefuted`. |
| 47 | +-- |
| 48 | +-- The witness sits at the CROSS-HEAD flavour of the boundary — |
| 49 | +-- `bpsi ν _` vs `bOmega ν` (syntactically distinct, `rank-pow`-equal) |
| 50 | +-- — which `Ordinal.Buchholz.RankLexJointBplus` flags as the case its |
| 51 | +-- `rank-lex-jb` pivot remains load-bearing for. This refutation is |
| 52 | +-- exactly why that pivot to a DIFFERENT rank (one whose `bplus` |
| 53 | +-- second component carries `leftmost-α`, placing ψ_ν(α) below Ω_ν) is |
| 54 | +-- the only viable forward path: the present `rank-pow` cannot be |
| 55 | +-- repaired into monotonicity here, it must be replaced. |
| 56 | +-- |
| 57 | +-- ## The witness (BOTH terms WfCNF) |
| 58 | +-- |
| 59 | +-- s = bplus (bpsi (fin 0) bzero) (bpsi (fin 0) bzero) -- ψ₀(0) + ψ₀(0) |
| 60 | +-- t = bplus (bOmega (fin 0)) bzero -- Ω₀ + 0 |
| 61 | +-- |
| 62 | +-- * `s <ᵇ t` via `<ᵇ-+1 (<ᵇ-ψΩ≤ (fin 0 ≤Ω fin 0))`: the source's |
| 63 | +-- leading summand ψ₀(0) is `<ᵇ` the target's leading summand Ω₀ |
| 64 | +-- at the EQUAL marker fin 0 — exactly the `<ᵇ-ψΩ≤` boundary that |
| 65 | +-- `head-Ω-inv-bpsi` can only bound non-strictly. |
| 66 | +-- * Yet `rank-pow t = ω¹ ⊕ oz <′ ω¹ ⊕ ω¹ = rank-pow s`: `rank-pow` |
| 67 | +-- ranks the SOURCE strictly ABOVE the TARGET, because both leading |
| 68 | +-- summands collapse to ω¹ = `ω-rank-pow (fin 0)` and the source |
| 69 | +-- carries a second ψ₀(0) summand while the target's tail is 0. |
| 70 | +-- |
| 71 | +-- Ordinally `s` really is below `t` (ψ₀(0)·2 < Ω₀, since Ω₀ is |
| 72 | +-- additively principal); the reversal is purely an artefact of |
| 73 | +-- `rank-pow`'s α-blind, ψ/Ω-collapsing shape. |
| 74 | +-- |
| 75 | +-- ## Headlines (pinned in `Ordinal/Buchholz/Smoke.agda`) |
| 76 | +-- |
| 77 | +-- * `s`, `t`, `wf-s`, `wf-t`, `s<ᵇt` -- the witness data |
| 78 | +-- * `rank-pow-strictly-reverses` -- rank-pow t <′ rank-pow s |
| 79 | +-- * `RankPowMono`, `rank-pow-mono-refuted` |
| 80 | +-- -- ¬ (WfCNF rank-monotonicity) |
| 81 | +-- * `RankPowMonoPlus1`, `rank-pow-mono-plus1-refuted` |
| 82 | +-- -- ¬ (joint-bplus, no strict-head) |
| 83 | + |
| 84 | +module Ordinal.Buchholz.RankPowMonoRefuted where |
| 85 | + |
| 86 | +open import Data.Nat.Base using (zero; suc; z≤n) |
| 87 | +open import Data.Empty using (⊥) |
| 88 | +open import Data.Sum.Base using (inj₁; inj₂) |
| 89 | +open import Relation.Nullary using (¬_) |
| 90 | +open import Relation.Binary.PropositionalEquality using (refl) |
| 91 | +open import Induction.WellFounded using (Acc; acc) |
| 92 | + |
| 93 | +open import Ordinal.Brouwer using (oz; osuc) |
| 94 | +open import Ordinal.Brouwer.Phase13 using |
| 95 | + ( _≤′_ |
| 96 | + ; _<′_ |
| 97 | + ; ≤′-zero |
| 98 | + ; ≤′-trans |
| 99 | + ; ⊕-mono-<-right |
| 100 | + ; ⊕-mono-≤-right |
| 101 | + ; wf-<′ |
| 102 | + ) |
| 103 | +open import Ordinal.Brouwer.OmegaPow using (ω^_; ω^_-pos) |
| 104 | +open import Ordinal.OmegaMarkers using (fin; _≤Ω_; fin≤fin) |
| 105 | +open import Ordinal.Buchholz.Syntax using |
| 106 | + ( BT; bzero; bOmega; bplus; bpsi ) |
| 107 | +open import Ordinal.Buchholz.Order using |
| 108 | + ( _<ᵇ_; <ᵇ-0-Ω; <ᵇ-ψΩ≤; <ᵇ-+1 ) |
| 109 | +open import Ordinal.Buchholz.WellFormed using (wf-fin) |
| 110 | +open import Ordinal.Buchholz.WellFormedCNF using |
| 111 | + ( WfCNF |
| 112 | + ; wf-cnf-bzero |
| 113 | + ; wf-cnf-bomega |
| 114 | + ; wf-cnf-bpsi |
| 115 | + ; wf-cnf-bplus |
| 116 | + ; atomic-bzero |
| 117 | + ; atomic-bpsi |
| 118 | + ) |
| 119 | +open import Ordinal.Buchholz.RankPow using (rank-pow) |
| 120 | + |
| 121 | +---------------------------------------------------------------------- |
| 122 | +-- The witness terms |
| 123 | +---------------------------------------------------------------------- |
| 124 | + |
| 125 | +-- s = ψ₀(0) + ψ₀(0); t = Ω₀ + 0. Both in Cantor normal form. |
| 126 | +s : BT |
| 127 | +s = bplus (bpsi (fin 0) bzero) (bpsi (fin 0) bzero) |
| 128 | + |
| 129 | +t : BT |
| 130 | +t = bplus (bOmega (fin 0)) bzero |
| 131 | + |
| 132 | +---------------------------------------------------------------------- |
| 133 | +-- Both witnesses are WfCNF |
| 134 | +---------------------------------------------------------------------- |
| 135 | + |
| 136 | +-- s: left = ψ₀(0) (WfCNF), right = ψ₀(0) (atomic), tail bound by |
| 137 | +-- equality (ψ₀(0) ≤ᵇ ψ₀(0) via `inj₂ refl`). |
| 138 | +wf-s : WfCNF s |
| 139 | +wf-s = |
| 140 | + wf-cnf-bplus |
| 141 | + (wf-cnf-bpsi wf-fin wf-cnf-bzero) |
| 142 | + (wf-cnf-bpsi wf-fin wf-cnf-bzero) |
| 143 | + atomic-bpsi |
| 144 | + (inj₂ refl) |
| 145 | + |
| 146 | +-- t: left = Ω₀ (WfCNF), right = 0 (atomic), tail bound 0 ≤ᵇ Ω₀ via |
| 147 | +-- `<ᵇ-0-Ω`. |
| 148 | +wf-t : WfCNF t |
| 149 | +wf-t = |
| 150 | + wf-cnf-bplus |
| 151 | + (wf-cnf-bomega wf-fin) |
| 152 | + wf-cnf-bzero |
| 153 | + atomic-bzero |
| 154 | + (inj₁ <ᵇ-0-Ω) |
| 155 | + |
| 156 | +---------------------------------------------------------------------- |
| 157 | +-- s <ᵇ t at the ψ/Ω equal-marker boundary |
| 158 | +---------------------------------------------------------------------- |
| 159 | + |
| 160 | +-- fin 0 ≤Ω fin 0 (reflexive) — the `<ᵇ-ψΩ≤` constructor only needs |
| 161 | +-- the NON-strict marker bound, so the equal marker fin 0 suffices. |
| 162 | +fin0≤Ωfin0 : fin 0 ≤Ω fin 0 |
| 163 | +fin0≤Ωfin0 = fin≤fin z≤n |
| 164 | + |
| 165 | +-- ψ₀(0) <ᵇ Ω₀ lifts to (ψ₀(0) + ψ₀(0)) <ᵇ (Ω₀ + 0) via `<ᵇ-+1` |
| 166 | +-- (source-strict-on-the-leading-summand). |
| 167 | +s<ᵇt : s <ᵇ t |
| 168 | +s<ᵇt = <ᵇ-+1 (<ᵇ-ψΩ≤ fin0≤Ωfin0) |
| 169 | + |
| 170 | +---------------------------------------------------------------------- |
| 171 | +-- rank-pow strictly REVERSES the step |
| 172 | +---------------------------------------------------------------------- |
| 173 | + |
| 174 | +-- rank-pow t = ω-rank-pow (fin 0) ⊕ rank-pow bzero = ω¹ ⊕ oz |
| 175 | +-- rank-pow s = ω-rank-pow (fin 0) ⊕ ω-rank-pow (fin 0) = ω¹ ⊕ ω¹ |
| 176 | +-- and ω¹ ⊕ oz <′ ω¹ ⊕ ω¹ by strict right-monotonicity of `_⊕_` |
| 177 | +-- (right summand oz <′ ω¹ via `ω^_-pos 1`). Both rank reductions are |
| 178 | +-- definitional, so the inequality typechecks against the goal. |
| 179 | +rank-pow-strictly-reverses : rank-pow t <′ rank-pow s |
| 180 | +rank-pow-strictly-reverses = |
| 181 | + ⊕-mono-<-right {ω^ 1} {oz} {ω^ 1} (ω^_-pos 1) |
| 182 | + |
| 183 | +-- The same reversal as a NON-strict bound, for the `≤′-trans` step in |
| 184 | +-- the refutations below (rank-pow t ≤′ rank-pow s). |
| 185 | +rank-pow-t≤s : rank-pow t ≤′ rank-pow s |
| 186 | +rank-pow-t≤s = |
| 187 | + ⊕-mono-≤-right {ω^ 1} {oz} {ω^ 1} (≤′-zero {ω^ 1}) |
| 188 | + |
| 189 | +---------------------------------------------------------------------- |
| 190 | +-- Irreflexivity of `_<′_` from well-foundedness |
| 191 | +---------------------------------------------------------------------- |
| 192 | + |
| 193 | +-- Standard derivation by structural recursion on `Acc _<′_ α` |
| 194 | +-- (mirrors `Ordinal.Brouwer.StrictLeftMonoRefuted.<′-irrefl`). |
| 195 | +acc-no-self : ∀ {α} → Acc _<′_ α → α <′ α → ⊥ |
| 196 | +acc-no-self (acc rec) α<α = acc-no-self (rec α<α) α<α |
| 197 | + |
| 198 | +<′-irrefl : ∀ {α} → ¬ (α <′ α) |
| 199 | +<′-irrefl {α} = acc-no-self (wf-<′ α) |
| 200 | + |
| 201 | +---------------------------------------------------------------------- |
| 202 | +-- Refutation 1: general WfCNF rank-monotonicity over `_<ᵇ_` |
| 203 | +---------------------------------------------------------------------- |
| 204 | + |
| 205 | +-- The property a single clean rank-mono theorem would assert: every |
| 206 | +-- `<ᵇ` step between WfCNF terms is reflected by a strict rank |
| 207 | +-- increase. This is precisely what fails — which is why the landed |
| 208 | +-- programme proceeds constructor-by-constructor with the head-Ω / |
| 209 | +-- strict-head machinery rather than as one inductive theorem. |
| 210 | +RankPowMono : Set |
| 211 | +RankPowMono = |
| 212 | + ∀ {a b} → WfCNF a → WfCNF b → a <ᵇ b → rank-pow a <′ rank-pow b |
| 213 | + |
| 214 | +-- Feeding the witness `s <ᵇ t` to the hypothetical monotonicity gives |
| 215 | +-- `rank-pow s <′ rank-pow t`; chaining with `rank-pow t ≤′ rank-pow s` |
| 216 | +-- yields `rank-pow s <′ rank-pow s`, refuted by `<′-irrefl`. |
| 217 | +rank-pow-mono-refuted : ¬ RankPowMono |
| 218 | +rank-pow-mono-refuted mono = |
| 219 | + <′-irrefl {rank-pow s} |
| 220 | + (≤′-trans {osuc (rank-pow s)} {rank-pow t} {rank-pow s} |
| 221 | + (mono wf-s wf-t s<ᵇt) rank-pow-t≤s) |
| 222 | + |
| 223 | +---------------------------------------------------------------------- |
| 224 | +-- Refutation 2: joint-bplus shape WITHOUT the strict-head premise |
| 225 | +---------------------------------------------------------------------- |
| 226 | + |
| 227 | +-- The exact statement `RankMonoUmbrellaSlice3.<ᵇ¹-+1-+` works around |
| 228 | +-- by adding `head-Ω x₁ <Ω head-Ω y₁`. Without that premise (only the |
| 229 | +-- source-strict witness `x₁ <ᵇ y₁` plus WfCNF), the joint-bplus |
| 230 | +-- rank-mono conclusion is false: the witness instantiates it at |
| 231 | +-- x₁ = ψ₀(0), x₂ = ψ₀(0), y₁ = Ω₀, y₂ = 0 (where head-Ω x₁ ≡ head-Ω y₁ |
| 232 | +-- ≡ fin 0, so no strict-head premise is available). |
| 233 | +RankPowMonoPlus1 : Set |
| 234 | +RankPowMonoPlus1 = |
| 235 | + ∀ {x₁ x₂ y₁ y₂} |
| 236 | + → WfCNF (bplus x₁ x₂) → WfCNF (bplus y₁ y₂) |
| 237 | + → x₁ <ᵇ y₁ |
| 238 | + → rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂) |
| 239 | + |
| 240 | +rank-pow-mono-plus1-refuted : ¬ RankPowMonoPlus1 |
| 241 | +rank-pow-mono-plus1-refuted mono = |
| 242 | + <′-irrefl {rank-pow s} |
| 243 | + (≤′-trans {osuc (rank-pow s)} {rank-pow t} {rank-pow s} |
| 244 | + (mono wf-s wf-t (<ᵇ-ψΩ≤ fin0≤Ωfin0)) rank-pow-t≤s) |
0 commit comments