# The Subsumption Sprint — Pareto core + fresh-chat handoff

**Goal of the sprint:** complete the full subsumption of **Lean 4 + Mathlib into S**, bring
`refound-s` to **parity with the old Rust interop**, then **drop Lean** and build purely from S
natively. Everything below serves that and only that.

> **THE TWO ROUTES ARE ONE SEED (2026-06-15).** The universal translator (`UniversalTranslation`:
> lift a surface → the meaning floor → express, the formal tier, lossless-EXACT) and the model seal
> (`sang model seal`: weights → the codebook floor → `qrun`, lossy-BOUNDED) are the SAME `x = B/U`
> collapse — **asserted, not proved**: the claim was written 2026-06-15 (`e2e1f5fb`) against
> `Substrate/Cic/SeedCollapse.lean` `translator_and_seal_one_seed`, and that module went with the <!-- CITATION-EXEMPT: deleted at b70fb1b1, kept as the record -->
> Cic kernel at `b70fb1b1` (2026-06-16). No declaration in this corpus states it. They differ
> only in lossless-exact vs lossy-bounded, on both faces of the Seed: the meaning/key (`termSeed`
> the def-eq floor vs `weightSeed` the codebook cell) and the section/storage (`Seed.idFloor` vs
> `Seed.quantFloor`, round-trip free). *Translate a surface = seal a model = subsume a def* is one
> operation; the supremacy face (the seal) and the Mathlib-subsumption face (the translator) are one
> primitive. The open frontiers are the **learned tier** (natural language, the floor learned not
> derived, L3) and the **scale-out** of both (the 8B+ seal, Mathlib throughput).

---

## The Pareto cut (grounded in import in-degree + the goal)

The corpus is **294 modules**. They form two largely-separable subtrees:

- **CORE — the subsumption machinery (~80 modules).** The ~20% that *achieves the goal*. This is
  what the sprint works on. (The machinery import-closure is 95 modules; ~13 of those are the
  physics the apex `Sanguine.lean`/`SanguineOS.lean` headline pulls in for presentation — strip
  those and the true machinery is ~80.)
- **TAIL — the materialized content (~210 modules).** Magnificent, proven *results* — but they are
  **content to be subsumed by the machinery, not the machinery itself.** Off the critical path for
  this sprint. Keep them (the physics is the headline reality), but **do not develop or get
  distracted by them** here; they are the corpus the finished machinery lifts.

### CORE — keep & complete (the working set)

1. **Term / bulk / K=4 evaluator (the foundation):** `Ski.PolyIotaTermAlgebra`,
   `Ski.IotaTermAlgebra`, `Algebra.BulkTower`, `Algebra.BulkContains`, `Algebra.BulkInevitability`,
   `Algebra.FreeBulkAlgebra`, `Algebra.BulkOfBulks`, `Ski.KernelRuntime`, `Ski.EvaluatorReduceStep`,
   `Ski.EvaluatorDeepReduce`, `Ski.HardwareProjectionDispatch`, `Ski.IotaChainMarkers`,
   `Ski.Confluence`, `Ski.DataReduces`/`WordReduces`/`TranslateReduces`/`SyscallReduces`,
   `Ski.RuntimeCorrespondence`, `Algebra.BitlistChurchEquivalence`, `Algebra.AbstractBulkDifferential`.
2. **Equation / trinity / encoder / translate / arithmetic:** `Algebra.UniversalEquation`,
   `Algebra.BeingMonism`, `Algebra.NonBeing`, `Algebra.TrinityOperations`, `Algebra.UniverseSyntax`,
   `Algebra.UniverseSyntaxSerialisation`, `Algebra.UniversalTranslation`, `Algebra.UniversalAdapter`,
   `Algebra.UniversalApplicativeLift`, `Algebra.ModalityIsomorphism`, `Algebra.DiscreteApplicative`,
   `Algebra.DiscreteArithmetic`, `Algebra.DivisionAlgebraSubstrate`.
