|
| 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 | +-- Binary Veblen — RUNG 7: the generic fixed-point engine is MINIMAL — |
| 6 | +-- `nextFix g x` is the LEAST pre-fixed point of `g` strictly above `x`, |
| 7 | +-- not merely *a* fixed point. Target-side climb toward ψ₀(Ω_ω) (BH |
| 8 | +-- order-type fidelity, open problem D-2026-06-14). Builds on |
| 9 | +-- `VeblenBinary` (the engine + Γ₀) and `VeblenBinaryNormal` |
| 10 | +-- (`φ-mono₂` / `commonStep-mono`). 2026-06-20. |
| 11 | +-- |
| 12 | +-- ## What this slice adds |
| 13 | +-- |
| 14 | +-- `VeblenBinary` proved `nextFix g x` is a fixed point of `g` |
| 15 | +-- (`nextFix-fixed-{≤,≥}`) lying strictly above `x` (`nextFix-above`). |
| 16 | +-- The missing half of the engine's correctness is MINIMALITY: |
| 17 | +-- |
| 18 | +-- * `nextFix-least` — for monotone `g`, if `x <′ z` and `g z ≤′ z` |
| 19 | +-- (z is a pre-fixed point of g strictly above x) then |
| 20 | +-- `nextFix g x ≤′ z`. So `nextFix g x` is the LEAST pre-fixed |
| 21 | +-- point of g strictly above x. Proof: every approximant of the |
| 22 | +-- iteration tower `g-tower g (osuc x)` is `≤′ z` — the base by |
| 23 | +-- `x <′ z`, each successor by monotonicity into the pre-fixed |
| 24 | +-- point `g z ≤′ z`; the supremum is then `≤′ z` definitionally |
| 25 | +-- (`olim T ≤′ z` unfolds to `∀ n → T n ≤′ z`). |
| 26 | +-- |
| 27 | +-- This is exactly the tool the reverse Γ₀ fixed-point direction (and |
| 28 | +-- "Γ₀ is the LEAST diagonal fixed point") needs, and which |
| 29 | +-- `VeblenBinaryMono` flagged as the open "common-fixed-point-from-above" |
| 30 | +-- piece. As an immediate payoff: |
| 31 | +-- |
| 32 | +-- * `Γ₀-fixed-from-closure` — REDUCES the open reverse direction |
| 33 | +-- `φ_Γ₀(0) ≤′ Γ₀` to a single closure obligation |
| 34 | +-- `commonStep (n ↦ φ_{Γ-tower n}) Γ₀ ≤′ Γ₀` (Γ₀ is closed under |
| 35 | +-- every diagonal-approximant level applied to Γ₀ itself). Because |
| 36 | +-- `φ Γ₀ oz` is, definitionally, `nextFix (commonStep …) oz`, the |
| 37 | +-- reduction is just `nextFix-least` at `x = oz`, `z = Γ₀` |
| 38 | +-- (`Γ₀-pos` supplies `oz <′ Γ₀`). |
| 39 | +-- |
| 40 | +-- ## Honest scope (still a LONG climb — do not overclaim) |
| 41 | +-- |
| 42 | +-- `nextFix-least` is a real, unconditional theorem. `Γ₀-fixed-from- |
| 43 | +-- closure` is a CONDITIONAL: it does NOT prove `φ_Γ₀(0) ≤′ Γ₀`; it |
| 44 | +-- proves it FOLLOWS from the closure `commonStep F Γ₀ ≤′ Γ₀`, which |
| 45 | +-- needs general first-argument monotonicity and REMAINS OPEN (the next |
| 46 | +-- slice). Combined with `VeblenBinaryMono.Γ₀-prefixed` (the `≤′` |
| 47 | +-- direction), discharging that one closure obligation would give the |
| 48 | +-- full bi-`≤′` fixed point `Γ₀ ≃ φ_Γ₀(0)`. ψ₀(Ω_ω) sits far above Γ₀ |
| 49 | +-- behind the ordinal-collapsing layer; order-type fidelity REMAINS OPEN |
| 50 | +-- (D-2026-06-14). No postulate is closed. |
| 51 | + |
| 52 | +module Ordinal.Brouwer.VeblenBinaryLeast where |
| 53 | + |
| 54 | +open import Data.Nat.Base using (ℕ; zero; suc) |
| 55 | + |
| 56 | +open import Ordinal.Brouwer using (Ord; oz; osuc; olim) |
| 57 | +open import Ordinal.Brouwer.Phase13 using (_≤′_; _<′_; ≤′-trans) |
| 58 | +open import Ordinal.Brouwer.VeblenBinary |
| 59 | + using (g-tower; nextFix; deriv; commonStep; φ; Γ-tower; Γ₀; Γ₀-pos) |
| 60 | +open import Ordinal.Brouwer.VeblenBinaryNormal using (φ-mono₂; commonStep-mono) |
| 61 | + |
| 62 | +---------------------------------------------------------------------- |
| 63 | +-- Minimality of the generic fixed-point engine. |
| 64 | +-- |
| 65 | +-- `nextFix g x = olim (g-tower g (osuc x))`, so `nextFix g x ≤′ z` |
| 66 | +-- unfolds (by the `olim f ≤′ β = ∀ n → f n ≤′ β` clause of `_≤′_`) to |
| 67 | +-- "every tower approximant is `≤′ z`". We prove that by induction on |
| 68 | +-- the tower index against a pre-fixed point `z` strictly above `x`. |
| 69 | +---------------------------------------------------------------------- |
| 70 | + |
| 71 | +nextFix-least : |
| 72 | + (g : Ord → Ord) (g-mono : ∀ {a b} → a ≤′ b → g a ≤′ g b) |
| 73 | + {x z : Ord} → x <′ z → g z ≤′ z → nextFix g x ≤′ z |
| 74 | +nextFix-least g g-mono {x} {z} x<z gz≤z = tower≤ |
| 75 | + where |
| 76 | + tower≤ : ∀ n → g-tower g (osuc x) n ≤′ z |
| 77 | + tower≤ zero = x<z |
| 78 | + tower≤ (suc n) = |
| 79 | + ≤′-trans {g (g-tower g (osuc x) n)} {g z} {z} |
| 80 | + (g-mono {g-tower g (osuc x) n} {z} (tower≤ n)) |
| 81 | + gz≤z |
| 82 | + |
| 83 | +---------------------------------------------------------------------- |
| 84 | +-- Payoff: the reverse Γ₀ fixed-point direction reduces to one closure. |
| 85 | +-- |
| 86 | +-- `φ Γ₀ oz` is definitionally `nextFix (commonStep F) oz` where |
| 87 | +-- `F n = φ (Γ-tower n)` (φ-olim recurrence + `deriv g oz = nextFix g oz`), |
| 88 | +-- so `nextFix-least` at `x = oz`, `z = Γ₀` turns the open |
| 89 | +-- `φ_Γ₀(0) ≤′ Γ₀` into the single closure obligation below. |
| 90 | +---------------------------------------------------------------------- |
| 91 | + |
| 92 | +Γ₀-fixed-from-closure : |
| 93 | + commonStep (λ n → φ (Γ-tower n)) Γ₀ ≤′ Γ₀ → |
| 94 | + φ Γ₀ oz ≤′ Γ₀ |
| 95 | +Γ₀-fixed-from-closure closure = |
| 96 | + nextFix-least (commonStep F) |
| 97 | + (commonStep-mono F (λ n {x} {y} → φ-mono₂ (Γ-tower n) {x} {y})) |
| 98 | + {oz} {Γ₀} Γ₀-pos closure |
| 99 | + where |
| 100 | + F : ℕ → Ord → Ord |
| 101 | + F n = φ (Γ-tower n) |
0 commit comments