From fddb8d0069bdcae72a7c169ca33b538efb1acebf Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 10:46:07 +0000 Subject: [PATCH 1/3] =?UTF-8?q?proof(db):=20EchoTransaction=20=E2=80=94=20?= =?UTF-8?q?rollback=20discards=20writes=20(no-section);=20closes=20#174?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit SQL transaction rollback safety as a Security instance reducing to no-section-of-collapsing-map (affinescript db-theory #2 / #DB-2.1). A staged WriteSet is an affine resource; rollback collapses it to an information-free RollbackLog, so no pure function recovers the discarded writes from the receipt alone. - proofs/agda/EchoTransaction.agda: Mutation/WriteSet/RollbackLog/rollback, rollback-discards-writes (direct no-section), transaction-security (Security instance), rollback-no-recovery (via the abstract theorem), honest matched-negative block (NOT durability/isolation/commit-dual/ savepoint/runtime-memory). - Wired into All.agda; headlines pinned in Smoke.agda. - Classified in echo-kernel-note.adoc + MAP.adoc (kernel-guard Check B). --safe --without-K, zero postulates. All.agda + Smoke.agda exit 0; kernel-guard PASS. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs --- docs/echo-types/MAP.adoc | 8 ++ docs/echo-types/echo-kernel-note.adoc | 2 +- proofs/agda/All.agda | 1 + proofs/agda/EchoTransaction.agda | 177 ++++++++++++++++++++++++++ proofs/agda/Smoke.agda | 13 ++ 5 files changed, 200 insertions(+), 1 deletion(-) create mode 100644 proofs/agda/EchoTransaction.agda diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index afbded1..9790c2b 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -253,6 +253,14 @@ 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]` * *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..a0e2cba 100644 --- a/docs/echo-types/echo-kernel-note.adoc +++ b/docs/echo-types/echo-kernel-note.adoc @@ -125,7 +125,7 @@ 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` 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..e41749f 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -96,6 +96,7 @@ 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) -- Narrative deliverable: curated index of "why Echo deserves a name". open import EchoCanonicalIdentitySuite 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/Smoke.agda b/proofs/agda/Smoke.agda index a002a2e..ffaf206 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -850,6 +850,19 @@ open import EchoSecurity using ; region-exit-audit-instance ) +-- EchoTransaction — SQL transaction rollback safety (issue #174). The +-- staged write-set is an affine resource; rollback collapses it to an +-- information-free receipt, so no pure function recovers the discarded +-- writes (#DB-2.1). A `Security` instance reducing to no-section. +open import EchoTransaction using + ( WriteSet + ; RollbackLog + ; rollback + ; rollback-discards-writes + ; transaction-security + ; rollback-no-recovery + ) + -- EchoProbabilisticSupport — third audience move per GPT order. -- Abstract `Sampling` record (outcome + index + distinguishability -- witness) with four parametric headline theorems via `module From 79be006a812a2f31ad50363d084a13680fe8b77e Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 10:55:28 +0000 Subject: [PATCH 2/3] =?UTF-8?q?proof(db):=20EchoSelectiveProjection=20?= =?UTF-8?q?=E2=80=94=20=CF=83=E2=80=93=CF=80=20commutativity=20(column-saf?= =?UTF-8?q?e);=20closes=20#176?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Relational-algebra selection/projection commutativity (Codd, subset case) as an Echo-fibre set-equality (affinescript db-theory #4). For a column-safe predicate (p factors through the projection as q), σ_p and π_S commute: ProjectSelect s ⇔ SelectProject s at every projected value. A predicate reading a projected-away column admits no column-restricted lift (no-column-safe-lift) — the non-commuting counterexample. - proofs/agda/EchoSelectiveProjection.agda: local _⇔_ (set-equality level), SelectiveProjection record (column-safe factoring), select-project-commute (K-free via refl-matching the fibre witness), column-safe-example instance, no-column-safe-lift counterexample. - Wired into All.agda; headlines pinned in Smoke.agda. - Classified in echo-kernel-note.adoc + MAP.adoc (kernel-guard Check B). --safe --without-K, zero postulates. All.agda + Smoke.agda exit 0; kernel-guard PASS. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs --- docs/echo-types/MAP.adoc | 10 ++ docs/echo-types/echo-kernel-note.adoc | 3 +- proofs/agda/All.agda | 1 + proofs/agda/EchoSelectiveProjection.agda | 164 +++++++++++++++++++++++ proofs/agda/Smoke.agda | 11 ++ 5 files changed, 188 insertions(+), 1 deletion(-) create mode 100644 proofs/agda/EchoSelectiveProjection.agda diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index 9790c2b..ca205fd 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -261,6 +261,16 @@ honest-bound matched-negative block. 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 a0e2cba..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`, `EchoTransaction` + `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 e41749f..f468e07 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -97,6 +97,7 @@ open import EchoDifferential -- Perturbation tracking (audience-facing sensi -- 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 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/Smoke.agda b/proofs/agda/Smoke.agda index ffaf206..d8f26d5 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -863,6 +863,17 @@ open import EchoTransaction using ; rollback-no-recovery ) +-- EchoSelectiveProjection — relational-algebra σ–π commutativity (issue +-- #176). Column-safe selection commutes with projection (set-equality of +-- the result relations); a projected-away-column predicate admits no +-- column-restricted lift (the non-commuting counterexample). +open import EchoSelectiveProjection using + ( SelectiveProjection + ; select-project-commute + ; column-safe-example + ; no-column-safe-lift + ) + -- EchoProbabilisticSupport — third audience move per GPT order. -- Abstract `Sampling` record (outcome + index + distinguishability -- witness) with four parametric headline theorems via `module From 44e3325b88780de312acb3ecffe5dc822def7c5e Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 11:02:27 +0000 Subject: [PATCH 3/3] =?UTF-8?q?proof(ordinal):=20nextFix=20is=20the=20LEAS?= =?UTF-8?q?T=20pre-fixed=20point=20(BH=20climb=20rung=207);=20reverse-?= =?UTF-8?q?=CE=93=E2=82=80=20reduced?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The generic Veblen fixed-point engine was proved correct (nextFix g x is *a* fixed point above x) but not minimal. nextFix-least closes that: for monotone g, nextFix g x is the LEAST pre-fixed point of g strictly above x. As payoff, Γ₀-fixed-from-closure reduces the open reverse direction φ_Γ₀(0) ≤′ Γ₀ to a single closure obligation (commonStep (n ↦ φ_{Γ-tower n}) Γ₀ ≤′ Γ₀); with VeblenBinaryMono.Γ₀-prefixed that closure yields the full bi-≤′ fixed point Γ₀ ≃ φ_Γ₀(0). - proofs/agda/Ordinal/Brouwer/VeblenBinaryLeast.agda: nextFix-least (tower induction against a pre-fixed point) + Γ₀-fixed-from-closure (reduction via nextFix-least at x=oz, z=Γ₀). - Wired into All.agda; headlines pinned in Smoke.agda. Honest scope: nextFix-least is unconditional; Γ₀-fixed-from-closure is conditional on the still-open closure (needs general first-arg monotonicity). Order-type fidelity ψ₀(Ω_ω) REMAINS OPEN (D-2026-06-14). --safe --without-K, zero postulates. All.agda + Smoke.agda exit 0; kernel-guard PASS. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs --- proofs/agda/All.agda | 1 + .../Ordinal/Brouwer/VeblenBinaryLeast.agda | 101 ++++++++++++++++++ proofs/agda/Smoke.agda | 12 +++ 3 files changed, 114 insertions(+) create mode 100644 proofs/agda/Ordinal/Brouwer/VeblenBinaryLeast.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index f468e07..0cc243a 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -129,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/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