|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Phase 1.3 — STATUS: scaffolding only. The recursive `_≤′_` |
| 4 | +-- definition lands here, plus `osuc-mono-≤′ p = p` (the bullseye |
| 5 | +-- lemma). `≤′-refl` for the `olim f` case requires `f-in-lim′`, |
| 6 | +-- which is the documented obstacle described below. |
| 7 | +-- |
| 8 | +-- This module compiles under `--safe --without-K`. Anything that |
| 9 | +-- depends on the open `f-in-lim′` is left out so the file is honest: |
| 10 | +-- what's here is provable, what's not here is exactly the work |
| 11 | +-- remaining. |
| 12 | +-- |
| 13 | +-- ## Background |
| 14 | +-- |
| 15 | +-- Echidna's SA design-search recommended switching `Ordinal.Brouwer._≤_` |
| 16 | +-- to a fully-recursive shape (energy [0, 0, 1, 0]; both single-chain |
| 17 | +-- and 4-agent swarm unanimous). The data-style alternative |
| 18 | +-- (`data + ≤-cong-suc`) was tested by hand-trace and rejected — the |
| 19 | +-- new constructor cascades into mutually-recursive `pred-of-osuc` |
| 20 | +-- proofs that need to be redesigned alongside. |
| 21 | +-- |
| 22 | +-- See `echidna/docs/decisions/2026-04-28-corpus-and-design-search.md` |
| 23 | +-- and `echo-types/docs/echidna-design-search-2026-04-28.adoc` for |
| 24 | +-- the full design-search log. |
| 25 | +-- |
| 26 | +-- ## What's done |
| 27 | +-- |
| 28 | +-- * Recursive `_≤′_` defined; passes Agda's coverage + termination |
| 29 | +-- checks under `--safe --without-K`. |
| 30 | +-- * `osuc-mono-≤′ p = p` — the Phase-1.3 bullseye is identity. |
| 31 | +-- * `≤′-zero` — definitional from the `oz ≤ _ = ⊤` clause. |
| 32 | +-- * `osuc-mono-<′` — strict version, also identity-shaped. |
| 33 | +-- |
| 34 | +-- ## What's open |
| 35 | +-- |
| 36 | +-- * `≤′-refl` for the `olim f` case is `(n : ℕ) → f n ≤′ olim f`, |
| 37 | +-- which requires `f-in-lim′ : ∀ f n → f n ≤′ olim f`. The |
| 38 | +-- `f-in-lim′` proof has three sub-cases (per `f n`'s constructor); |
| 39 | +-- the `oz` and `osuc α` cases are routine, but the `olim g` case |
| 40 | +-- (where `f n = olim g`) is the documented obstacle. |
| 41 | +-- |
| 42 | +-- The `olim g` case wants `(m : ℕ) → g m ≤′ olim f`. Termination is |
| 43 | +-- fine — `g m` is strictly smaller than `f n = olim g`, so structural |
| 44 | +-- recursion goes through — but Agda's `with f n` pattern loses the |
| 45 | +-- equation `f n ≡ olim g`, leaving the goal in a shape Foetus can't |
| 46 | +-- verify is decreasing. |
| 47 | +-- |
| 48 | +-- Two viable closure paths: |
| 49 | +-- |
| 50 | +-- 1. Mutual definition with `≤′-trans`. Then the `olim g` case |
| 51 | +-- becomes `≤′-trans (f-in-lim′ g m) (f-in-lim′ f n)` — both |
| 52 | +-- calls are structurally smaller, and Foetus accepts mutual |
| 53 | +-- structural recursion when each call shrinks one of the |
| 54 | +-- lex-ordered measures. |
| 55 | +-- |
| 56 | +-- 2. Strengthen `f-in-lim′` to carry an accessibility witness for |
| 57 | +-- the limit — `(∀ k → Acc _<′_ (f k)) → f n ≤′ olim f`. This |
| 58 | +-- makes the recursion structure visible to Foetus directly. |
| 59 | +-- |
| 60 | +-- The Phase-1.3 follow-up commit lands either path; for now the |
| 61 | +-- recursive shape stands up + the bullseye lemma compiles. |
| 62 | + |
| 63 | +module Ordinal.Brouwer.Phase13 where |
| 64 | + |
| 65 | +open import Data.Nat.Base using (ℕ) |
| 66 | +open import Data.Product.Base using (Σ) |
| 67 | +open import Data.Unit.Base using (⊤; tt) |
| 68 | +open import Data.Empty using (⊥) |
| 69 | + |
| 70 | +open import Ordinal.Brouwer using (Ord; oz; osuc; olim) |
| 71 | + |
| 72 | +---------------------------------------------------------------------------- |
| 73 | +-- Recursive `_≤′_` per the Echidna SA recommendation |
| 74 | +---------------------------------------------------------------------------- |
| 75 | + |
| 76 | +infix 4 _≤′_ |
| 77 | + |
| 78 | +_≤′_ : Ord → Ord → Set |
| 79 | +oz ≤′ _ = ⊤ |
| 80 | +osuc α ≤′ oz = ⊥ |
| 81 | +osuc α ≤′ osuc β = α ≤′ β |
| 82 | +osuc α ≤′ olim f = Σ ℕ (λ n → osuc α ≤′ f n) |
| 83 | +olim f ≤′ β = (n : ℕ) → f n ≤′ β |
| 84 | + |
| 85 | +---------------------------------------------------------------------------- |
| 86 | +-- Phase-1.3 bullseye: osuc-mono-≤′ is identity |
| 87 | +---------------------------------------------------------------------------- |
| 88 | + |
| 89 | +-- Under the recursive definition, `osuc α ≤′ osuc β` reduces |
| 90 | +-- definitionally to `α ≤′ β`. No structural recursion on the proof, |
| 91 | +-- no case split on α or β. This is the entire point of the |
| 92 | +-- redesign — what was a non-trivial induction in the data-`_≤_` |
| 93 | +-- shape collapses to identity. |
| 94 | + |
| 95 | +osuc-mono-≤′ : ∀ {α β} → α ≤′ β → osuc α ≤′ osuc β |
| 96 | +osuc-mono-≤′ p = p |
| 97 | + |
| 98 | +-- Strict version follows immediately. α <′ β is `osuc α ≤′ β`. |
| 99 | + |
| 100 | +infix 4 _<′_ |
| 101 | + |
| 102 | +_<′_ : Ord → Ord → Set |
| 103 | +α <′ β = osuc α ≤′ β |
| 104 | + |
| 105 | +osuc-mono-<′ : ∀ {α β} → α <′ β → osuc α <′ osuc β |
| 106 | +osuc-mono-<′ p = p |
| 107 | + |
| 108 | +---------------------------------------------------------------------------- |
| 109 | +-- Trivial corollaries (all definitional) |
| 110 | +---------------------------------------------------------------------------- |
| 111 | + |
| 112 | +≤′-zero : ∀ {α} → oz ≤′ α |
| 113 | +≤′-zero = tt |
| 114 | + |
| 115 | +-- `oz <′ α` for α nonzero. Since `oz <′ α = osuc oz ≤′ α`, we case on α. |
| 116 | + |
| 117 | +oz<′osuc : ∀ {α} → oz <′ osuc α |
| 118 | +oz<′osuc {α} = ≤′-zero {α} |
0 commit comments