diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index afbded1..ca205fd 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -253,6 +253,24 @@ honest-bound matched-negative block. the `affine` mode in `EchoObservationalEquivalence`. Honest-bound: NOT side-channel-safe / cryptographic deniability / adaptive adversary. `proofs/agda/EchoDeniability.agda`. `[REAL]` +* *Transaction (rollback safety, issue #174)* — `WriteSet` (staged + mutations) → `RollbackLog` collapsing audit boundary; `rollback` + admits no section, so a discarded write-set is unrecoverable from the + receipt alone (#DB-2.1). Packaged as a `Security` instance + (`transaction-security`), reducing to `no-section-of-collapsing-map`. + Honest-bound: NOT durability / isolation / commit-semantics (the + dual) / savepoint-locality / runtime-memory-zeroed. + `proofs/agda/EchoTransaction.agda`. `[REAL]` +* *Selective projection (σ–π commutativity, issue #176)* — the Codd law + σ_p(π_S(R)) = π_S(σ_p(R)) for column-safe predicates, as an Echo-fibre + set-equality (`_⇔_` of the two result relations per projected value). + `SelectiveProjection` carries the column-safe factoring `p b ⇔ q + (projection b)`; `select-project-commute` is the commutativity; + `no-column-safe-lift` is the counterexample (a projected-away-column + predicate has no column-restricted lift, so σ/π do not commute). + Honest-bound: `_⇔_` is set-equality (full `_↔_` would need + proof-irrelevant predicates); NOT a runtime query planner. + `proofs/agda/EchoSelectiveProjection.agda`. `[REAL]` * *Aggregation (general, issue #175)* — aggregation-as-fold over a `Monoid`, with a `GroupAggregator` and the monoid-homomorphism law `aggregation-as-fold` (aggregating a concatenation = combining the diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc index f7cc508..9044c39 100644 --- a/docs/echo-types/echo-kernel-note.adoc +++ b/docs/echo-types/echo-kernel-note.adoc @@ -125,7 +125,8 @@ kernel** — the boundary is real and lives outside this core. *Application/extension modules* (also added via the same sweep): `EchoEntropy`, `EchoLLEncoding`, `EchoProvenance`, `EchoSecurity`, `EchoProbabilisticSupport`, `EchoDifferential`, `EchoDeniability`, - `EchoAggregation`, `EchoVariance` + `EchoAggregation`, `EchoVariance`, `EchoTransaction`, + `EchoSelectiveProjection` are derived domain applications mapped under their own headings in MAP.adoc. `EchoDeniability` formalises residue deniability: the perfect (constant / no-section) case and the partial (injective / diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 7b06ec4..0cc243a 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -96,6 +96,8 @@ open import EchoDifferential -- Perturbation tracking (audience-facing sensi -- and the injective/section-exists story (partial case), with the -- IsConstantOpener boundary tying deniability to the affine mode. open import EchoDeniability +open import EchoTransaction -- Transaction rollback safety (issue #174; Security instance) +open import EchoSelectiveProjection -- σ–π commutativity (issue #176; relational-algebra carrier) -- Narrative deliverable: curated index of "why Echo deserves a name". open import EchoCanonicalIdentitySuite @@ -127,6 +129,7 @@ open import Ordinal.Brouwer.VeblenPhiNormal -- φ₁ a normal function; next-ε open import Ordinal.Brouwer.VeblenBinary -- binary Veblen φ_α(β) + the diagonal Γ₀ open import Ordinal.Brouwer.VeblenBinaryNormal -- every φ_α a normal function; φ_{α+1} enumerates fixed points of φ_α open import Ordinal.Brouwer.VeblenBinaryMono -- first-arg monotonicity; Γ₀ ≤′ φ_Γ₀(0) (diagonal pre-fixed point) +open import Ordinal.Brouwer.VeblenBinaryLeast -- nextFix is the LEAST pre-fixed point; reverse-Γ₀ reduced to one closure open import Ordinal.Brouwer.StrictLeftMonoRefuted open import Ordinal.Brouwer.AdditivePrincipalGenericRefuted open import Ordinal.Buchholz.Syntax diff --git a/proofs/agda/EchoSelectiveProjection.agda b/proofs/agda/EchoSelectiveProjection.agda new file mode 100644 index 0000000..670c5f5 --- /dev/null +++ b/proofs/agda/EchoSelectiveProjection.agda @@ -0,0 +1,164 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell + +-- EchoSelectiveProjection: the relational-algebra selection/projection +-- commutativity (the subset case) as an Echo-fibre statement. Closes +-- echo-types#174's sibling echo-types#176 (consumer: affinescript +-- db-theory #4, `stdlib/Select.affine`). +-- +-- The classical law (Codd): for selection σ_p (predicate-driven row +-- filter) and projection π_S (column-subset), +-- +-- σ_p(π_S(R)) = π_S(σ_p(R)) when p references only columns in S, +-- σ_p(π_S(R)) ≠ π_S(σ_p(R)) when p references a column NOT in S. +-- +-- *Honest level.* "=" between relations is SET equality: same rows. +-- The Echo formalisation states it as a per-projected-value LOGICAL +-- equivalence `_⇔_` of the two result fibres (co-membership), which is +-- exactly set-equality of the result relations. A full `_↔_` (with +-- round-trips) would additionally require the predicate family to be +-- proof-irrelevant (`is-prop`); set-equality does not, and `_⇔_` is the +-- faithful level. See the companion remark. +-- +-- *The column-safe condition.* "p references only columns in S" is +-- formalised as: p factors through the projection — there is a +-- predicate `q : S → Set` on the projected columns with `p b ⇔ q +-- (projection b)` for every record `b`. This `factors` field IS the +-- "uses only columns in S" hypothesis. +-- +-- *The Echo content.* With `pf = projection ∘ f` (the projected map), +-- `Echo pf s` is π_S(R) at projected value `s` — the rows projecting to +-- `s`. The two composites: +-- +-- ProjectSelect s = Σ (Echo pf s) (λ e → p (f (proj₁ e))) +-- -- π_S(σ_p(R)) at s: rows projecting to s that satisfy p +-- SelectProject s = Σ (Echo pf s) (λ _ → q s) +-- -- σ_q(π_S(R)) at s: rows projecting to s, kept iff q holds at s +-- +-- `select-project-commute` is `∀ s → ProjectSelect s ⇔ SelectProject s`. +-- The proof is K-free: pattern-matching the fibre witness `pf x ≡ s` as +-- `refl` (s a free variable, so --without-K-safe) collapses the +-- transport, and the predicate move is exactly the `factors` field. +-- +-- *The counterexample.* `no-column-safe-lift` shows a predicate that +-- reads a projected-away column (`proj₂`, with projection `= proj₁`) +-- admits NO column-restricted lift `q` at all: the records `(true,true)` +-- and `(true,false)` share projection `true` but disagree on the +-- predicate, so any `q true` would be both inhabited and empty. This is +-- the "≠" direction: σ and π do not commute for such a predicate. +-- +-- Headlines (pinned in Smoke.agda): +-- * SelectiveProjection -- the column-safe setup record +-- * select-project-commute -- σ–π commute (column-safe), per s +-- * column-safe-example -- worked column-safe instance +-- * no-column-safe-lift -- counterexample (non-column-safe ⇒ ✗) + +module EchoSelectiveProjection where + +open import Echo using (Echo) +open import Data.Product.Base using (Σ; _,_; proj₁; proj₂; _×_) +open import Data.Bool.Base using (Bool; true; false) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) +open import Relation.Nullary using (¬_) + +---------------------------------------------------------------------- +-- Logical equivalence (set-equality level). Kept local and minimal — +-- the σ–π law is co-membership of the two result relations, not a +-- structure-carrying bijection. +---------------------------------------------------------------------- + +record _⇔_ (P Q : Set) : Set where + constructor equiv + field + to : P → Q + from : Q → P + +---------------------------------------------------------------------- +-- The column-safe selection/projection setup. +---------------------------------------------------------------------- + +record SelectiveProjection {A B : Set} (f : A → B) (S : Set) : Set₁ where + field + projection : B → S -- π_S + p : B → Set -- σ predicate on full records + q : S → Set -- its restriction to the projected columns + -- "p uses only columns in S": p factors through projection as q. + factors : ∀ b → p b ⇔ q (projection b) + + -- The projected map; `Echo pf s` = π_S(R) at projected value s. + pf : A → S + pf a = projection (f a) + + -- π_S(σ_p(R)) at s : rows projecting to s that satisfy p. + ProjectSelect : S → Set + ProjectSelect s = Σ (Echo pf s) (λ e → p (f (proj₁ e))) + + -- σ_q(π_S(R)) at s : rows projecting to s, kept iff q holds at s. + SelectProject : S → Set + SelectProject s = Σ (Echo pf s) (λ _ → q s) + +---------------------------------------------------------------------- +-- σ–π commute (column-safe): the two result relations co-inhabit at +-- every projected value. Set-equality of σ_p(π_S(R)) and π_S(σ_p(R)). +---------------------------------------------------------------------- + +select-project-commute : + ∀ {A B : Set} {f : A → B} {S : Set} (sp : SelectiveProjection f S) (s : S) → + SelectiveProjection.ProjectSelect sp s ⇔ SelectiveProjection.SelectProject sp s +select-project-commute {f = f} sp s = equiv to from + where + open SelectiveProjection sp + to : ProjectSelect s → SelectProject s + to ((x , refl) , pe) = (x , refl) , _⇔_.to (factors (f x)) pe + from : SelectProject s → ProjectSelect s + from ((x , refl) , qs) = (x , refl) , _⇔_.from (factors (f x)) qs + +---------------------------------------------------------------------- +-- Worked column-safe instance: 2-column Bool records, project to +-- column 0, predicate "column 0 is true" — uses only the projected +-- column, so it factors (the identity equivalence). +---------------------------------------------------------------------- + +column-safe-example : SelectiveProjection {Bool × Bool} {Bool × Bool} (λ b → b) Bool +column-safe-example = record + { projection = proj₁ + ; p = λ b → proj₁ b ≡ true + ; q = λ s → s ≡ true + ; factors = λ b → equiv (λ z → z) (λ z → z) + } + +---------------------------------------------------------------------- +-- Counterexample (the "≠" direction): a predicate reading a +-- projected-away column has NO column-restricted lift. `(true,true)` +-- and `(true,false)` share projection `true` but disagree on +-- `proj₂ · ≡ true`, so any candidate `q true` is both inhabited and +-- empty. Hence σ and π do not commute for such a predicate. +---------------------------------------------------------------------- + +no-column-safe-lift : + ¬ Σ (Bool → Set) (λ q → ∀ b → (proj₂ b ≡ true) ⇔ q (proj₁ b)) +no-column-safe-lift (q , fac) + with _⇔_.from (fac (true , false)) (_⇔_.to (fac (true , true)) refl) +... | () + +---------------------------------------------------------------------- +-- Companion remark. +-- +-- `_⇔_` (set-equality of the result relations) is the faithful level: +-- relational-algebra equality is membership equality. Upgrading to a +-- structure-preserving `_↔_` would need the predicate family to be +-- proof-irrelevant (an `is-prop (p b)` field); under `--safe +-- --without-K` that is an extra hypothesis, not free, and it adds no +-- relational-algebra content. NOT claimed: σ–π commutativity for +-- arbitrary (non-column-safe) predicates (refuted by +-- `no-column-safe-lift`); any runtime query-planner behaviour (the +-- decision of whether a predicate is column-safe lives in the +-- consumer). The carrier encodes only the property. +---------------------------------------------------------------------- + +NotProved-arbitrary-predicate-commute : Set +NotProved-arbitrary-predicate-commute = Bool + +NotProved-runtime-query-planner : Set +NotProved-runtime-query-planner = Bool diff --git a/proofs/agda/EchoTransaction.agda b/proofs/agda/EchoTransaction.agda new file mode 100644 index 0000000..c5f1cb6 --- /dev/null +++ b/proofs/agda/EchoTransaction.agda @@ -0,0 +1,177 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell + +-- EchoTransaction: SQL transaction rollback safety as an instance of the +-- generic no-section theorem. Closes echo-types#174 (consumer: +-- affinescript db-theory #2, `stdlib/Transaction.affine`, +-- `docs/academic/proofs/db-theory-2-transaction-safety.md` #DB-2.1). +-- +-- !! HONEST BOUND, STATED UP FRONT !! +-- +-- `rollback-discards-writes` is a TYPE-LEVEL guarantee that no pure Agda +-- function reconstructs a discarded write-set from the rollback receipt +-- alone (factored through +-- `EchoNoSectionGeneric.no-section-of-collapsing-map`). It is NOT: +-- * `durability` — a claim about writes surviving a crash; +-- * `isolation` — a claim about concurrent-transaction visibility; +-- * `commit-semantics` — #DB-2.2 commit-promotes-writes is the DUAL +-- (commit PRESERVES writes, so it is not a +-- no-section statement at all); +-- * `savepoint-locality` — #DB-2.3 is a structural/runtime nesting +-- claim outside this carrier; +-- * `runtime-memory-zeroed` — a claim about physical memory contents. +-- Conflating any of these with `rollback-discards-writes` is the category +-- error the matched-negative block at the bottom heads off. Same +-- honest-bound discipline as `EchoSecurity` / `RegionExitAudit` +-- (R-2026-05-18). +-- +-- *Structural content (#DB-2.1).* A transaction's staged-but-uncommitted +-- writes are an affine resource; `rollback` consumes that resource and +-- emits a receipt that records only THAT a rollback occurred, never which +-- writes were discarded. Two distinct write-sets therefore collapse to +-- the same receipt, so `rollback` admits no section: a post-rollback +-- caller holding only the receipt cannot type-check a function returning +-- the discarded write-set. This is precisely "the one consumption that +-- discards is observationally equivalent to never having started". +-- +-- This is the first `Security` instance outside the original region-exit +-- audit setting (`EchoSecurity.region-exit-audit-instance`), establishing +-- that any bracketed-mutation resource — transactions, scoped +-- capabilities, scoped logs — reduces to the same generic lemma. +-- +-- Headlines (pinned in Smoke.agda): +-- +-- * Mutation / WriteSet / RollbackLog -- the carrier types +-- * rollback -- the collapsing audit boundary +-- * rollback-discards-writes -- #DB-2.1, direct no-section +-- * transaction-security -- the `Security` instance +-- * rollback-no-recovery -- #DB-2.1 via the abstract theorem +-- +-- Scope guardrail (Echo-vs-Σ clearance). `rollback-discards-writes` uses +-- `no-section-of-collapsing-map` directly, whose three-line trans/sym/cong +-- proof is the canonical non-trivial Echo-typed content; replacing it with +-- a bare `Σ` + `_≡_` would lose the collapse/no-section content. The +-- `NotProved-*` aliases pin the honest scope. + +module EchoTransaction where + +open import EchoNoSectionGeneric using (no-section-of-collapsing-map) +open import EchoSecurity using (Security; module SecurityTheorems) + +open import Data.Nat.Base using (ℕ) +open import Data.List.Base using (List; []; _∷_) +open import Data.Product.Base using (Σ) +open import Data.Unit.Base using (⊤; tt) +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl) +open import Relation.Nullary using (¬_) + +---------------------------------------------------------------------- +-- The carrier. +-- +-- A `Mutation` is an opaque cell-write (address, value); a `WriteSet` is +-- the ordered list a transaction has staged but not committed. The +-- `RollbackLog` receipt is information-free: it records only that a +-- rollback happened. +---------------------------------------------------------------------- + +data Mutation : Set where + set-cell : ℕ → ℕ → Mutation + +WriteSet : Set +WriteSet = List Mutation + +data RollbackLog : Set where + rolled-back : RollbackLog + +-- The audit boundary: rollback collapses every write-set to the single +-- receipt, discarding the staged mutations. +rollback : WriteSet → RollbackLog +rollback _ = rolled-back + +---------------------------------------------------------------------- +-- The audit witnesses: two distinct write-sets that collapse identically. +---------------------------------------------------------------------- + +ws₁ ws₂ : WriteSet +ws₁ = [] +ws₂ = set-cell 0 1 ∷ [] + +ws₁≢ws₂ : ws₁ ≢ ws₂ +ws₁≢ws₂ () + +rollback-collapses : rollback ws₁ ≡ rollback ws₂ +rollback-collapses = refl + +---------------------------------------------------------------------- +-- #DB-2.1 rollback-discards-writes (headline): no pure function +-- reconstructs a discarded write-set from the rollback receipt alone. +---------------------------------------------------------------------- + +rollback-discards-writes : + ¬ Σ (RollbackLog → WriteSet) (λ recover → ∀ ws → recover (rollback ws) ≡ ws) +rollback-discards-writes = + no-section-of-collapsing-map rollback ws₁ ws₂ ws₁≢ws₂ rollback-collapses + +---------------------------------------------------------------------- +-- The same guarantee as a `Security` instance, so the transaction +-- carrier joins the EchoSecurity audience family. A single transaction +-- scope is the (trivial) `RegionId`; `audit-no-recovery-at` re-derives +-- #DB-2.1 through the abstract theorem, witnessing that the instance is +-- real (not merely structurally similar). +---------------------------------------------------------------------- + +transaction-security : Security +transaction-security = record + { RegionId = ⊤ + ; Resource = λ _ → WriteSet + ; Receipt = λ _ → RollbackLog + ; exit = λ _ → rollback + ; res₁ = λ _ → ws₁ + ; res₂ = λ _ → ws₂ + ; res-distinct = λ _ → ws₁≢ws₂ + ; exit-collapses = λ _ → rollback-collapses + } + +rollback-no-recovery : + (r : ⊤) → + ¬ Σ (RollbackLog → WriteSet) (λ recover → ∀ ws → recover (rollback ws) ≡ ws) +rollback-no-recovery = SecurityTheorems.audit-no-recovery-at transaction-security + +---------------------------------------------------------------------- +-- Matched-negative block (HONEST BOUND, per R-2026-05-18 discipline). +-- +-- `⊤`-aliased so `grep NotProved` catches them. A consumer citing +-- `rollback-discards-writes` beyond these scopes is making a category +-- error: the guarantee is exactly "no pure Agda function reconstructs +-- the discarded write-set from the receipt alone, inside this model". +---------------------------------------------------------------------- + +NotProved-durability : Set +NotProved-durability = ⊤ + +NotProved-isolation : Set +NotProved-isolation = ⊤ + +NotProved-commit-semantics : Set -- #DB-2.2 is the dual, not a no-section +NotProved-commit-semantics = ⊤ + +NotProved-savepoint-locality : Set -- #DB-2.3 is structural/runtime +NotProved-savepoint-locality = ⊤ + +NotProved-runtime-memory-zeroed : Set +NotProved-runtime-memory-zeroed = ⊤ + +---------------------------------------------------------------------- +-- Companion remark. +-- +-- #DB-2.2 (commit-promotes-writes) is the dual of #DB-2.1: commit +-- PRESERVES the write-set, so it is an equality/section statement, not a +-- no-section one — it belongs in a separate carrier and is deliberately +-- not modelled here. #DB-2.3 (savepoint-locality) is a nesting/structural +-- property of the transaction tree; it too is out of scope for this +-- minimal rollback-safety carrier. The `Mutation` / `RollbackLog` types +-- are placeholders chosen for inhabitability + a clean distinctness +-- witness; the proof goes through for any carrier with two distinct +-- write-sets collapsing to the same receipt. +---------------------------------------------------------------------- diff --git a/proofs/agda/Ordinal/Brouwer/VeblenBinaryLeast.agda b/proofs/agda/Ordinal/Brouwer/VeblenBinaryLeast.agda new file mode 100644 index 0000000..e8010b0 --- /dev/null +++ b/proofs/agda/Ordinal/Brouwer/VeblenBinaryLeast.agda @@ -0,0 +1,101 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell + +-- Binary Veblen — RUNG 7: the generic fixed-point engine is MINIMAL — +-- `nextFix g x` is the LEAST pre-fixed point of `g` strictly above `x`, +-- not merely *a* fixed point. Target-side climb toward ψ₀(Ω_ω) (BH +-- order-type fidelity, open problem D-2026-06-14). Builds on +-- `VeblenBinary` (the engine + Γ₀) and `VeblenBinaryNormal` +-- (`φ-mono₂` / `commonStep-mono`). 2026-06-20. +-- +-- ## What this slice adds +-- +-- `VeblenBinary` proved `nextFix g x` is a fixed point of `g` +-- (`nextFix-fixed-{≤,≥}`) lying strictly above `x` (`nextFix-above`). +-- The missing half of the engine's correctness is MINIMALITY: +-- +-- * `nextFix-least` — for monotone `g`, if `x <′ z` and `g z ≤′ z` +-- (z is a pre-fixed point of g strictly above x) then +-- `nextFix g x ≤′ z`. So `nextFix g x` is the LEAST pre-fixed +-- point of g strictly above x. Proof: every approximant of the +-- iteration tower `g-tower g (osuc x)` is `≤′ z` — the base by +-- `x <′ z`, each successor by monotonicity into the pre-fixed +-- point `g z ≤′ z`; the supremum is then `≤′ z` definitionally +-- (`olim T ≤′ z` unfolds to `∀ n → T n ≤′ z`). +-- +-- This is exactly the tool the reverse Γ₀ fixed-point direction (and +-- "Γ₀ is the LEAST diagonal fixed point") needs, and which +-- `VeblenBinaryMono` flagged as the open "common-fixed-point-from-above" +-- piece. As an immediate payoff: +-- +-- * `Γ₀-fixed-from-closure` — REDUCES the open reverse direction +-- `φ_Γ₀(0) ≤′ Γ₀` to a single closure obligation +-- `commonStep (n ↦ φ_{Γ-tower n}) Γ₀ ≤′ Γ₀` (Γ₀ is closed under +-- every diagonal-approximant level applied to Γ₀ itself). Because +-- `φ Γ₀ oz` is, definitionally, `nextFix (commonStep …) oz`, the +-- reduction is just `nextFix-least` at `x = oz`, `z = Γ₀` +-- (`Γ₀-pos` supplies `oz <′ Γ₀`). +-- +-- ## Honest scope (still a LONG climb — do not overclaim) +-- +-- `nextFix-least` is a real, unconditional theorem. `Γ₀-fixed-from- +-- closure` is a CONDITIONAL: it does NOT prove `φ_Γ₀(0) ≤′ Γ₀`; it +-- proves it FOLLOWS from the closure `commonStep F Γ₀ ≤′ Γ₀`, which +-- needs general first-argument monotonicity and REMAINS OPEN (the next +-- slice). Combined with `VeblenBinaryMono.Γ₀-prefixed` (the `≤′` +-- direction), discharging that one closure obligation would give the +-- full bi-`≤′` fixed point `Γ₀ ≃ φ_Γ₀(0)`. ψ₀(Ω_ω) sits far above Γ₀ +-- behind the ordinal-collapsing layer; order-type fidelity REMAINS OPEN +-- (D-2026-06-14). No postulate is closed. + +module Ordinal.Brouwer.VeblenBinaryLeast where + +open import Data.Nat.Base using (ℕ; zero; suc) + +open import Ordinal.Brouwer using (Ord; oz; osuc; olim) +open import Ordinal.Brouwer.Phase13 using (_≤′_; _<′_; ≤′-trans) +open import Ordinal.Brouwer.VeblenBinary + using (g-tower; nextFix; deriv; commonStep; φ; Γ-tower; Γ₀; Γ₀-pos) +open import Ordinal.Brouwer.VeblenBinaryNormal using (φ-mono₂; commonStep-mono) + +---------------------------------------------------------------------- +-- Minimality of the generic fixed-point engine. +-- +-- `nextFix g x = olim (g-tower g (osuc x))`, so `nextFix g x ≤′ z` +-- unfolds (by the `olim f ≤′ β = ∀ n → f n ≤′ β` clause of `_≤′_`) to +-- "every tower approximant is `≤′ z`". We prove that by induction on +-- the tower index against a pre-fixed point `z` strictly above `x`. +---------------------------------------------------------------------- + +nextFix-least : + (g : Ord → Ord) (g-mono : ∀ {a b} → a ≤′ b → g a ≤′ g b) + {x z : Ord} → x <′ z → g z ≤′ z → nextFix g x ≤′ z +nextFix-least g g-mono {x} {z} x