From e822b8f938555f130f718463f00ed82d7b890ad9 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 02:25:08 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20forget-witness-encoding-has-section=20?= =?UTF-8?q?=E2=80=94=20universal=20LL-encoding=20gap?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Strengthens EchoLLEncoding's existence theorem (`ll-encoding-gap`, the trivial ⊤-shadow) to the UNIVERSAL form over the forget-witness class: every shallow LL encoding whose `X linear` is a proposition (no inhabitant-level witness at the linear mode) admits an encoded section of `wX`. The section is the constant map at a fixed linear inhabitant `enc echo-true`, correct by forget-witness propositionality — uniform over the class, no cherry-picked carrier. - `ForgetsWitness E = (x y : X linear) → x ≡ y` — the invariant. - `forget-witness-encoding-has-section` — the universal headline. - `trivial-forgets-witness` — the ⊤-shadow is in the class. - `trivial-via-universal` — the existence form recovered from the universal one (the generalisation is checked, not asserted). Sharpens the dichotomy: forget the witness ⇒ a section always exists; keep it (`X linear` not a proposition) ⇒ no-section may be preserved, but the encoding is then no longer the standard `!A := 1` shadow. Header headline list, scope guardrail, and companion remark updated to match. `--safe --without-K`, zero postulates. 4 Smoke pins; `EchoLLEncoding` already classified (no new module). EchoLLEncoding + Smoke.agda + All.agda exit 0; kernel-guard PASS. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We --- proofs/agda/EchoLLEncoding.agda | 96 +++++++++++++++++++++++++++------ proofs/agda/Smoke.agda | 4 ++ 2 files changed, 84 insertions(+), 16 deletions(-) diff --git a/proofs/agda/EchoLLEncoding.agda b/proofs/agda/EchoLLEncoding.agda index 965b4cf..9f9458e 100644 --- a/proofs/agda/EchoLLEncoding.agda +++ b/proofs/agda/EchoLLEncoding.agda @@ -56,15 +56,26 @@ -- * source-no-section -- matched-negative: source-side -- no-section-weaken (cited) -- * gap-paired -- gap + source matched in one Σ +-- * ForgetsWitness -- the forget-witness invariant +-- (`X linear` a proposition) +-- * forget-witness-encoding-has-section -- UNIVERSAL form: every +-- forget-witness encoding has a +-- section +-- * trivial-forgets-witness -- the trivial shadow is in the class +-- * trivial-via-universal -- existence form recovered from the +-- universal one (checked) -- --- Scope guardrail. The theorem proved is the *existence* of an LL- --- shallow encoding with an encoded section. It is NOT a claim that --- *every* LL encoding loses the no-section property — a sufficiently --- rich encoding (one that keeps the witness equality in `X linear`) --- could in principle preserve it. The interesting content is that --- the *standard* LL collapse — sending `!A` to a forget-resources --- shadow — already loses it. The companion remark at the end of the --- file makes this explicit. +-- Scope guardrail. Two strengths are proved. (1) `ll-encoding-gap` is the +-- *existence* of an LL-shallow encoding with an encoded section. +-- (2) `forget-witness-encoding-has-section` is the *universal* form over +-- the *forget-witness class*: every encoding whose `X linear` is a +-- proposition (no inhabitant-level witness at the linear mode) has an +-- encoded section. What remains NOT claimed is universality over *all* +-- encodings: an encoding that does NOT forget the witness (re-introduces +-- the second-projection equality into `X linear`, so `X linear` is not a +-- proposition) could preserve no-section — but it is then no longer the +-- standard `!A := 1` LL shadow. The companion remark sharpens this +-- dichotomy. module EchoLLEncoding where @@ -74,6 +85,7 @@ open import EchoLinear ; weaken ; no-section-weaken ) +open import EchoCharacteristic using (echo-true) open import Data.Product.Base using (Σ; _,_; proj₁; proj₂; _×_) open import Data.Unit.Base using (⊤; tt) @@ -201,17 +213,69 @@ gap-paired : (λ raise → ∀ e → raise (weaken e) ≡ e)) gap-paired = ll-encoding-gap , source-no-section +---------------------------------------------------------------------- +-- The universal form: the gap holds for the WHOLE forget-witness class. +-- +-- `ll-encoding-gap` is an existence statement (the trivial shadow). The +-- strengthening below pins the *universal* content the audit asked for: +-- EVERY shallow LL encoding that *forgets the witness* admits an encoded +-- section of `wX`. "Forgets the witness" is made precise as `X linear` +-- being a *proposition* (a subsingleton) — no inhabitant-level +-- distinction survives at the linear mode, exactly the data +-- `no-section-weaken` depends on. The standard `!A := 1` shadow is the +-- minimal member of this class; so is any `X m := F m` with `F` constant +-- on inhabitants. +-- +-- The section is the constant map at a fixed linear inhabitant +-- `enc echo-true`, correct because forget-witness propositionality makes +-- every `X linear` element equal to it. No cherry-picked carrier: the +-- argument is uniform over the class. +---------------------------------------------------------------------- + +-- The forget-witness invariant: `X linear` is a proposition. +ForgetsWitness : LLShallowEncoding → Set +ForgetsWitness E = let open LLShallowEncoding E in (x y : X linear) → x ≡ y + +-- Universal headline: any forget-witness shallow LL encoding has an +-- encoded section, so the encoded analogue of `no-section-weaken` fails +-- across the whole class — not merely at the trivial shadow. +forget-witness-encoding-has-section : + (E : LLShallowEncoding) → ForgetsWitness E → + let open LLShallowEncoding E + in Σ (X affine → X linear) (λ s → ∀ x → s (wX x) ≡ x) +forget-witness-encoding-has-section E prop = + let open LLShallowEncoding E + in (λ _ → enc {linear} echo-true) , (λ x → prop (enc {linear} echo-true) x) + +-- The trivial `⊤`-shadow is a member of the forget-witness class +-- (`X linear = ⊤` is a proposition)… +trivial-forgets-witness : ForgetsWitness trivial-encoding +trivial-forgets-witness tt tt = refl + +-- …so the existence form `trivial-encoding-has-section` is recovered as +-- the universal form instantiated at the trivial encoding — the +-- generalisation is checked, not merely asserted. +trivial-via-universal : + let open LLShallowEncoding trivial-encoding + in Σ (X affine → X linear) (λ s → ∀ x → s (wX x) ≡ x) +trivial-via-universal = + forget-witness-encoding-has-section trivial-encoding trivial-forgets-witness + ---------------------------------------------------------------------- -- Companion remark on what is NOT claimed. -- --- * This is an EXISTENCE statement: there exists a shallow LL --- encoding under which `no-section-weaken` fails to lift. It is --- NOT a universal statement that every conceivable LL-style --- encoding loses the property. A sufficiently rich encoding — one --- that re-introduces the second-projection equality witness into --- `X linear` — could preserve no-section, but such an encoding is --- no longer the standard `!A := 1` LL shadow; it has smuggled the --- Echo structure back in. +-- * The result is now SHARP, in two strengths. `ll-encoding-gap` is the +-- existence statement (the trivial shadow loses no-section). +-- `forget-witness-encoding-has-section` is universal over the +-- forget-witness class: EVERY encoding whose `X linear` is a +-- proposition loses it. The dichotomy is exact — forget the witness +-- (`X linear` a proposition) ⇒ an encoded section always exists; keep +-- the witness (re-introduce the second-projection equality into +-- `X linear`, so it is not a proposition) ⇒ no-section may be +-- preserved, but the encoding is then no longer the standard +-- `!A := 1` LL shadow; it has smuggled the Echo structure back in. +-- So the *only* way for a shallow LL encoding to carry Echo's +-- no-section discipline is to stop being a witness-forgetting shadow. -- -- * The encoding gap is therefore best read as: "the standard LL -- `!A` interpretation is too weak to be a faithful translation of diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index f9b4092..a002a2e 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -671,6 +671,10 @@ open import EchoLLEncoding using ; ll-encoding-gap ; source-no-section ; gap-paired + ; ForgetsWitness + ; forget-witness-encoding-has-section + ; trivial-forgets-witness + ; trivial-via-universal ) -- examples.EchoVsSigma — Track C of the Echo-vs-Σ identity claim.