3. **Recursion as the one fold (the generalization — the heart):** `Ski.RecursorCollapse`,
   `Ski.LeanRecLift`, `Ski.BrecOnLift`, `Ski.ListRecLift`, `Ski.WordChurchBridge`, `Ski.ContentEnv`,
   `Ski.CombRealization`, `Ski.CompositionalLift`, `Ski.ConversionOpsAreIdentity`,
   `StationaryPhase.SpinorLoop`, `StationaryPhase.AffineLoopCollapse`, `Ski.ListOpsClosedForm`,
   `StationaryPhase.RecursionFloor`. **`deriveFold` is GENERIC and landed** (the masks read off the
   declaration; indexed + recursive + nested all land — commits 2026-06-08).
4. **The CIC kernel (all of it):** `Substrate.Cic.*` — `CExpr`, `Level`, `Typing`, `Conv`,
   `ConvCollapse`, `Inductive`, `Env`, `EnvAsData`, `Kernel`, `KernelStruct`, `KernelRec`,
   `ProofIrrel`, `CicReflect`, `CicValidate`, `CheckReflected`, `CheckHarness`, `CheckFidelity`,
   `Serialize`, `TermFloorComplete`, `FloorDefeq`, `SangCollapseDefEq`, `SeedCollapse`.
5. **Lean lift + sovereignty + check-is-collapse:** `Ski.LeanSubsumption`, `Ski.LeanReflect`,
   `Ski.KernelSovereignty`, `LogicalSovereignty`, `Ski.CollapseVerification`,
   `Closures.Applied.DefeqIsOneCollapse`, `Substrate.Collapse`, `Substrate.Seed`.
6. **Universe-morphism infra (the subsume relation):** `Algebra.Subsumption`,
   `Algebra.CrossUniverseNavigation`, `Algebra.CrossLevelNavigation`, `Algebra.Origin`.
7. **Apex + runtime + tooling:** `Sanguine`, `SanguineOS`, `LeanFidelity`, `Prover`,
   `Runtime.{NativeRuntime,SangCheck,SangCorpus,SangAdapt,Serialise,Certify,MetalEmit,MetalNative}`,
   and the **one `sang` binary** (`adapt` = the universal lift, `dump`/`check`/`fidelity` = the
   lift/check loop, `emit` = native ELF). *(The old Rust `./sanguine-interop` is retired —
   deleted source, subsumed by `sang adapt`; do not use it.)*

### TAIL — set aside for this sprint (content, not machinery)

The materialized physics (`MadelungCell`→`EinsteinCurvature`→`CosmologyFriedmann`→`Stellar*`→
`Koide*`→`Gauge*`→`SectorBulk`→neutrino→`CasimirCollapse`), the dimension/cell codex (`NullCell*`,
`TwentySixDescent`, `LeechAscent`, `Octonion*`, `Sedenion`, `BottPeriod`, `DimensionLadder`,
`Cell{Field,Lattice,Conservation,Distribution}`, `HyperbolicPlane`, the spinor-physics files), all
of `Closures/Sat/*` and `Closures/Folding/*`, most of `Closures/Applied/*` (`Sha256d*`,
`BitcoinClosure`, `OblivionClosure`, `AndGateReadout`, `BicliqueArc`, `TransformerGeometry`, …), and
the navigation re-derivations (`BoostNavigation`, `WarpNavigation`, `KeplerCollapse`, `GPSClock`,
`GravityAssist`, `RocketEquation`, `BayesFilter`, `Navigation*`). **Proven, kept, off-path.** When
the machinery is complete these become test-content for `lift-lean`/`sangcheck`, not sprint work.

