# KERNEL_BOUNDARY.md — What topolei can achieve in unmodified Lean 4, and what needs kernel work *Stage 4 / post-Phase B artifact, 2026-04-24. The precise boundary between what a deep cubical-HoTT embedding gives us within Lean's current kernel, and what would require a kernel-level intervention. This document is the scope contract: if a feature is below the boundary, topolei can deliver it as a library; if above, it requires upstream Lean work and therefore lies outside topolei's scope.* --- ## 0. TL;DR - **Achievable now (the ceiling in unmodified Lean 4):** a full *embedded* cubical-transport HoTT with kernel-speed reductions (via FFI Rust). Univalence, Glue types, Σ/Π/Path, composition, transport, and a partial bridge to `Eq` on discrete types. - **Requires kernel work (the floor of the restricted region):** making Lean's *native* `Eq` cubical, HITs in the native inductive framework, universe-level univalence for `Type`, and any definitional (not just propositional) computation of cubical axioms. - **The two regions are disjoint.** Nothing topolei does can cross this boundary without forking Lean. Nothing in the restricted region is required for the cells-spec vision. --- ## 1. The fundamental obstruction Lean 4's kernel has three design choices that, together, force UIP (Uniqueness of Identity Proofs): 1. `propext` — propositional extensionality. `(P ↔ Q) → P = Q` for propositions. 2. `Quot.sound` — quotient soundness. Relation-equal elements become equal after quotienting. 3. Proof irrelevance in `Prop` — all inhabitants of `P : Prop` are definitionally equal. By a classical argument (Hofmann-Streicher-style), `propext` + `Quot.sound` imply that Lean's `Eq` on any type is a proposition: `∀ x y : α, ∀ h₁ h₂ : x = y, h₁ = h₂` — i.e. UIP. **Univalence contradicts UIP.** If `ua : A ≃ B → A = B` in Lean's `Eq` world, then applying UIP to `ua e` vs `ua e'` for two genuinely distinct equivalences would collapse them, which collapses the equivalences themselves. Therefore: Lean's native `Eq` cannot be cubical without rejecting at least one of `propext` / `Quot.sound` / `Prop`-irrelevance. Rejecting any of these is a fundamental change to the kernel — it's not a matter of adding features but of removing guaranteed properties. This obstruction is what makes HoTT-in-Lean necessarily a *deep embedding* (as in topolei, cubical-Agda's approach) rather than a native feature (as in Cubical Agda or cubical tt proper). --- ## 2. Achievable in unmodified Lean 4 (topolei's delivery region) Everything below can be done — and most is already done — using nothing but Lean's existing primitives plus FFI. ### 2.1 Deep-embedded cubical calculus - `CType` / `CTerm` / `CVal` / `CNeu` as mutual inductive Lean declarations. **Done** (Cubical/Syntax.lean, Value.lean). - Face lattice (`FaceFormula`), de Morgan interval (`DimExpr`), substitution, dim-absent analysis. **Done.** - Typing judgment `HasType : Ctx → CTerm → CType → Prop`. **Done.** ### 2.2 Computational content via FFI - Rust implementation of the evaluator, linked via `@[extern]` + `@[implemented_by]`. **Done** (Phase A+B). At runtime, any call to `eval` routes through Rust at native speed; kernel-level proof reasoning goes through axioms (unchanged). - The FFI boundary is trust-based: Lean's kernel does not verify that the Rust symbol matches the corresponding axiom. We pay for this with audit discipline (FFI_COMPLETENESS.md). ### 2.3 Reductions as axioms + NbE theorems - Every CCHM reduction rule stated as a Lean axiom in Eval.lean / Transport.lean / Readback.lean / Glue.lean / CompLaws.lean. - Kernel-level proofs use these axioms via `rw` / `simp` / explicit rewriting. - NbE theorems promote step-level claims from axioms to theorems (Stream B #2b/c/d, Stage 2.3). ### 2.4 Univalence as a *theorem*, not an axiom - `transp_ua` in Soundness.lean is a proved theorem, not posited. Exhibits the forward map of an equivalence as the computational content of Glue transport. **Done.** ### 2.5 Σ, Π, Path, Glue as type-formers - All four have `CType` constructors, eval arms, readback arms, and typing rules. **Done** (Stage 1.2 for Σ). ### 2.6 Partial bridges to Lean's `Eq` - **Always-available direction:** `Eq a b → Path (embed α) (embed a) (embed b)` (Bridge 1 in the cubical-to-eq companion). Forgets UIP information — proof. - **Discrete-type direction:** `Path (embed α) (embed a) (embed b) → a = b` when `[DecidableEq α]`. Proves by decidable-equality case analysis. - **Prop-level bijection:** `P : Prop` → paths and `Eq` coincide trivially via proof irrelevance. These bridges let users transport discrete-math lemmas (Nat, Bool, decidable structures, Mathlib-style hypotheses) into cubical proofs and vice versa. An `Eq ↔ Path` bridge module is planned (not yet written). A different cubical bridge — `Topolei/Cubical/Trace.lean` in the sibling `topolei` repo — already exists, but it lifts CTerms into the polymorphic `Trace` for provenance, not for `Eq` interop. ### 2.7 Higher cells via Zigzag Lean port - `Cell/Higher.lean` (2-cells / n-cells) built atop a Lean-native port of the n-category engine at `zigzag-engine/`. Pure Lean, no kernel changes. Scheduled 6–8 weeks, not blocked by anything in this document. ### 2.8 Cell layer / reactive / GPU / shader / interaction - Cells-spec §6–§10 entirely achievable within this boundary. Cells are `Cell` Lean structures whose `line` field is a CType function; composition is path concatenation; interaction is via `IO` + GPU FFI. No kernel changes needed. ### 2.9 Summary of "below the boundary" **topolei can deliver:** cells-spec Phases 1–6 in their entirety, the full Rust evaluator, all of cells-spec §14's theorems, the zigzag higher-cell engine, cell graphs, rendering, direct manipulation, GPU shaders. The cells vision does not require kernel work. --- ## 3. Above the boundary (requires kernel work) These items are *desirable* but cannot be delivered by any library (topolei or otherwise) within Lean 4's current kernel. Each item lists (a) what it is, (b) why it's blocked, (c) what upstream Lean change would unblock it, (d) its topolei consumer (if any). ### 3.1 Native `Eq` as cubical identity **What:** `(a = b) : Type` being cubical — non-trivial paths, univalence, proof-relevant equality at the base-types level. **Blocked by:** `propext` + `Quot.sound` + `Prop`-irrelevance forcing UIP (§1). **Upstream change:** Lean would need to offer a *separate universe* in which one of the three axioms above is dropped — e.g. a `HType` universe or `--cubical-native` mode where `Eq` is the path type and propext no longer applies. This is a fundamental kernel extension, comparable in scope to adding Cubical Agda's `--cubical` flag to Agda. **topolei consumer:** none critical. Deep embedding already provides cubical equality as `Path` within CType. `Eq` / `Path` interop handled via `Bridge.lean`. ### 3.2 Definitional computation of cubical axioms **What:** Lean's kernel would compute `transp (refl) x` to `x` *automatically* (definitional equality), instead of requiring explicit `rw [eval_transp_top, …]` in proofs. **Blocked by:** axioms are opaque to Lean's definitional-equality check. The kernel's reduction algorithm only unfolds `def`s and recursors, not axioms. **Upstream change:** Lean would need a user-extensible definitional equality — e.g., a `@[compute]` attribute that lets axioms participate in reduction. No such mechanism exists. Adding one would require validating that the claimed reductions are confluent and type-preserving — a significant metatheoretic burden the kernel does not currently bear. **topolei workaround:** all reductions are propositional; proofs must invoke them via `rw` / `simp` / `dsimp`. We ship a simp set for the common reductions (future work, Phase C+). **topolei consumer:** UX. Propositional reductions make cubical proofs verbose. Worth-paying friction for the current scope. ### 3.3 HITs (Higher Inductive Types) in Lean's native inductive framework **What:** `inductive S¹ where | base : S¹ | loop : base = base` — defining types by point *and* path constructors directly in Lean's `inductive` command. **Blocked by:** Lean's inductive-type elaborator only generates point constructors; there is no mechanism for path constructors. Lean's recursor generator can't handle the higher-dimensional case-analysis needed for HITs. **Upstream change:** A `--hit` extension to the inductive elaborator that (a) accepts path constructors, (b) generates higher-dimensional recursors with proof obligations, (c) ensures consistency with the remaining kernel axioms. Cubical Agda supports this; Lean does not. **topolei workaround:** HITs can be encoded as Glue types + bespoke recursion principles inside CType. Awkward but expressible. **topolei consumer:** `Color/Space.lean` (modular color spaces), future Cell/Higher.lean extensions — but all existing uses encode HITs explicitly via Glue. ### 3.4 Universe-level univalence for `Type` **What:** `Type` itself being a univalent universe — `A ≃ B → A = B` at the Lean-universe level. **Blocked by:** Lean's `Type` satisfies UIP per §1. `A = B` at the universe level is trivial (only `rfl`). **Upstream change:** same as §3.1 — a separate cubical universe. **topolei has it:** `CType.univ` is a universe inside the embedded cubical calculus, and `transp_ua` proves univalence there. Users reason about universe paths via `uaLine` inside the calculus; they don't reason about them on Lean's `Type`. ### 3.5 Proof-relevant `Prop` **What:** `Prop` inhabitants being distinguishable — useful for modelling 2-cells, homotopies, truncation levels. **Blocked by:** `Prop` has proof irrelevance by kernel design. **Upstream change:** Remove proof irrelevance from `Prop` or add a second "relevant" `Prop`-like universe. Would break a large amount of existing Lean code that assumes `Prop`-irrelevance. **topolei has it:** relevance lives in `CTerm` / `CVal`, which are regular `Type`-level Lean data with no proof irrelevance. Homotopies are `CTerm`s inhabiting `.path (.path …)` types. Cells-spec's 2-cells and n-cells live entirely in this layer. ### 3.6 Native transport along Lean `Eq` **What:** Given `h : a = b : α` in Lean's `Eq` and `P : α → Type`, the coercion `h ▸ x : P b` should be *cubical transport* on Path- structured types. **Blocked by:** Lean's `▸` is `Eq.ndrec` — it computes only when `h` is `rfl`, and its one-step unfolding is UIP-dependent. **Upstream change:** same kernel work as §3.1. **topolei workaround:** users transport in the cubical world using `.transp` CTerm, then bridge back to Lean via the `Bridge` module for discrete types. Universe-level / HoTT-relevant transports live exclusively in the embedded calculus. ### 3.7 Cubical-aware `simp`/`rewrite` tactics **What:** tactics that understand Path-equality and rewrite cubically — e.g., "rewrite this occurrence using a path, respecting path composition and transport." **Blocked by:** tactic framework sees only Lean's `Eq`. Cubical paths are opaque terms it cannot pattern-match. **Upstream change:** either adding cubical-aware tactic primitives (extending the tactic API) or — more cleanly — making cubical paths first-class via §3.1. **topolei workaround:** users invoke cubical rewrites by explicit `rw [eval_...]` / `rw [readback_...]` calls. Less automation, more bookkeeping. Planned mitigation: a `cubical_simp` tactic as a pure-Lean extension in Phase 6 (cells-spec §19). ### 3.8 Kernel-verified FFI **What:** Lean's kernel would check that the Rust symbol `topolei_cubical_eval` actually implements the `eval_*` axioms before trusting it. **Blocked by:** `@[extern]` is trust-based by design. Verifying a Rust function against a Lean axiom is outside Lean's typechecker. **Upstream change:** A certified-compilation story — Lean would either check via translation validation or require a certificate. Nontrivial research topic. **topolei workaround:** differential fuzz testing (Phase D) + FFI_COMPLETENESS.md audit + review discipline. The Rust side matches the Lean spec by human inspection; we trust what we build. ### 3.9 Summary of "above the boundary" These are long-term targets that would require forking Lean's kernel or submitting substantive upstream proposals. None of them is a blocker for cells-spec's core vision. Each is a *UX enhancement* on top of what topolei already delivers. --- ## 4. Dependency graph of kernel items ``` ┌─────────────────────────────────────┐ │ 3.1 Native Eq as cubical identity │ │ (requires dropping UIP) │ └─────────────────────────────────────┘ ▲ ▲ ▲ │ │ │ │ │ │ ┌────────────┘ │ └────────────┐ │ │ │ │ │ │ ┌───────────────┐ ┌────────────────────┐ ┌─────────────────────┐ │ 3.4 Type- │ │ 3.6 Native Eq ▸ │ │ 3.7 Cubical-aware │ │ level univ. │ │ as cubical transp │ │ tactics │ └───────────────┘ └────────────────────┘ └─────────────────────┘ ┌──────────────────────────────┐ │ 3.2 Definitional computation │ ← independent of 3.1, but benefits │ of cubical axioms │ users regardless of cubicality └──────────────────────────────┘ ▲ │ enables ▼ ┌──────────────────────────────┐ │ 3.7 Cubical-aware tactics │ ← also benefits from 3.1 └──────────────────────────────┘ ┌─────────────────────────────────────────┐ │ 3.3 HITs in native inductive framework │ ← mostly independent; │ │ better with 3.1 but └─────────────────────────────────────────┘ not required ┌──────────────────────────────┐ │ 3.5 Proof-relevant Prop │ ← independent; breaking change └──────────────────────────────┘ ┌──────────────────────────────┐ │ 3.8 Kernel-verified FFI │ ← independent; cross-cutting └──────────────────────────────┘ ``` **3.1 is the keystone:** if Lean adopted a cubical universe, most other items follow or simplify. Until then, everything above is deliverable only via deep embedding (§2). --- ## 5. Boundary diagnostic checklist Use this to quickly determine whether a feature request lies below or above the boundary: | Question | If yes, below boundary (topolei can deliver) | |----------|----------------------------------------------| | Is the feature expressible in `CTerm` / `CType`? | ✅ yes | | Does the feature only require propositional (not definitional) reduction? | ✅ yes | | Does the feature live inside `CType.univ` (the embedded universe)? | ✅ yes | | Does the feature avoid depending on `propext` being false? | ✅ yes | | Does the feature avoid requiring Lean to pattern-match on paths? | ✅ yes | | Question | If yes, above boundary (requires kernel work) | |----------|-----------------------------------------------| | Does the feature make Lean's native `Eq` non-trivial on a type where `DecidableEq` fails? | ❌ blocked | | Does the feature require automatic (non-tactic) cubical reduction inside kernel type-checking? | ❌ blocked | | Does the feature need HIT path constructors in the `inductive` keyword? | ❌ blocked | | Does the feature need 2-cells or higher in `Prop`? | ❌ blocked | | Does the feature require Lean's typechecker to verify Rust FFI implementations? | ❌ blocked | --- ## 6. What topolei commits to delivering Scope: everything below the boundary (§2), full Rust evaluator, all cells-spec phases 1–6. Bridges (§2.6) provide partial interop with `Eq` for discrete types. Scope: NOT delivering. None of §3. Attempts to deliver them within topolei would either (a) require forking Lean (out of scope), (b) require abandoning soundness (not acceptable), or (c) duplicate effort that upstream Lean is better positioned to handle. If upstream Lean ever adds a cubical universe (§3.1), topolei's deep embedding can be retired incrementally in favor of the native layer — most of the code (the axiom set, the reductions, the Bridge module) would become theorems rather than primitives. The Rust backend's role shrinks but doesn't disappear: performance wins for cubical reductions remain valuable regardless of kernel native support. --- ## 7. Recommendations for upstream Lean *(Not a project dependency — topolei ships without these. Recorded here as a standing list of things worth advocating for in Lean 4 developer discussions.)* 1. **Highest value:** Definitional-equality extensibility (§3.2). Unblocks cubical UX *without* breaking any existing invariants. Could be implemented as a restricted rewrite engine attached to kernel reduction. 2. **Medium value:** Opt-in universe with reduced axioms (§3.1 via a `CubeType` universe sibling to `Type`). Would let cubical HoTT be a native Lean feature for users who opt in, while preserving `Type` for classical work. 3. **Research-grade:** Kernel-verified FFI (§3.8). Out of scope for any near-term Lean release but valuable for production trust. 4. **Lower priority:** HITs (§3.3), proof-relevant `Prop` (§3.5). Both handleable via embedding; native support is UX, not necessity. --- --- ## 8. PR readiness checklist — self-assessment for contributing to Lean 4 *A standing checklist for when a kernel-level PR feels within reach. Not a gatekeeping list; a learning roadmap. Work through the items in rough order. The goal is not to pass every item before writing a single word, but to know where you are on each axis, and which axis is the current bottleneck.* ### 8.1 Foundational type-theory literacy (the common base) - [ ] Can state the **inference rules** for intensional MLTT (Π, Σ, `Eq`, inductive types) without reference. - [ ] Can explain the **difference between propositional and definitional equality**, and what "reduction" means at each level. - [ ] Can sketch the **Hofmann-Streicher argument** that UIP follows from `propext` + `Quot.sound` + `Prop`-irrelevance. Bonus: identify which of the three is *actually* load-bearing in different presentations. - [ ] Can explain **what makes a universe univalent** and why univalence contradicts UIP. - [ ] Can describe **higher inductive types** via Cubical Agda's path constructors, and state their recursor correctness condition. - [ ] Can read a **CCHM paper passage** (Cohen-Coquand-Huber- Mörtberg 2016) and explain a `transp` or `hcomp` rule in your own words. - [ ] Know what **canonicity** and **normalization** mean, and why they are the metatheorems any new reduction rule must preserve. ### 8.2 Lean 4 kernel literacy - [ ] Understand how **Lean's kernel checks definitional equality**: reduction, type-directed elaboration, η, proof irrelevance. - [ ] Read the **Lean 4 kernel source** (`src/kernel/`) at least once: `TypeChecker`, `Reducer`, `whnf`, `isDefEq`. Know where axioms are stored and how they interact with reduction. - [ ] Understand **Lean's universe hierarchy**, cumulativity, and how `Prop` differs from `Type u`. - [ ] Understand the **inductive elaborator**: `Construction`, `recursor` generation, positivity check, nested/mutual inductives. - [ ] Know how **`@[extern]` and `@[implemented_by]`** work at the compiler level vs. the kernel level (only the former ships Rust/C code; the latter routes at codegen). - [ ] Have written **at least one non-trivial Lean 4 kernel-adjacent piece of code** — e.g., a custom elaborator, a tactic, a user-defined reducer extension, or a metaprogram that inspects the reduction behaviour. - [ ] Read **existing Lean 4 RFCs and closed PRs** on kernel changes to see the discussion style and rigor expected. ### 8.3 Item-specific preparation For each kernel item in §3 that you want to propose, the cliff face gets smaller as you check these boxes. #### 8.3.1 For §3.2 — definitional-equality extensibility (highest-value) - [ ] Can articulate the **difference between axioms and reduction rules** at the kernel level. Why can't axioms currently participate in `whnf`? - [ ] Know how **rewrite systems interact with type checking** — confluence, termination, subject reduction. Read one paper on SMT-style or equality-saturation rewriting inside a proof assistant. - [ ] Can explain **why a naive `@[compute]` on axioms breaks soundness** (axioms can be inconsistent pairs; rewriting would let the kernel derive `False`). - [ ] Have a design for **how the proposer verifies confluence** — e.g., external tool, proof obligation at axiom-declaration time, trusted metatheorem. - [ ] Know **Agda's `REWRITE` feature** and can explain its tradeoffs (convenient, but trust-based; PR would likely propose something analogous or more conservative). - [ ] Have a **concrete use case from topolei** — e.g., "after this change, `rw [eval_transp_top]` becomes `rfl` in these contexts" — to motivate the proposal with lived experience. #### 8.3.2 For §3.1 — cubical universe (keystone, hardest) - [ ] Fluent in **CCHM §§2–6** — interval, face lattice, reductions, Glue, univalence. Can present each from memory. - [ ] Understand **at least one normalization proof** for cubical type theory (e.g., Sterling-Angiuli NbE for CTT). - [ ] Can describe **how Cubical Agda integrates** cubical type theory into Agda's existing universe hierarchy. What did Agda's kernel change? What stayed the same? - [ ] Understand **the sized-types / inductive-inductive / indexed family interaction** with cubical — e.g., why W-types need special treatment. - [ ] Have a sketch of **what coexistence looks like**: two universes (`Type` + `CubeType`), with what coercions and what restrictions? Does `propext` apply in `CubeType`? How does `Prop` fit in? - [ ] Read **at least one Lean kernel maintainer's statement** (Leo's blog, the Lean Zulip, etc.) on their position on HoTT / cubical extensions. Know the political climate. - [ ] Implementation experience at the kernel level — have you extended *some* proof assistant's kernel (even a toy one, even just a new type former)? If not, this is the longest-running prerequisite. #### 8.3.3 For §3.3 — HITs in native inductive framework - [ ] Can define **S¹** in Cubical Agda and step through its recursor and computation rules. - [ ] Understand how **HIT elimination differs from ordinary inductive elimination** — two-level: point rule + path rule. - [ ] Know **the consistency proof sketch** for a fragment (e.g., S¹ with `propext`-free intensional MLTT). - [ ] Have a design for **how Lean's inductive elaborator would accept path constructors** — syntax, positivity, recursor generation. - [ ] Understand the **Lean Community HoTT library** (if it exists) as a source of use cases and prior art. #### 8.3.4 For §3.5 — proof-relevant `Prop` - [ ] Can articulate **why `Prop`-irrelevance is load-bearing** in Lean 4's practice (tactic automation, `decide`, Mathlib patterns). This is the PR that most risks being rejected on pragmatic grounds. - [ ] Understand the **squashing / truncation modality** — propositional truncation `‖·‖` in HoTT — and whether providing it solves the problem without removing `Prop` irrelevance. - [ ] Have concrete **use cases that require non-trivial `Prop`** — topolei's 2-cells are handled via `CTerm` (Type-level), so this is low-priority for this project specifically. #### 8.3.5 For §3.8 — kernel-verified FFI - [ ] Have read about **CompCert**, **CakeML**, and **Alectryon**- style certified compilation. - [ ] Can distinguish **translation validation** from **certified compilation** and articulate the tradeoffs. - [ ] Understand **Lean's `@[extern]` trust model** — what exactly is trusted vs. what is verified? - [ ] Have a concrete **attack surface analysis** — how could a malicious Rust impl subvert kernel soundness? - [ ] This is research-grade; realistically a multi-year effort. Not a near-term PR candidate. ### 8.4 Drafting the PR — when the research has landed Once you're 80%+ through the relevant §8.3 subsection: - [ ] **Draft a Lean 4 RFC** (Request For Comments) in the community repo BEFORE writing code. PRs without RFC discussion rarely land for kernel-level proposals. - [ ] Include a **motivating example** that uses topolei. Real lived pain from `rw [eval_...]` chains beats abstract appeals. - [ ] Include **prior art** — Cubical Agda, Coq's `SProp`, OCaml's extension mechanisms — with accurate descriptions of what they do and don't do. - [ ] Include a **consistency argument** — if not a full proof, then at least the proof sketch and citation of the relevant papers. - [ ] Include a **"what existing code breaks?"** section. For any PR touching `propext` / `Quot.sound` / `Prop`-irrelevance, the answer is "a lot" — honesty here is respected. - [ ] Include a **backwards-compatibility story**: opt-in flag, new universe, deprecation path, whatever applies. - [ ] Draft a **minimal kernel patch** — even a 50-line proof of concept helps reviewers understand the proposal concretely. - [ ] Be prepared for **a long feedback cycle** (months, not days) and for the outcome to be **"close without merge"** on the first attempt. Kernel PRs are rarely merged on first try. ### 8.5 Post-submission — learning from the process - [ ] Respond to all reviewer questions with **precise, cited answers**. Vague answers are the main reason kernel PRs stall. - [ ] Be willing to **narrow the proposal**: reviewer asks for scope reduction is common and not a rejection. - [ ] If the PR is closed, **extract the specific objections** and address them in a future revision. Kernel-level changes often take 2–3 attempts over 1–2 years. - [ ] Whether accepted or not, **write up what you learned** — the proposal itself becomes documentation, and future proposers benefit. ### 8.6 Current readiness estimate Self-assess roughly at the start of each research phase: | Sub-section | Your current estimated % ready | |-------------|-------------------------------| | §8.1 Foundational type theory | ____% | | §8.2 Lean 4 kernel literacy | ____% | | §8.3.1 Def-eq extensibility (§3.2) | ____% | | §8.3.2 Cubical universe (§3.1) | ____% | | §8.3.3 HITs (§3.3) | ____% | | §8.3.4 Proof-relevant Prop (§3.5) | ____% | | §8.3.5 Verified FFI (§3.8) | ____% | Update this table as research advances. When any §8.3 row hits 80%+ AND §8.1 and §8.2 are both above 70%, consider drafting the RFC for that specific item. The gating principle: *research depth first, PR second*. --- *End of KERNEL_BOUNDARY.md. Update this document when upstream Lean moves any item between regions, when topolei delivery plans change, or as your readiness estimates in §8.6 advance.*