|
| 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 8: the generic fixed-point engine is MONOTONE IN |
| 6 | +-- ITS ITERATED FUNCTION. Target-side climb toward ψ₀(Ω_ω) (BH order-type |
| 7 | +-- fidelity, open problem D-2026-06-14). Builds on `VeblenBinary` (the |
| 8 | +-- engine) and `VeblenBinaryNormal` (`nextFix-mono` — monotone in the |
| 9 | +-- base). 2026-06-21. |
| 10 | +-- |
| 11 | +-- ## What this slice adds |
| 12 | +-- |
| 13 | +-- The engine's monotonicity was known in the BASE argument (`nextFix-mono`, |
| 14 | +-- `deriv-mono`). The missing axis is monotonicity in the iterated FUNCTION |
| 15 | +-- `g` itself: a pointwise-smaller (continuous) function has a pointwise- |
| 16 | +-- smaller fixed-point enumeration. |
| 17 | +-- |
| 18 | +-- * `g-tower-mono-in-g` — `g ≤ h` pointwise (and `h` monotone) ⇒ the |
| 19 | +-- iteration towers are ordered at every index. |
| 20 | +-- * `nextFix-mono-in-g` — hence `nextFix g x ≤′ nextFix h x`. |
| 21 | +-- * `deriv-mono-in-g` — hence `deriv g β ≤′ deriv h β` for every β |
| 22 | +-- (osuc case also uses `nextFix-mono` in the base). |
| 23 | +-- |
| 24 | +-- This is the engine-side tool that *general first-argument monotonicity* |
| 25 | +-- of `φ` (`a ≤′ b ⇒ φ_a x ≤′ φ_b x`) and the Γ₀ diagonal-closure |
| 26 | +-- (`commonStep (n ↦ φ_{Γ-tower n}) Γ₀ ≤′ Γ₀`, the obligation |
| 27 | +-- `VeblenBinaryLeast.Γ₀-fixed-from-closure` reduces the reverse Γ₀ fixed |
| 28 | +-- point to) are built from: when one level's defining function dominates |
| 29 | +-- another's, their `deriv` enumerations are ordered. |
| 30 | +-- |
| 31 | +-- ## Honest scope (the Γ₀ fixed point is NOT closed here) |
| 32 | +-- |
| 33 | +-- These are unconditional engine lemmas. They do NOT by themselves close |
| 34 | +-- `φ_Γ₀(0) ≤′ Γ₀`. That closure is a COUPLED CLUSTER — it additionally |
| 35 | +-- needs (i) level-inflationarity `α <′ φ_α(0)`, (ii) strict Γ-tower |
| 36 | +-- monotonicity (from i), (iii) the general level-fixed-point |
| 37 | +-- `a <′ b ⇒ φ_a(φ_b(y)) ≤′ φ_b(y)` (a value of a higher level is a fixed |
| 38 | +-- point of every lower level), and (iv) general first-argument |
| 39 | +-- monotonicity — which are mutually entangled and have delicate |
| 40 | +-- degenerate-`olim` cases under the recursive `_≤′_`. This slice supplies |
| 41 | +-- the engine-monotonicity axis (iv's engine half); the rest remains the |
| 42 | +-- open frontier. Order-type fidelity ψ₀(Ω_ω) REMAINS OPEN |
| 43 | +-- (D-2026-06-14). No postulate is closed. bi-`≤′` throughout. |
| 44 | + |
| 45 | +module Ordinal.Brouwer.VeblenBinaryMonoG where |
| 46 | + |
| 47 | +open import Data.Nat.Base using (ℕ; zero; suc) |
| 48 | + |
| 49 | +open import Ordinal.Brouwer using (Ord; oz; osuc; olim) |
| 50 | +open import Ordinal.Brouwer.Phase13 |
| 51 | + using (_≤′_; ≤′-refl; ≤′-trans; ≤′-lim; f-in-lim′) |
| 52 | +open import Ordinal.Brouwer.VeblenBinary using (g-tower; nextFix; deriv) |
| 53 | +open import Ordinal.Brouwer.VeblenBinaryNormal using (nextFix-mono) |
| 54 | + |
| 55 | +---------------------------------------------------------------------- |
| 56 | +-- The iteration tower is monotone in the iterated function. |
| 57 | +-- |
| 58 | +-- With `g y ≤′ h y` everywhere and `h` monotone, each tower step keeps |
| 59 | +-- the order: `g-tower g x (suc n) = g (g-tower g x n) ≤′ h (g-tower g x n)` |
| 60 | +-- [pointwise] `≤′ h (g-tower h x n) = g-tower h x (suc n)` [h monotone on |
| 61 | +-- the IH]. |
| 62 | +---------------------------------------------------------------------- |
| 63 | + |
| 64 | +g-tower-mono-in-g : |
| 65 | + (g h : Ord → Ord) |
| 66 | + (g≤h : ∀ y → g y ≤′ h y) |
| 67 | + (h-mono : ∀ {a b} → a ≤′ b → h a ≤′ h b) |
| 68 | + (x : Ord) → ∀ n → g-tower g x n ≤′ g-tower h x n |
| 69 | +g-tower-mono-in-g g h g≤h h-mono x zero = ≤′-refl {x} |
| 70 | +g-tower-mono-in-g g h g≤h h-mono x (suc n) = |
| 71 | + ≤′-trans {g (g-tower g x n)} {h (g-tower g x n)} {h (g-tower h x n)} |
| 72 | + (g≤h (g-tower g x n)) |
| 73 | + (h-mono {g-tower g x n} {g-tower h x n} (g-tower-mono-in-g g h g≤h h-mono x n)) |
| 74 | + |
| 75 | +---------------------------------------------------------------------- |
| 76 | +-- nextFix is monotone in the iterated function. |
| 77 | +-- |
| 78 | +-- `nextFix g x = olim (g-tower g (osuc x))`; `olim T ≤′ olim S` unfolds to |
| 79 | +-- `∀ n → T n ≤′ olim S`, discharged per index by the tower order above |
| 80 | +-- routed through `≤′-lim`. |
| 81 | +---------------------------------------------------------------------- |
| 82 | + |
| 83 | +nextFix-mono-in-g : |
| 84 | + (g h : Ord → Ord) |
| 85 | + (g≤h : ∀ y → g y ≤′ h y) |
| 86 | + (h-mono : ∀ {a b} → a ≤′ b → h a ≤′ h b) |
| 87 | + (x : Ord) → nextFix g x ≤′ nextFix h x |
| 88 | +nextFix-mono-in-g g h g≤h h-mono x = λ n → |
| 89 | + ≤′-lim {g-tower g (osuc x) n} (g-tower h (osuc x)) n |
| 90 | + (g-tower-mono-in-g g h g≤h h-mono (osuc x) n) |
| 91 | + |
| 92 | +---------------------------------------------------------------------- |
| 93 | +-- deriv is monotone in the iterated function. |
| 94 | +-- |
| 95 | +-- Structural recursion on β. The `osuc` case composes monotonicity in |
| 96 | +-- the function (`nextFix-mono-in-g` at the smaller base `deriv g β`) with |
| 97 | +-- monotonicity in the base (`nextFix-mono h` along the IH); the `olim` |
| 98 | +-- case is branchwise through `≤′-lim`. |
| 99 | +---------------------------------------------------------------------- |
| 100 | + |
| 101 | +deriv-mono-in-g : |
| 102 | + (g h : Ord → Ord) |
| 103 | + (g≤h : ∀ y → g y ≤′ h y) |
| 104 | + (h-mono : ∀ {a b} → a ≤′ b → h a ≤′ h b) |
| 105 | + (β : Ord) → deriv g β ≤′ deriv h β |
| 106 | +deriv-mono-in-g g h g≤h h-mono oz = nextFix-mono-in-g g h g≤h h-mono oz |
| 107 | +deriv-mono-in-g g h g≤h h-mono (osuc β) = |
| 108 | + ≤′-trans {nextFix g (deriv g β)} {nextFix h (deriv g β)} {nextFix h (deriv h β)} |
| 109 | + (nextFix-mono-in-g g h g≤h h-mono (deriv g β)) |
| 110 | + (nextFix-mono h h-mono {deriv g β} {deriv h β} |
| 111 | + (deriv-mono-in-g g h g≤h h-mono β)) |
| 112 | +deriv-mono-in-g g h g≤h h-mono (olim k) = λ n → |
| 113 | + ≤′-lim {deriv g (k n)} (λ m → deriv h (k m)) n |
| 114 | + (deriv-mono-in-g g h g≤h h-mono (k n)) |
0 commit comments