*(Servitor/ethics — `CapabilityAwarenessOrthogonality`, `AssistantWithoutSelfReference` — are
imported by the `SanguineOS` apex (laws 6–7); they stay with the core as the apex's gates.)*

---

## The three gates (the real distance, located by running — absorbs SUBSUMPTION_HANDOFF, 2026-06-13)

The pipeline **lift → reduce → check → store → emit-native → run-standalone** runs with **zero Lean
in the run** (`sang native`: 8/8 + 12/12 agree with Lean; `sang run`: a disk program collapses to one
integer; `sang emit p.sang -o p.elf --check` → a 1555-byte static x86-64 ELF, ran standalone,
exit = WHNF head tag, native=lean=1 PASS; `sang dump`/`check`/`all`/`fidelity` re-check the lift
natively). The lift's recursor-path map (`THE_HASHMAP_PATH` §the dual): constructor → Scott/Church
(B), recursor/function → the fold (B/U), proof → erase to `I` (NB). **Lift fidelity measured:**
`Init.Data.Nat.Basic` 20/20 computational content resolves (the other 296 are type-residue, erased);
`Init.Data.List.Basic --fuel 2000` 2581/2581 value-decls collapse over the full 6081-constant closure.
The remaining distance is three named gates:

- **Gate 1 — lift completeness (the `deriveFold` frontier).** Simple + list recursion resolve
  (2581/2581). Named-open seam: **nested / mutual recursion** (a `Tree` with `List Tree` children;
  mutual inductives) and **indexed families**, plus **leaf gaps** (un-wired functions show
  `unresolved`). Lives in `LeanFidelity.lean`, `Substrate/Ski/RecursorCollapse.lean`,
  `LeanSubsumption.lean`, `deriveFold`. Not a wall — one rule per face. *(Note: `deriveFold` is generic
  and landed for indexed + recursive + nested per CORE above; the residual is the un-wired leaves +
  mutual at scale.)*
- **Gate 2 — run/emit *speed* (the optimizing-emit gap).** A function can **lift** (resolve to `Comb`)
  yet not **run to the answer** at a given fuel/repr (`Nat.mul 2 3` collapses but `✗ at this fuel/repr`
  while `add/pred/sub` run clean); the emitted ELF is **1 byte/node** — it embeds the program and runs
  the *reducer* over it (interpreter speed), not machine code compiled to the program's logic. Same
  wall the WAF hit (0.5× nginx = the Lean-runtime tax). Finishing the lift gives CORRECT pure-S, not
  FAST pure-S — that is this gate. Lives in `Runtime/NativeRuntime.lean`, `MetalNative.lean`,
  `MetalEmit.lean`.
- **Gate 3 — self-hosting (drop Lean as the compiler).** `sang emit` produces the native ELF, but
  `sang emit` *itself* is Lean-compiled (the bootstrap that compiles the emitter once — `REFOUND_S
  §3b`). The terminus is **S emitting the S emitter**. We have the reducer ELF (the seed); the emitter
  is the remaining self-host piece. (Can precede Gate 2 — a correct-but-slow pure-S is still Lean-free.)

**The size of the cut (the Being-weight, `sang adapt`).** The lift collapses the Null (redundancy) and
lifts the Being (irreducible structure), so the cut's real weight is the Being content: `proof/Substrate`
1.79 bits/sym (75.8% folds), `proof/Runtime` 1.67 (77.3%), whole `proof/` ≤32 MB sample 1.88 (76.4%).
~76% folds; sub-MB of Being per major subtree — the corpus is dense (one idea, one place, measured), the
harder-but-smaller target. Mathlib is the open swing (`sang all Mathlib` under `lake env`; swung at
134,120 declarations).

**`sang adapt`'s three faces, measured (absorbs RESONANCE_ANALYSIS — 2026-06-13).** `sang adapt <dir>`
reads any data's resonance off its **own** geometry (no parser/whitelist, Axiom XX): it discovers the
alphabet, learns the data's own conditional statistics (the B/U accumulator over the suffix filtration),
and reads the **three faces of the Null cell** (`SangAdapt`, grounded in `NullCell.nNorm_mul` — info adds
where the norm multiplies): **B (monad)** = `log₂(alphabet)` (uniform equilibrium); **B/U (Being)** =
the irreducible structure (bits/symbol) at the deepest *reliable* context order, `/` total; **NB (Null)**
= `monad − Being`, the redundancy that folds, `/` singular. It also discovers the data's own units (a
lossless RE-PAIR grammar, round-trip verified). Full-model entropy, deepest reliable order = 3:

