rjwalters · rjwalters · May 8, 2026
diff --git a/proofs/Proofs/CantorDiagonalizationOQ04OQ01.lean b/proofs/Proofs/CantorDiagonalizationOQ04OQ01.lean
@@ -34,6 +34,9 @@ the original theorem exactly.
 5. `cannot_code_endomorphisms_bool_setoid` — Bool cannot code its endomorphisms
 6. `cantor_setoid_no_surjection` — Cantor diagonal in setoid setting
 7. `cannot_code_endomorphisms_nat_parity` — ℕ cannot code endomorphisms up to parity
+8. `trivial_setoid_codes_endomorphisms` — every inhabited Y codes under the trivial (one-class) setoid
+9. `bool_trivial_setoid_codes_endomorphisms` — Bool codes under trivial setoid (contrast with #5)
+10. `coding_descends_to_coarser` — coding under a finer setoid descends to any coarser setoid
 
 ## Proof Technique
 Diagonal construction: g(y) = f(decode(y)(y)).
@@ -163,4 +166,56 @@ theorem cannot_code_endomorphisms_nat_parity :
     CodesEndomorphismsSetoid ℕ paritySetoidN → False :=
   no_coding_setoid_if_fixpoint_free paritySetoidN (fun n : ℕ => n + 1) succ_no_parity_fixpoint
 
+-- ============================================================
+-- Part VIII: Trivial Setoid — Coding Always Possible
+-- ============================================================
+
+/-- The trivial setoid: every pair is equivalent. Collapses Y to a single class. -/
+def trivialSetoid (Y : Type*) : Setoid Y where
+  r := fun _ _ => True
+  iseqv := ⟨fun _ => trivial, fun _ => trivial, fun _ _ => trivial⟩
+
+/-- **Setoid-choice sensitivity**: under the trivial (one-class) setoid, every
+    inhabited type codes its endomorphisms vacuously. The retraction holds because
+    `s.r a b = True` for all `a, b`. Together with `cannot_code_endomorphisms_bool_setoid`
+    this shows that coding-feasibility depends genuinely on the setoid structure,
+    not just on the underlying type. -/
+theorem trivial_setoid_codes_endomorphisms (Y : Type*) [Inhabited Y] :
+    CodesEndomorphismsSetoid Y (trivialSetoid Y) where
+  encode := fun _ => default
+  decode := fun _ => id
+  retract := fun _ _ => trivial
+
+/-- Bool DOES code its endomorphisms under the trivial setoid, even though it
+    fails under the discrete setoid (cf. `cannot_code_endomorphisms_bool_setoid`).
+    Witnesses that the impossibility result for Bool is setoid-specific. -/
+theorem bool_trivial_setoid_codes_endomorphisms :
+    CodesEndomorphismsSetoid Bool (trivialSetoid Bool) :=
+  trivial_setoid_codes_endomorphisms Bool
+
+-- ============================================================
+-- Part IX: Refinement Lemma — Coding Descends to Coarser Setoids
+-- ============================================================
+
+/-- A setoid `s` **refines** `t` when `s`-equivalence implies `t`-equivalence
+    (equivalently, `t` is coarser than `s`). The discrete setoid refines every
+    setoid; every setoid refines the trivial setoid. -/
+def IsRefinement {Y : Type*} (s t : Setoid Y) : Prop :=
+  ∀ a b : Y, s.r a b → t.r a b
+
+/-- **Refinement-descent**: if `Y` codes its endomorphisms under a finer setoid `s`,
+    the same encode/decode also code under any coarser setoid `t`. The retraction
+    transports along refinement because `t`-equivalence is weaker than `s`-equivalence. -/
+theorem coding_descends_to_coarser {Y : Type*} {s t : Setoid Y}
+    (hst : IsRefinement s t) (c : CodesEndomorphismsSetoid Y s) :
+    CodesEndomorphismsSetoid Y t where
+  encode := c.encode
+  decode := c.decode
+  retract := fun g y => hst _ _ (c.retract g y)
+
+/-- Every setoid is a refinement of the trivial setoid (vacuously: the trivial relation
+    is `True`). This is the canonical "top" of the refinement order on `Setoid Y`. -/
+theorem refines_trivial {Y : Type*} (s : Setoid Y) : IsRefinement s (trivialSetoid Y) :=
+  fun _ _ _ => trivial
+
 end CantorDiagonalizationOQ04OQ01
diff --git a/research/problems/cantor-diagonalization-oq-04-oq-01/knowledge.md b/research/problems/cantor-diagonalization-oq-04-oq-01/knowledge.md
@@ -6,6 +6,64 @@ Generalize Lawvere's retraction FPT from exact Type equality to Setoid equivalen
 **Parent**: CantorDiagonalizationOQ04 (Lawvere FPT, Type-level retraction version)
 **OQ**: "Can the retraction version be formalized beyond the Type category?"
 
+## Session 2026-05-08 (Session 2, researcher-3) — ACT (refinement structure)
+
+**Mode**: REVISIT (RICH, score 24)
+**Phase change**: COMPLETED → ACT (re-opened with new structural content)
+**Outcome**: Added the *success* side and the *refinement* structure to round out the spectrum of coding-feasibility on `Setoid Y`.
+
+### What I Did
+
+Added Parts VIII and IX to `proofs/Proofs/CantorDiagonalizationOQ04OQ01.lean` (166 → 221 lines).
+
+**Part VIII — Trivial setoid (success side):**
+- `trivialSetoid Y : Setoid Y` — collapses Y to one class (`r := fun _ _ => True`).
+- `trivial_setoid_codes_endomorphisms` — every inhabited Y vacuously codes its endomorphisms under `trivialSetoid`. Witness: `encode = const default`, `decode = const id`, retract is `trivial`.
+- `bool_trivial_setoid_codes_endomorphisms` — explicit Bool corollary, contrasting with the discrete-setoid impossibility (`cannot_code_endomorphisms_bool_setoid`). Demonstrates that *coding-feasibility is genuinely setoid-dependent*, not a fixed property of the underlying type.
+
+**Part IX — Refinement structure:**
+- `IsRefinement s t : Prop` — `s.r a b → t.r a b` for all a, b (s is finer; t is coarser).
+- `coding_descends_to_coarser` — `IsRefinement s t → CodesEndomorphismsSetoid Y s → CodesEndomorphismsSetoid Y t`. Same encode/decode work; the retract weakens because `t`-equivalence is implied by `s`-equivalence.
+- `refines_trivial` — every setoid refines the trivial setoid. Places the trivial setoid at the canonical *top* of the refinement order on `Setoid Y`.
+
+### Key Findings (S2)
+
+1. **Setoid choice matters structurally**: Bool fails coding under discrete setoid (S1), but succeeds under trivial setoid (S2). Same type, different setoid, different coding behavior.
+2. **Coding-existence is downward-closed**: in the refinement lattice on `Setoid Y`, the set `{s : CodesEndomorphismsSetoid Y s is inhabited}` is closed under going to coarser setoids.
+3. **The discrete and trivial setoids bracket the spectrum**: discrete = strongest condition (often fails), trivial = weakest condition (always succeeds). The interesting structural information lives in setoids strictly between them (parity, congruence classes, isomorphism-up-to-coherence).
+
+### Files Modified
+
+- `proofs/Proofs/CantorDiagonalizationOQ04OQ01.lean` (166 → 221 lines): +2 defs, +4 theorems, 0 axioms unchanged, 0 sorries unchanged.
+- `src/data/proofs/cantor-diagonalization-oq-04-oq-01/meta.json`: lineCount 166→221, theoremCount 8→12, definitionCount 3→5; +4 originalContributions entries; +2 sections for Parts VIII/IX; conclusion summary updated.
+- `src/data/research/problems/cantor-diagonalization-oq-04-oq-01.json`: phase COMPLETED→ACT, status completed→active, iteration 1→2; +6 builtItems, +4 insights, +3 nextSteps; lastUpdate 2026-05-07→2026-05-08; leanFiles entry for OQ04OQ01 updated to 221/12/5.
+- `research/problems/cantor-diagonalization-oq-04-oq-01/knowledge.md`: this file.
+
+### Build Status
+
+**Pending.** The worktree's `proofs/.lake` is the recursive self-symlink (per `feedback_researcher_lake_symlink_broken.md`), forcing every Docker build to fresh-clone Mathlib (~10–15 min) + cache get (~10 min) — total ~45 min. Following the established convention from PRs #16936 (cantor-OQ-01-OQ-01-OQ-02-OQ-01 S5), #17008 (ehrhart-cube-proven-oq-02 S4), this PR opens as **draft**.
+
+The new theorems use only basic Mathlib primitives already exercised in this file:
+- `Setoid` constructor with `Equivalence` proof from `⟨fun _ => trivial, fun _ => trivial, fun _ _ => trivial⟩` (Part VIII)
+- `default` (from `Inhabited`), `id`, `trivial` (Part VIII)
+- Anonymous constructor of `CodesEndomorphismsSetoid`-records using fields (Parts VIII, IX)
+
+Risk of build failure is low; review of the proof bodies should be straightforward by inspection.
+
+### Honesty Assessment
+
+- **What this is**: a structural rounding-out of S1, not a deep new result. The four new theorems are 1-2 line proofs each, and the trivial-setoid case is genuinely vacuous (the retract holds because `True` is always provable). The refinement-descent lemma is also nearly trivial (function composition).
+- **What this is NOT**: a characterization theorem. OQ-04-OQ-01-OQ-02 ("which setoids admit coding?") remains open — S2 only provides the structural backbone (refinement lattice + downward-closure) for a future characterization.
+- **What this enables**: future sessions can target the converse of `coding_descends_to_coarser` (when does coding lift to finer setoids?) and the cardinality classification (is `|Y/≈| ≤ 1` the right boundary?). The refinement structure is the right organizing principle.
+
+### Next Concrete Steps
+
+1. **S3+ (OQ-04-OQ-01-OQ-02 attack)**: explore the boundary of admissible setoids on a concrete `Y` (try `Bool` with all 5 setoids; classify exactly which admit coding).
+2. **S3+ (ℕ spectrum)**: extend `succ_no_parity_fixpoint` to `succ_no_modk_fixpoint` for arbitrary `k ≥ 2`. Find the *finest* setoid on ℕ admitting coding (likely the cofinite-quotient or a similar limit).
+3. **Phase-3 (CCC lift)**: target the original OQ-04-OQ-01-OQ-01 (Mathlib `CartesianClosed` typeclass formalization). Setoid layer is the natural intermediate; the next step is replacing `Setoid` with an arbitrary equality-up-to-coherent-equivalence in a CCC.
+
+---
+
 ## Session 2026-05-07 (Session 1) — SOLVED
 
 **Mode**: FRESH