backup: WIP snapshot of feat/q2-1-nontruncatable 2026-05-18 (#95)

Non-disruptive remote backup of uncommitted work (NonTruncatable.agda +
characteristic/All.agda + docs). Created via temp-index plumbing; the
local working tree/index/HEAD/branch were NOT modified. Restore notes in
the agent report. Not a merge target.

Author: hyperpolymath

docs/adjacency/README.adoc

@@ -32,10 +32,18 @@ is the family of `echo-not-prop` lemmas formalised in
 * `EpistemicUpdate.echo-not-prop` — eight worlds, four consistent
 * `LinearErasure.echo-not-prop` — two annotated types, one erasure
 
-The general theorem (forwarded as Q2.1 in `next-questions.adoc`):
-for non-injective `f : A → B` with at least two distinct preimages
-of `y`, `is-prop (Echo f y) → ⊥`. The n=2 special cases are proved;
-the general theorem awaits gate-2 evaluation.
+The general theorem (Q2.1 in `next-questions.adoc`): for
+non-injective `f : A → B` with at least two distinct preimages of
+`y`, `is-prop (Echo f y) → ⊥`. **Proved.** The received-`y` form is
+`EchoTruncation.echo-not-prop`, re-exported as
+`characteristic.NonTruncatable.Q2-1`; the stronger constructed-`y`
+form (non-injectivity of `f` *forces* a non-propositional fibre,
+the `y` being produced rather than assumed) is
+`characteristic.NonTruncatable.non-injective⇒echo-not-prop`. The
+gate-2 audit (recorded in that module's header and in
+`next-questions.adoc` §Q2.1) demotes the received-`y` form as
+Σ-reducible and forwards only the constructed-`y` form as a
+candidate nominee.
 
 Truncation arguments are load-bearing against:
 
@@ -305,10 +313,15 @@ meta-note it has no axis engagement; retained for traceability.
 The truncation argument has formal exhibits for three of its
 target neighbours via gate-3's `echo-not-prop` family
 (`TropicalArgmin`, `EpistemicUpdate`, `LinearErasure`). The
-general theorem (Q2.1) is unstated and unproven. Q2.1 is the
-single most leveraged open formalisation: closing it would
-discharge truncation arguments against all four
-truncation-vulnerable neighbours simultaneously.
+general theorem (Q2.1) is now **stated and proved** in
+`characteristic.NonTruncatable` (received-`y` form `Q2-1` plus the
+stronger constructed-`y` form `non-injective⇒echo-not-prop`),
+discharging the truncation argument against all four
+truncation-vulnerable neighbours at the general level rather than
+the three n=2 instances. The remaining open work is the gate-2
+*nomination* decision (the audit demotes the received-`y` form as
+Σ-reducible and forwards only the constructed-`y` form), not the
+formalisation.
 
 The 2-cell argument has formal exhibits for both of its target
 neighbours (quotients via `EchoVsQuotient.Sophisticated`, Galois

docs/echo-types/types-list-note.md

@@ -0,0 +1,131 @@
+# Draft note for the TYPES mailing list
+
+**Status:** draft, not sent. Written to satisfy gate G2 of the
+`types-list` readiness system (a self-contained, honestly sized
+framing note linking a type-checked artifact). Reviewed against the
+list's cardinal rule: *do not present a known notion as a new one.*
+
+Target list: `types-list@lists.seas.upenn.edu`
+(https://lists.seas.upenn.edu/mailman/listinfo/types-list).
+
+---
+
+## Subject
+
+Prior art: fibers studied systematically as the *residue* of
+information-losing maps (mechanised, `--safe --without-K` Agda)
+
+## Body
+
+Dear all,
+
+I have a small mechanised Agda development and a prior-art /
+related-work question. I want to be explicit up front about what is
+**not** new, because the honest framing is the question.
+
+### What the object is (and is not)
+
+The central object is, definitionally, the fiber:
+
+```
+Echo : (f : A → B) → B → Set
+Echo f y = Σ A (λ x → f x ≡ y)
+```
+
+This is `hfiber` / the homotopy fiber. I am **not** claiming a new
+type former. The development (`--safe --without-K`, no postulates,
+no holes, CI-checked; ~13k LOC) is an *editorial* programme: it
+studies fibers **systematically as the structured remainder of
+information-losing computation**, with
+
+1. an 8-axis taxonomy of how such remainders differ (extensional vs
+   intensional, exact vs approximate, local vs global, canonical vs
+   presentation-dependent, compositional vs not, static vs dynamic,
+   proof-relevant vs irrelevant, information-theoretic vs
+   computational access), each axis carrying a distinguishing
+   formalised example; and
+2. a falsifiable identity claim with an explicit retraction
+   protocol, audited per neighbouring framework (refinement types,
+   setoid quotients, Galois/abstract interpretation, provenance
+   semirings, IFC, QTT-style modal calculi, HoTT fibers).
+
+### The two structural distinctness arguments
+
+Against the neighbours, distinctness rests on two arguments, both
+with formal exhibits:
+
+- **Truncation.** For non-injective `f`, `Echo f y` is *not* a mere
+  proposition. General form now proved
+  (`characteristic.NonTruncatable`): a bare non-injectivity witness
+  on `f` *constructs* an output whose echo fibre is non-propositional
+  — the witnessing value is produced, not assumed. (The
+  *received-`y`* form is, honestly, just the generic Σ fact "a Σ
+  with two first-component-distinct elements is not `isProp`"; only
+  the *constructed-`y`* form is more than that.)
+- **2-cell.** The natural 2-cell in the quotient and Galois
+  encodings is itself Σ-over-preimages-shaped (equalizer; lattice
+  meet) — formal exhibits `EchoVsQuotient.Sophisticated`,
+  `EchoVsGalois.Sophisticated`.
+
+A negative result is also recorded rather than hidden: a
+cross-axis "integration recipe" over the five named decoration
+axes does **not** produce substantive simultaneous interaction
+(the EI-2 investigation); the distinctness load is carried only by
+the two arguments above.
+
+### The questions
+
+1. **Prior art for the framing.** Is the *systematic* treatment of
+   fibers-as-information-residue, with an axis taxonomy of this
+   shape, named anywhere I should cite? I know the obvious
+   neighbours (HoTT fibers; container/polynomial functors;
+   lens/optic theory; provenance semirings; QTT). What I am asking
+   is whether the *organising programme* — not the object — has a
+   name in the literature.
+2. **Characteristic-theorem status.** Is the constructed-`y`
+   non-truncatability ("ordinary non-injectivity *forces* a
+   non-propositional fibre", with the bad output produced from the
+   non-injectivity witness) a recognised lemma with a standard
+   citation, or genuinely folklore? I want to attribute it
+   correctly rather than claim it.
+
+Artifact (type-checked, gated, with the honest self-assessment):
+<repo URL>. The relevant module is
+`proofs/agda/characteristic/NonTruncatable.agda`; the taxonomy is
+`docs/echo-types/taxonomy.md`; the falsifiable-claim protocol is
+`roadmap-gates.adoc`.
+
+Grateful for pointers, corrections, or "this is just X under
+another name" — the latter is a useful answer, not a bad one.
+
+Best regards,
+Jonathan Jewell
+
+---
+
+## Pre-send checklist (the readiness gates)
+
+- [x] **G2 — artifact exists.** Q2.1 proved and CI-checked; this
+  note is self-contained and links the repo.
+- [ ] **G1 — prior-art saturation.** Before sending, do one more
+  literature pass on: container/polynomial functors as fiber
+  bookkeeping; "fibre-wise" / display-map framings; Spivak-style
+  data-migration / provenance; any "information residue" usage in
+  PL. The note must survive "isn't this just a polynomial functor /
+  display map?" — pre-empt it in body §1 with one sentence each if a
+  near-hit is found.
+- [x] **G3 — claim correctly sized.** Body opens by conceding the
+  object is the fiber; asks prior-art and attribution questions, not
+  "I invented a notion".
+- [ ] Replace `<repo URL>` with the public URL at send time.
+- [ ] Trim to ≤ ~400 words of body before sending; list readers
+  reward brevity. The taxonomy enumeration can become "(8 axes;
+  see `taxonomy.md`)".
+
+## Why this is postable now (vs. earlier)
+
+The trigger named in the readiness system was *closing Q2.1*. It is
+closed and CI-checked, so there is now a checkable result behind the
+prior-art question rather than a framework pitch. The one remaining
+gate is G1 (a literature pass), which is a desk task, not a
+formalisation blocker.

docs/next-questions.adoc

@@ -200,23 +200,43 @@ This is naturally echo-shaped because it is about the *type*
 characteristic status depends on the gate-2 bar.
 
 Status::
-Open. Forwarded by gate-3's `gate-3-handoff.adoc` for gate-2
-evaluation.
-
-Attack path::
+Closed (formalisation), gate-2 audit recorded. The received-`y`
+general theorem is `EchoTruncation.echo-not-prop`, re-exported under
+the gate name as `characteristic.NonTruncatable.Q2-1`. The
+genuinely open end — the *non-injectivity* form, which does not
+receive `y` but constructs it from a bare non-injectivity witness
+on `f` — is closed as
+`characteristic.NonTruncatable.non-injective⇒echo-not-prop`. Both
+compile under `--safe --without-K` and are in the CI characteristic
+lane via `characteristic/All.agda`.
+
+Attack path (done)::
 . State and prove the general theorem in
-  `proofs/agda/characteristic/NonTruncatable.agda`.
+  `proofs/agda/characteristic/NonTruncatable.agda`. *Done.*
 . Audit it against the gate-2 falsifier ("naturally echo-shaped,
-  not reducible to generic Σ/fiber lemmas").
+  not reducible to generic Σ/fiber lemmas"). *Done — see the
+  module header.*
 . If it survives, add to `roadmap-gates.adoc` Gate 2 nominee table
   as a candidate N6 (or N5 if `choreo-grade-commute` is not
-  separately adopted).
-
-Internal falsifier::
-If the general theorem follows by routine unfolding from a stdlib
-lemma about Σ-types having distinct elements, it is not echo-
-specific; it is just "a Σ with two distinct inhabitants is not
-propositional".
+  separately adopted). *Integrator decision: see audit verdict.*
+
+Gate-2 audit verdict::
+The *received-`y`* form (`Q2-1`) is PARTIALLY REDUCIBLE: its proof
+is `ne (cong proj₁ (prop e₁ e₂))`, a generic Σ fact ("a Σ with two
+elements differing in the first component is not `isProp`"). It is
+echo-shaped only in *statement*. Same demotion as
+`VisibleConstraintAudit` applied to `visible-constraint`: kept for
+exposition, **not** nominated. The *constructed-`y`* form
+(`non-injective⇒echo-not-prop`) is strictly more than a Σ fact —
+it shows ordinary non-injectivity (no Σ in the hypothesis) *forces*
+a non-propositional echo fibre. This is the form worth forwarding
+to gate-2; the integrator decision on adoption as a nominee is left
+explicit and not pre-decided here.
+
+Internal falsifier (outcome)::
+The received-`y` form *does* follow by routine unfolding from the
+generic Σ fact, so it is correctly *not* claimed as echo-specific.
+The constructed-`y` form is not reached by that falsifier.
 
 === Q2.2 — Refinement injectivity as characteristic
 

proofs/agda/characteristic/All.agda

@@ -25,6 +25,7 @@ import characteristic.ChoreoInjective
 import characteristic.IntegrationAudit
 import characteristic.InteractionTest
 import characteristic.ModeGraded
+import characteristic.NonTruncatable
 import characteristic.RecipeNonTriviality
 import characteristic.RecipeSpec
 import characteristic.RecipeTheorem

proofs/agda/characteristic/NonTruncatable.agda

@@ -0,0 +1,97 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Q2.1 — Generalisation of `echo-not-prop`.
+--
+-- This module is the artefact named in the Q2.1 attack path
+-- (`docs/next-questions.adoc` §Q2.1): "State and prove the general
+-- theorem in `proofs/agda/characteristic/NonTruncatable.agda`".
+--
+-- Gate-3 supplies three n=2 special cases that an `Echo` type is not
+-- a mere proposition (`EchoExamples` / `EchoTropical` /
+-- `EchoCharacteristic`, recovered as corollaries in
+-- `EchoTruncation`). Q2.1 asks for the general statement:
+--
+--   For f : A → B and y : B, if there exist x₁ ≢ x₂ with
+--   f x₁ ≡ y and f x₂ ≡ y, then ¬ isProp (Echo f y).
+--
+-- That statement is already proved generically as
+-- `EchoTruncation.echo-not-prop`. This module (1) re-exports it under
+-- the Q2.1 name so the gate paperwork points at a single audited
+-- artefact, and (2) closes the genuinely open end of Q2.1: the
+-- *non-injectivity* form, which does not receive the witnessing
+-- value `y` but **constructs** it from a bare non-injectivity
+-- witness on `f`. The received-`y` form needs the caller to have
+-- already factored their non-injectivity through a common output;
+-- the constructed-`y` form is the statement an external reader
+-- means by "non-injective ⇒ non-truncatable".
+--
+----------------------------------------------------------------------
+-- Gate-2 falsifier audit (honest).
+--
+-- Gate-2 falsifier: "naturally echo-shaped, not reducible to generic
+-- Σ/fiber lemmas". Verdict for the *received-y* form (`Q2-1`):
+-- PARTIALLY REDUCIBLE. Its proof is `ne (cong proj₁ (prop e₁ e₂))`,
+-- which is the generic fact "a Σ-type with two elements differing in
+-- the first component is not an `isProp`" — true of any Σ, not
+-- specific to `Echo`. The only echo-specific content is in the
+-- *statement*: the two Σ-elements are constrained to be preimages of
+-- a *common* `y`. So `Q2-1` is echo-shaped in statement but its
+-- proof factors through `Σ`. Under the strict gate-2 bar this is the
+-- same demotion `VisibleConstraintAudit` applied to
+-- `visible-constraint`: kept for expository value, **not** nominated
+-- as a characteristic theorem on its own.
+--
+-- The *constructed-y* form (`non-injective⇒echo-not-prop`) is
+-- strictly more than a Σ fact: it asserts that ordinary
+-- non-injectivity of a function (`f x₁ ≡ f x₂`, `x₁ ≢ x₂`) — a
+-- property with no Σ in sight — *forces* the existence of a
+-- non-propositional echo fibre. The Σ-genericity argument does not
+-- reach it, because the bad `y` is produced, not assumed. This is
+-- the form worth forwarding to gate-2 as a nominee; the audit
+-- conclusion is recorded for the integrator, not pre-decided here.
+----------------------------------------------------------------------
+
+module characteristic.NonTruncatable where
+
+open import Echo using (Echo)
+open import EchoTruncation using (isProp; echo-not-prop)
+
+open import Level using (Level)
+open import Data.Product.Base using (Σ; _,_)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym)
+open import Relation.Nullary using (¬_)
+
+private
+  variable
+    ℓa ℓb : Level
+    A : Set ℓa
+    B : Set ℓb
+
+----------------------------------------------------------------------
+-- Q2.1, received-y form.  Re-export of the once-and-for-all generic
+-- lemma, under the gate name, so `next-questions.adoc` §Q2.1 and
+-- `roadmap-gates.adoc` Gate 2 point at one audited artefact.
+
+Q2-1 :
+  (f : A → B) {y : B}
+  (x₁ x₂ : A) (p₁ : f x₁ ≡ y) (p₂ : f x₂ ≡ y) →
+  x₁ ≢ x₂ →
+  ¬ isProp (Echo f y)
+Q2-1 = echo-not-prop
+
+----------------------------------------------------------------------
+-- Q2.1, constructed-y form (the genuinely open end, now closed).
+--
+-- From a bare non-injectivity witness on `f` — two distinct inputs
+-- with equal output — *produce* an output value whose echo fibre is
+-- not a mere proposition.  The witnessing `y` is `f x₁`; `x₁` lands
+-- in its own fibre by `refl`, and `x₂` lands in the same fibre by
+-- `sym eq`.  No common output is assumed: it is constructed.
+
+non-injective⇒echo-not-prop :
+  (f : A → B) (x₁ x₂ : A) →
+  f x₁ ≡ f x₂ →
+  x₁ ≢ x₂ →
+  Σ B (λ y → ¬ isProp (Echo f y))
+non-injective⇒echo-not-prop f x₁ x₂ eq ne =
+  f x₁ , Q2-1 f x₁ x₂ refl (sym eq) ne