| codebase | alphabet | monad | **Being** (irreducible) | **Null** fold |
|---|---|---|---|---|
| nginx (C) | 127 | 6.98 | **1.31** bits/sym | 81.2% |
| caddy (Go) | 256 | 8.00 | **1.44** bits/sym | 82.0% |
| our `proof/Substrate` | 173 | 7.43 | **1.79** bits/sym | 75.8% |
| our `proof/Runtime` | 167 | 7.38 | **1.67** bits/sym | 77.3% |

Irreducible structure sits in a tight ~1.3–1.8 bits/symbol band across every codebase regardless of
language; the rest (76–82%) is redundancy that folds (source code is mostly Null). nginx is the *most*
redundant (Being 1.31) — its discovered units *are* logging macros + C boilerplate, which is why its
hot path is a 6,645-line repetitive state machine (the redundancy is the cost of the speed). Our corpus
is **denser** (1.79/1.67 — more genuine info per symbol, less to fold): the "one idea, one place"
discipline, measured. The tool found nginx's `ngx_log_error(NGX_LOG_` macro and our `═══`
dividers / `Polymorphic.` / `. -/ theorem` cadence *as units*, from raw bytes. *Honest scope: the
Being/Null entropy is robust (full-model conditional entropy at the reliable order); the RE-PAIR
grammar-fold % is sampled (first 256 KB), representative only when the sample is. The measure is native
(`NullCellCoding`/`nNorm_mul`); "this is the subsumption size" is the labeled L1 reading it supports —
the lift collapses the Null and lifts the Being, so the real cost is the ~720 KB of Being under
`proof/Substrate`'s 3.2 MB, not the byte count.*

**Recommended first reconnaissance swing:** take ONE *whole* real recursive
program (a `List.foldl` computation or a small structured Lean function), drive `lift → emit → run`, and
report **where it breaks** — Gate 1 (does it lift?) vs Gate 2 (does it run fast enough?). The break IS
the measurement (Axiom XXII).

## THE FRESH-CHAT PROMPT (paste this verbatim into a new chat)

> Read `AGENTS.md` and `theory/SUBSUMPTION_SPRINT.md` first, then `proof/INDEX.md` "two kernels"
> section. We are completing the subsumption of **Lean 4 + Mathlib into S**, bringing `refound-s`
> to **parity with the old Rust interop**, then **dropping Lean** to build natively from S.
>
> **THE ONE MOVE — the only method, no exceptions.** Everything is: **lift → run/check by collapse
> → the fold read off the signature.** A program is a `Term`; running, checking, translating, and
> lifting are all `state` under an applicative (`SanguineOS` Laws 1–3, 9: *checking is collapse, and
> the subsumption of Lean follows*). **There are no edge cases.** Every Lean declaration is one of
> three faces — constructor → Scott/Church, recursor → the **generic** `foldExpr`/`recExprI` read
> off the signature *as data*, proof → `I` (`THE_HASHMAP_PATH.md`). If you catch yourself writing
> per-type / per-recursor / per-case code, a search, a brute-force `2^k`, or a hedge — **STOP**.
> That is the zoo, the exact thing this framework deletes. Generalize; never grind a special case.
>
> **THE TOOL — run it, never hunt or reimplement.** The ONE universal lift is **`sang adapt
> <file|dir>`** (`fromTerm ∘ universalLift`, proven format-agnostic — `OneLift`, `universal_adapter`):
> a file → its fingerprint; **a whole repository → walk the tree, lift every file through the one
> encoder into one shared resonance histogram, report the corpus mass-cancellation + dominant
> faces** read off the data's own conditional entropy — the three faces of the Null cell (`NullCell.lean`), no whitelist (alien-robust: noise→0.6% fold, compressed PNG→1%, Lean source→88%; our `proof/`→1.79 bits/symbol irreducible vs goose 1.97).
> path, not two. The Lean lift is `sang dump <Module>`; the lift/check loop is `sang
> check`/`fidelity`/`all`; native ELF is `sang emit`. **⚠ Do not use the old Rust
> `./sanguine-interop` CLI** (`translate`/`lift-lean`/`analyze`/`project`) — its source is deleted
> and `translate` is the per-format parser Axiom XX forbids, subsumed by `sang adapt`. Producing
> S/Iota from anything is a command (THE FIRST MOVE), never a research blocker. **Touch the system
> — `lake build` + run `sang` — before any claim.**
>
> **STANDING (verify with `lake build`/`fidelity`, do not re-derive).** The CIC kernel is up:
> `checkKR` self-checks every arbitrary `Function.*` Mathlib declaration (`CicValidate`, 60/60);
> `EnvAsData` runs the kernel **with Lean out of the check loop**; the generic `foldExpr`/recursor
> collapse landed (indexed + recursive + nested); `LeanFidelity` is ~93%; the one universal lift
> `sang adapt` (file or whole-repo) and the `lift-lean`/`analyze` diagnostics are live.
>
> **THE GAP TO PARITY + DROP-LEAN (the actual sprint).** (1) Native `sangcheck`/`sangcorpus` over
> **all of Mathlib** — the labeled-open boundary is serialization + scale, not a missing mechanism.
> (2) The `.s` → native-ELF pipeline at parity with the Rust `project`/self-hosting compiler. (3)
> Then **Lean fully out of the loop**: `EnvAsData` + native `sangcheck` is S verifying S's content
> against S's own floor (`CollapseVerification.defeqCheck_sound`, Law 9), no external kernel.
>
> **THE WORKING SET** is the CORE in `theory/SUBSUMPTION_SPRINT.md` (~80 machinery modules). **Do
> NOT work the TAIL** (the materialized physics, the cell/dimension codex, the SAT/folding/applied
> closures, the navigation files) — it is proven content the finished machinery will lift, off this
> sprint's critical path.
>
> **DISCIPLINE (hard-won — do not repeat the last session's failures).** No search/brute-force —
> `O(1)` means stationary-phase collapse (Axiom V). No reflexive "honest-scope" hedge trailers
> (killed 2026-06-04 — name the next task instead). No courting auditors/reception (Axiom XIX —
> reception is the world's job). **No smuggling the hard part into a hypothesis** — a theorem with
> `(h : Function.Injective C)` where `C` is the difficulty is a `sorry` wearing the word `theorem`;
> `#print axioms` clean is worthless if the payload is above the turnstile. Report by pointing at
> the artifact (the build, the number, the theorem); name a measured win as a win, in a line, then
> go to the next task — no funeral, no extrapolation. Build **with** the corpus and Lucas's results;
> never grade them.
>
> **FIRST MOVES.** (1) `cd proof && lake build`; run `sang` (no args) to see the command map.
> (2) `sang dump` a small Mathlib module and `sang check` it to measure current native coverage
> against the 60/60 baseline. (3) Pick the next slice of Mathlib that the native checker doesn't yet
> cover, and close the serialization/scale gap — one generalized lift, not per-declaration code.
> Diagnose, prove, proceed.

## Labels (Axiom XIII)

This is a sprint plan, so most of it is `Open:` by construction. What is not open is the working
set: five of the modules it lists were deleted after it was written.

* **Retired:** §4's "the CIC kernel (all of it)". `Substrate/Cic/` (22 files) and six dependents —
  `DefeqIsOneCollapse` (§5), `Prover`, `SangCheck`, `SangCorpus` (§7) among them — were deleted in
  `b70fb1b1`, "the floor-based universal translator is the kernel now". `sang check` and `sang all`
  survive as routes into `SangDump.entry` (`--check` / `--all`). What carried the tier forward is
  `Ski.CollapseVerification` with `Substrate.Collapse` and `Substrate.Seed`.
* **Retired:** §3's `LeanRecLift`, `BrecOnLift`, `ListRecLift` and §5's `LeanReflect`, deleted in
  `6e44dfa` ("Subsume all of Mathlib by the def-eq coordinate; drop the reflect lane"). None is
  planned-but-unwritten and none is misspelled: a working set that names five deleted modules reads
  as work outstanding on code that is gone.
* **Retired:** Gate 1's named-open **nested** seam, at the algebra layer.
  `TreeRecursorCollapse.tree_recursor_converges` proves the branching (W-type) recursor collapses
  unconditionally with an explicit step count (`TreeRecursorCollapse.treeSteps`), and
  `TreeRecursorCollapse.eval_within` closes the three-constructor `Expr` the same way — the
  unconditional law the deleted `ListRecLift` had stated only conditionally. The seam that remains
  is the resolver, not the algebra.
* **Open:** §3's "**`deriveFold` is GENERIC and landed** (indexed + recursive +
  nested all land)" and CORE's note repeating it. `LeanFidelity.lean:10` states the opposite —
  "where a shape is not yet built (nested recursion, indexed recursive families) the resolver
  defers to the recursion tier" — and that file's own warrant reads its four witnesses
  (`LeanFidelity.foldExpr_computes_nat_pred`, `foldExpr_computes_list_length`,
  `foldExpr_drops_index`, `nested_fold_composes`) at their width: "they are not a soundness theorem
  about `deriveFold`, `deriveRec` or `resolve` at any shape not listed."
* **Open:** the header's "THE TWO ROUTES ARE ONE SEED", written against <!-- CITATION-EXEMPT: deleted at b70fb1b1, kept as the record -->
  `Substrate/Cic/SeedCollapse.lean` `translator_and_seal_one_seed`. That module went with the Cic <!-- CITATION-EXEMPT: deleted at b70fb1b1, kept as the record -->
  kernel in `b70fb1b1` and the theorem is in no declaration in this corpus — the header now says so
  in place;
  `Substrate/Algebra/QuantumField/ObserverState.lean:96` records the same dangling citation and its
  history. The two floors it contrasts do stand: `Sanguine.Seed.idFloor`
  (`Substrate/SeedCore.lean:151`) and `Sanguine.Seed.quantFloor` (`Substrate/Seed.lean:81`), with
  `SeedCore.loadR_saveR` the round-trip. What is unproved is that they are one operation.
* **Open:** that a §1–§7 module *path* locates its module. 24 of the names spell
  `Algebra.X` for a module now under a subdirectory — `Bulk/` (10, including `UniversalEquation`),
  `Translation/` (6), `Trinity/` (4), `Navigation/` (2), `DivisionAlgebras/` (1), and
  `NullCell/Origin`. The modules ride; the paths are stale, the same defect `CORE.md` records of
  its own §1.
* **Open:** every number in "The three gates" and "the size of the cut" — 8/8,
  12/12, the 1555-byte ELF, 2581/2581 over the 6081-constant closure, 20/20, 1.79 / 1.67 / 1.88
  bits/sym with the four-row entropy table, 134,120 declarations, and the 47.28%-era corpus size
  of "294 modules" against 604 today. Each is a `sang` run; no script in the tree reproduces one.
  Same standing as `CORE.md §2`'s five.
* **Open:** Gate 2 and Gate 3. Gate 2 closes when the emitter compiles the program's logic instead
  of embedding it at 1 byte/node for the reducer to walk; Gate 3 when `sang emit` emits itself.
  Neither is a proposition in the corpus — "drop Lean" is a build state a bootstrap measures.
* **Open:** the sprint's own goal, the full subsumption of Lean 4 + Mathlib into S. What would
  close it is a native check over Mathlib's whole declaration set at the floor;
  `CollapseVerification.defeqCheck_sound` is the soundness half already standing, and the
  134,120-declaration swing is a run, not that statement.