From 95f11020d7b347df5e52e89c65d279d0cc386059 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Fri, 1 May 2026 00:04:48 -0600 Subject: [PATCH] Document the question-form algebra + Dev_Algebra plan + Eulerian record MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three companion documents capturing the design corpus that emerged from the mid-REL2 conversation about the universal question form, the macro-layer collapse-to-one, and the autodiscovery tactic. docs/QUESTIONS.md — Philosophy. The ODE.lean → universal question-form motivation. CompQ as the canonical question type. Classifiers (IsConstLine, IsFullFace, IsPathLine, …) mirroring ODE.IsExact / IsBernoulli. Three levels of commitment (structural reification / routing / question-driven proofs). The realisation that the macro layer itself is `comp` lifted to the meta-level — the same five-field shape applied at a higher stratum. docs/ALGEBRA_PLAN.md — Dev_Algebra branch design. One universal macro `restructure` covering all 32+ proof-organisation operations as frozen partial applications. `@[macroAlias]` for naming-by-usage, `@[methodology]` + `cubical_search` for autodiscovery, widget rendering the question-graph, monadic Edit + comonadic Context with soundness-guard distributive law. Phases A–D′ (~19 days) + open-ended Phase E reorganisation. Sequencing relative to REL2, risk register, definition-of-done, OQ list. docs/EULERIAN.md — The poetic record. Each architectural metaphor (river bed, river, ferry, current, carrying load, wake, confluence, map, autodiscovery) paired with its concrete Lean / Rust counterpart. Stratum table showing how the same universal pattern applies at cubical / question / meta / tactic levels. What the discipline buys; where the metaphor strains and how to talk about those strains. Companion to existing INDUCTIVE_TYPES.md / REL2_PLAN.md / KERNEL_BOUNDARY.md. Total ~1100 new lines. No code changes; 74/76 + 46/46 tests still pass. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/ALGEBRA_PLAN.md | 484 +++++++++++++++++++++++++++++++++++++++++++ docs/EULERIAN.md | 329 +++++++++++++++++++++++++++++ docs/QUESTIONS.md | 316 ++++++++++++++++++++++++++++ 3 files changed, 1129 insertions(+) create mode 100644 docs/ALGEBRA_PLAN.md create mode 100644 docs/EULERIAN.md create mode 100644 docs/QUESTIONS.md diff --git a/docs/ALGEBRA_PLAN.md b/docs/ALGEBRA_PLAN.md new file mode 100644 index 0000000..1c82849 --- /dev/null +++ b/docs/ALGEBRA_PLAN.md @@ -0,0 +1,484 @@ +# ALGEBRA_PLAN.md — `Dev_Algebra`: the universal-macro layer + +*Drafted 2026-05-01 on `Dev_REL2`. Captures the design and +implementation plan for the long-running `Dev_Algebra` branch, +which lifts the project's universal question form (`docs/QUESTIONS.md`) +to a full **meta-level proof-organisation algebra** — one universal +macro that reflects `comp` at the source-code level, plus a small +attribute-and-tactic layer for autodiscovery of proof +methodology.* + +--- + +## 0. The headline + +> **One macro. Built from `comp`. Aliases accrue by usage; tactics +> are search over a library that grows under structural-Path +> declarations alone.** + +A first sketch enumerated 32 macros (one per cubical primitive + +boundary / face / substitution / soundness families). All 32 are +**frozen partial applications of a single universal macro**, +`restructure`, which is `comp` lifted from the cubical-CTerm world +to the meta-Lean-source world. The codebase ships with one macro +and zero aliases; aliases accrue when patterns earn names. + +--- + +## 1. Goals + +### 1.1 In scope (Dev_Algebra REL2.5) + +- One universal macro `restructure` covering all proof-organisation + operations: relocate, rename, factor, merge, splice, classify, + refactor-with-witness, etc. +- An attribute `@[macroAlias]` letting users (or the system itself) + name recurring `restructure` invocations as ordinary Lean `def`s. +- An attribute `@[methodology]` registering tactic-fragments tagged + by classifier, plus the `cubical_search` tactic that walks the + registry, applies fragments via `restructure`, and *transports* + fragments along declared structural Paths to derive new + candidates from old ones. +- A widget rendering the question-graph and dispatching code + actions via `MakeEditLinkProps.ofReplaceRange`. +- Incremental reorganisation: existing theorems gain question / + classifier annotations file-by-file. Existing names are + preserved as derived corollaries — no breaking change downstream. + +### 1.2 Out of scope (deferred to future REL3+) + +- Proof-body synthesis. Bodies remain hand-written (or written by + AI agents in conventional tactic mode). The macro layer manages + *structure*, never *bodies*. +- Higher-question algebra (paths-between-classifier-equivalences; + 2-cells in the question category). Out of scope until + cells-spec §8. +- Cross-language tooling (e.g., a CLI that batch-restructures + outside the LSP session). Listed in §10 OQ. + +### 1.3 Non-goals + +- Replacing Lean 4's existing tactic framework. `cubical_search` + is a tactic *built on top of* the standard infrastructure, not a + replacement. +- Eliminating hand-written tactic scripts. The boundary is + deliberate: structure is mechanical, bodies are creative. + +--- + +## 2. The universal macro: `restructure` + +### 2.1 Signature + +``` +restructure + (i : MetaPosition) -- where in source: file slot, + -- namespace position, decl ID + (Context : MetaCType) -- meta-type of the artifact: + -- theorem, def, instance, file, + -- classifier-set, … + (φ : MetaClassifier) -- when this restructuring applies + (witness : MetaArtifact) -- new content valid on φ + (fallback : MetaArtifact) -- existing content off-φ + : Edit Unit -- effect: source mutation +``` + +Same five fields as `comp i A φ u t`, promoted to the meta level. +The macro emits zero or more `MakeEditLinkProps.ofReplaceRange` +calls in the `Edit` monad. + +### 2.2 Meta-mirror types + +```lean +namespace Algebra + +inductive MetaCType where + | theorem : MetaCType -- a `theorem foo : T := proof` + | definition : MetaCType -- a `def foo := body` + | instance : MetaCType + | structure : MetaCType + | inductive_ : MetaCType -- a Lean `inductive` declaration + | file : MetaCType + | namespace_ : MetaCType + | classifierSet : MetaCType + | dependencyEdge : MetaCType + +inductive MetaClassifier where + | always : MetaClassifier -- "everywhere" + | never : MetaClassifier -- "nowhere" + | atDecl : Name → MetaClassifier + | inFile : System.FilePath → MetaClassifier + | underAttribute : Name → MetaClassifier + | dependencyOf : Name → MetaClassifier + | meet : MetaClassifier → MetaClassifier → MetaClassifier + | join : MetaClassifier → MetaClassifier → MetaClassifier + +inductive MetaArtifact where + | source : String → MetaArtifact -- raw Lean text + | declAt : Lean.Syntax → MetaArtifact -- a syntax tree + | refTo : Name → MetaArtifact -- a reference to existing decl + | empty : MetaArtifact -- "remove this" + +end Algebra +``` + +Every restructuring operation in the codebase reduces to a +`restructure` call with these data. + +### 2.3 Frozen aliases — the 32 macros revisited + +| Alias | Frozen arguments | +|---|---| +| `transport_artifact i ctx w` | `φ := .always`, `witness := w`, `fallback := w` | +| `relocate_invariant i src dst` | `Context := .file`, classifier `inFile src`, witness `inFile dst` | +| `compose_proof_fragments` | pure `restructure` (no freezing) | +| `multi_compose ...` | `φ := join_of(branches)`, weave witnesses | +| `rename_throughout x y` | `φ := atDecl x`, `witness := y`, `fallback := x` | +| `dispatch_on_shape S brs` | `Context := .inductive_`, fold over branches | +| `present_alternative T e` | `Context := MetaGlue T e _` (Glue lifted to meta) | +| `submit_face_proof t a` | classifier-conditioned `glueIn`-shape | +| `extract_underlying g` | inverse of `present_alternative` | +| `define_question_shape S` | `Context := .inductive_`, witness = the schema decl | +| `instantiate_question S c args` | `restructure` at a fresh position | +| `MetaPath a b` | `Context := .definition`, witness emits an alias | +| `treat_as_equivalence` | `MetaPath` plus a propositional witness | +| `materialize` | leaf: emit Lean text via `ofReplaceRange` | +| `parse_back` | dual leaf: read Lean source into a `Question` value | +| `preserve_typing` | guard composed *over* any `restructure` call | +| `preserve_equivalences` | guard checking declared `MetaPath`s survive | +| … (all others) | curry / pin / specialise the same five parameters | + +**Implementation:** the codebase ships with `restructure` itself +(~150 lines). Each `@[macroAlias] def …` is a 1–3-line shorthand. +The widget surfaces "name this pattern?" when an instantiation +recurs, automatically inserting a new alias. + +--- + +## 3. The Edit monad and Context comonad + +### 3.1 The pair + +```lean +namespace Algebra + +/-- The `Edit` monad: a thread of source mutations. Leaf operation + is `ofReplaceRange`; everything else composes from there. -/ +structure Edit (α : Type) where + run : Lean.Server.CodeActionContext → IO (α × List MakeEditLinkProps) + +instance : Monad Edit := … + +/-- The `Context` comonad: at each point in the source, exposes the + surrounding state — theorems in scope, classifiers applicable + to the current goal, the question-graph neighbourhood. -/ +structure Context (α : Type) where + here : α + scope : Lean.Environment + graph : QuestionGraph + pos : Lean.Syntax + +instance : Comonad Context := … + +end Algebra +``` + +### 3.2 The distributive law + +The comonad provides context; the monad consumes context and +produces edits: + +```lean +/-- Lift a context-aware decision into an edit. -/ +def Algebra.contextualEdit + (decide : Algebra.Context α → Algebra.Edit β) : + Algebra.Context α → Algebra.Edit β := + fun ctx => decide ctx +``` + +This is the standard "comonad-to-monad" distributive setup; it lets +you write context-aware code actions ergonomically: + +```lean +def renameQuestion (newName : String) : Context CompQ → Edit Unit := + contextualEdit fun ctx => do + let oldName := ctx.here.name + -- find every reference to oldName in ctx.scope + let refs ← ctx.scope.findReferences oldName + -- emit one ofReplaceRange per reference + for r in refs do + ofReplaceRange r.range newName +``` + +### 3.3 Soundness invariant + +Every `Edit` operation passes through a `preserve_typing` guard: + +```lean +def Edit.guarded (e : Edit α) : Edit α := do + let (a, edits) ← e.run + -- Apply edits to a fresh source buffer; type-check + let buf ← applyEdits edits + let result ← typeCheck buf + if result.hasErrors then + throw "restructure would break typing — aborting" + return (a, edits) +``` + +This is the global invariant: **no `Edit` ever surfaces in the +editor that would break type-checking**. The user can click any +code action confidently. + +--- + +## 4. The autodiscovery tactic: `cubical_search` + +### 4.1 The methodology library + +```lean +@[methodology] +def constLineSolver : Methodology := + { classifier := IsConstLine + body := fun q => CompQ.const_line_is_identity q (by classifier_check) } + +@[methodology] +def fullFaceSolver : Methodology := + { classifier := IsFullFace + body := fun q => CompQ.full_face_is_identity q (by classifier_check) } + +-- … one per cubical-core axiom; ~12-15 base methodologies. +``` + +The attribute registers the methodology in a global discrtree, +indexed by classifier shape. + +### 4.2 The tactic + +```lean +syntax "cubical_search" : tactic + +elab_rules : tactic + | `(tactic| cubical_search) => do + let goal ← Lean.Elab.Tactic.getMainGoal + let goalType ← goal.getType + -- 1. Reify goal as a CompQ (via parse_back from §3 of ALGEBRA_PLAN) + let q ← reifyAsCompQ goalType + -- 2. Find applicable methodologies via classifier matching + let candidates ← MethodologyLibrary.findMatching q + -- 3. Try each in priority order + for M in candidates do + try + let proof ← M.body q + Lean.Elab.Tactic.assignGoal goal proof + return + catch _ => continue + -- 4. Try methodology-transport: for each existing M and each + -- declared MetaPath M.classifier ↦ Q, attempt the transport + let transported ← deriveByTransport q + for M' in transported do + try ... (same as step 3) ... + -- 5. Structured failure + throwError "no methodology applies; consider registering one + for {q.classifierShape}" +``` + +### 4.3 The methodology-transport mechanism + +The crucial autodiscovery payoff: + +```lean +def deriveByTransport (q : CompQ) : MetaM (List Methodology) := do + let knownPaths ← getStructuralPaths + let library ← getMethodologyLibrary + let mut out := #[] + for path in knownPaths do + -- path : MetaPath classifierA classifierB + if path.target.classifier.matches q then + for M in library.matching path.source.classifier do + let M' := transp path.line .top M.body + out := out.push { classifier := q.classifierShape, body := M' } + return out.toList +``` + +Once a small library of base methodologies exists, every new +structural Path declared in the codebase **automatically generates +new methodology candidates** by transporting existing methodologies +across the path. Twenty starting methodologies + a hundred +declared paths → potentially thousands of derived methodologies, +each formally certified-by-construction. + +### 4.4 Failure as a feature + +When `cubical_search` fails it emits a structured report: + +``` +no methodology applies for question shape: + CompQ + body := .glue ψ T f fInv s r c A + φ := .top + isPath := false + isConst := false + isPi := false + isGlue := true (matched) + +candidates considered: + ✗ glueAtTopSolver — guarded by `IsConstLine`, didn't fire + ✗ glueAtTopSolver_specialised — registered for ψ = eq0, current ψ = eq1 + +derive-by-transport: + no MetaPath connects current classifier to a known one + +would you like to register a new methodology? [click here] +``` + +The "click here" is itself a code action that opens a skeleton +`@[methodology] def …` declaration via `ofReplaceRange`, which the +human (or the next agent) fills in. + +--- + +## 5. The widget + +### 5.1 Surface + +A `Lean.Widget.UserWidgetDefinition` rendering, for the active +declaration: + +- The current `CompQ` value (or its absence) at the cursor. +- The classifier shape of the goal. +- The list of applicable methodologies. +- Buttons: "factor question," "rename classifier," "compose with + …," "transport along …," "name this pattern." +- The question-graph neighbourhood (5 hops in each direction), + rendered as an interactive node-link diagram. + +### 5.2 Code-action plumbing + +Every button corresponds to one or more `Edit` actions. When +clicked, the widget calls back to Lean (via `Lean.Widget.RpcCall`), +the Edit runs, the source mutates via `ofReplaceRange`, the LSP +re-elaborates, and the widget re-renders the new state. + +### 5.3 No-LSP fallback + +For users without the widget (CLI, headless CI), the same +operations are available as `lake exe algebra-restructure` +subcommands. The widget is the convenience surface; the +underlying algebra works either way. + +--- + +## 6. Phases + +| Phase | Deliverable | Days | +|---|---|---| +| A | `MetaCType` / `MetaClassifier` / `MetaArtifact` data types — meta-mirror of `CType` / `FaceFormula` / `CTerm` | 3 | +| B | `restructure` macro + `Edit` monad + `Context` comonad + soundness guard | 5 | +| C | `@[macroAlias]` attribute + alias-suggestion widget | 3 | +| D | `UserWidgetDefinition` rendering question-graph; `ofReplaceRange` integration | 4 | +| D′ | `@[methodology]` attribute + `cubical_search` tactic + methodology-transport clause | 4 | +| E | Reorganisation — incremental annotation of existing theorems with `@[question]` / `@[classifier]`; aliases accrue as patterns earn names | open-ended | + +**Committed: ~19 days** for Phases A–D′. Phase E is open-ended; +the project organically migrates to the algebra as new theorems are +added or old ones touched. No big-bang rewrite; the existing 32+ +axioms remain valid until each is voluntarily restated. + +--- + +## 7. Risks & mitigations + +| Risk | Likelihood | Mitigation | +|---|---|---| +| `restructure` design hard to get right with no escape hatches | Medium | Phase B explicitly tests against ~10 representative restructuring scenarios from existing engine refactors before committing the design. | +| Macro debuggability — failed elaboration surfaces inside macro internals, not user source | Medium | Every `restructure` call wraps in a context-rich error report naming the classifier that didn't fire and the artifact that wasn't found. | +| Editor lock-in (widget assumes Lean LSP + WebView client) | Low | §5.3 fallback: same operations as `lake exe algebra-restructure` subcommands. Formal artifact (the Lean source) is still the source of truth. | +| Search performance — `cubical_search` walking a large library on every goal | Medium | `MethodologyLibrary` indexed by classifier shape (discrtree). Failed matches are O(1) on classifier disjointness; only matching methodologies are tried. | +| Compile-time cost — every macro expansion triggers Lean elaboration | Low | Macro outputs are small (`ofReplaceRange` calls); elaboration cost is dominated by re-checking the user's actual proof, not the macro itself. | +| Two different generated tactic scripts represent the same morphism | Low | Canonical-form pass on emitted source; structural equality on `restructure` invocations (REL2.5+ refinement). | + +--- + +## 8. Sequencing relative to REL2 + +``` + cubical-engine main (REL1 landed; REL2 Phase 1+2 on Dev_REL2) + │ + ┌───────────────┴───────────────┐ + ▼ ▼ + Dev_REL2 (continuing) Dev_Algebra (new, parallel) + Phase 3: paideia K7 Phase A: meta-types + (5–10d, paideia repo) Phase B: restructure + Phase C: macroAlias + Phase D: widget + Phase D': cubical_search + Phase E: incremental reorg + │ │ + └────────────┬───────────────────┘ + ▼ + Coordinated merge train when both arcs ready + (engine `Dev_REL2` + `Dev_Algebra` → main; topolei, + paideia → main; engine issue #1 closes with K7 + + algebra-driven proof restructure) +``` + +The two arcs are **independent at the engine level** (neither +blocks the other); they coordinate at merge time. + +--- + +## 9. Definition of "done" + +- Every existing `eval_*` / `vTransp_*` / `vCompValue_*` / Glue / + Soundness theorem has at least one corresponding + `@[methodology]` registration that closes its representative + question via `cubical_search`. +- The widget renders the question-graph for any open Lean file. +- A code action exists for: factor, compose, rename, relocate, + attach-classifier, declare-MetaPath, transport-methodology. +- A regression suite verifies that every code action preserves + type-checking on the engine's existing test corpus. +- `KERNEL_BOUNDARY.md §3.7` (cubical-aware tactics) updated to + record `cubical_search` as a mid-horizon delivery (still + pending full `cubical_simp` for §3.7's strongest form). + +--- + +## 10. Open questions (logged here) + +1. **Domain of `restructure`** — strictly cubical-core artifacts + (theorems / definitions in `CubicalTransport.*`), or everything + in scope (any Lean declaration)? Cubical-core is simpler and + more justifiable; everything-in-scope is more general but + harder to keep sound. Default: cubical-core, with a per-call + opt-in to broader scope. +2. **Persistence** — graph computed on the fly each LSP session + (always-fresh, slower), or persisted as Lean attributes + (cached, possibly stale). Default: on the fly, with an + optional cache file generated by `lake exe algebra-cache`. +3. **CLI tool** — do we ship `lake exe algebra-restructure` from + day one, or wait for editor adoption? Default: from day one, + so headless CI can verify code actions. +4. **AI prior surface** — does `cubical_search` consult a learned + prior (from past successes) for ordering candidates? + Out-of-scope for REL2.5; tracked for REL3+. + +--- + +## 11. Why this matters (summary) + +The Eulerian framing throughout the project has emphasised +**river bed → ferry → carrying load** for REL2. `Dev_Algebra` adds +the **map**: a navigable register of currents, a tooling +infrastructure that lets you trace any flow, splice rivers, divert +without losing volume. The map is built from the same primitive +the rivers are built from. Every layer of the system, from the +cubical-CTerm engine through the Lean-source-organisation algebra, +is the same `comp`-shape applied at a different stratum. The +codebase is closed under its own operations — and the autodiscovery +tactic is the visible face of that closure. + +--- + +*End of ALGEBRA_PLAN.md. Companion to `QUESTIONS.md` (philosophy) +and `EULERIAN.md` (poetic record).* diff --git a/docs/EULERIAN.md b/docs/EULERIAN.md new file mode 100644 index 0000000..8d4fc0a --- /dev/null +++ b/docs/EULERIAN.md @@ -0,0 +1,329 @@ +# EULERIAN.md — The Project's Poetic Record + +*Drafted 2026-05-01 on `Dev_REL2`. The metaphors that have +guided this project's design discipline, paired with their concrete +Lean / Rust counterparts. This document is for newcomers, future +agents, and the project's own philosophical record. It is not a +specification — `INDUCTIVE_TYPES.md`, `REL2_PLAN.md`, +`QUESTIONS.md`, `ALGEBRA_PLAN.md`, and `KERNEL_BOUNDARY.md` carry +that load. This document carries the *image of the system*.* + +--- + +## 0. Why a poetic record + +Cubical type theory's geometric vocabulary — paths, faces, lines, +fillers, transports, currents — is not decoration. It is the +*design discipline* that keeps the codebase architecturally +coherent across REL1, REL2, and beyond. When a metaphor lands +cleanly on a concrete Lean construct, that's the system signalling +its own architectural soundness. When a metaphor breaks down, the +underlying construct usually has a real design flaw. + +The metaphors below are not aspirational; each one names something +that *already exists in the code* (or is committed to in a planned +phase). + +--- + +## 1. The river bed — `CType.interval` + +> *The river requires a river bed. Without one, paths flow over +> unspecified medium.* + +**Concrete:** `CType.interval` (REL2 Phase 1, landed 2026-04-30 as +commit `ce2ee87` on `Dev_REL2`). Promoted the cubical interval to +a first-class type primitive. Pre-REL2, `CTerm.dimExpr r` typed at +the placeholder `.univ`; post-REL2 it types at `.interval`. + +**Why it matters:** Path-constructor dim arguments (`loop @ r`, +`seg @ r`, `squash _ _ @ r`, …) now carry real semantic ground. +The interval is the *medium* that all dimension-flowing +computation requires. Without it, the engine had Paths but no +canonical river-bed type for the dim-coordinate paths flow along. + +--- + +## 2. The river — `Path` and `transp` + +> *Water moves. A path is the witness of motion from one bank to +> the other; transport is the act of crossing.* + +**Concrete:** `CType.path A a b` (the type of paths from `a` to +`b` in `A`); `CTerm.transp i A φ t` (transport of `t : A(0)` to +`A(1)` along the line `λi.A`, restricted by face `φ`). + +**Why it matters:** Paths are proof-relevant equalities; transport +is the operation that turns a path into actual movement of values. +This is the cubical equivalent of "we don't just *know* the river +runs from source to mouth; we *follow* the current." + +--- + +## 3. The estuary — boundary firing on path constructors + +> *Where the river meets the sea, the current becomes one with +> something larger.* + +**Concrete:** Path-ctor boundary firing in `eval`: when a `.dim`- +typed argument lands on a face in the constructor's boundary +system, eval substitutes the boundary clause body instead of +producing the raw `vctor`. Currently TODO in REL2 (REL1 has the +syntactic shape; REL2.1 lands the firing semantics). + +**Why it matters:** This is what makes HITs *compute*. S¹'s `loop +@ 0` reduces to `base`; `‖A‖₋₁`'s `squash x y @ 0` reduces to +`x`. Without boundary firing, HITs are syntactic placeholders; +with it, they are operational. + +--- + +## 4. The current — pointwise transport distribution + +> *Matter flows along the geometry; the current is how it gets +> there.* + +**Concrete:** Pointwise transport distribution over `.ind S +params`: when transport encounters a `.ctor` term, it distributes +through the ctor's args by transporting each non-recursive arg via +its CType's transport rule, recursing on `.self` args. Currently +deferred to REL2.1 (REL2.0 produces stuck `ntransp` neutrals, +correct but not maximally reduced). + +**Why it matters:** Once distribution lands, `K7.step` (paideia's +gradient composition, REL2 Phase 3) reduces *definitionally* +instead of staying as a syntactic `.comp`. The river not only has +a bed and a current — its motion is *visible*, not just *implied*. + +--- + +## 5. The ferry — `Bridge.lean` (`Eq ↔ Path`) + +> *Two rivers run in parallel; the ferry carries payload between +> them.* + +**Concrete:** `CubicalTransport/Bridge.lean` (REL2 Phase 2, +landed 2026-04-30 as commit `7152807` on `Dev_REL2`). The +`CubicalEmbed α` typeclass with default instances for `Bool`, +`Nat`, and `List α [CubicalEmbed α]`. Forward bridge `Eq.toPath` +(always available); backward bridge `Path.toEq_canonical` +(REL2.0 canonical case via `toCTerm_injective`); full backward +bridge over arbitrary well-typed paths is REL2.1. + +**Why it matters:** Lean's discrete `Eq` river (Mathlib, decidable +equality, all the discrete-math infrastructure) and the embedded +cubical `Path` river (univalence, proof-relevant identity, the +whole CCHM apparatus) flow in parallel through the codebase. The +ferry lets payload — Mathlib lemmas, decidable witnesses, K7 +encoding — cross between them. Without the ferry, the two rivers +exist but can't share cargo. + +--- + +## 6. The carrying load — paideia K7 + +> *The ferry exists. The river bed exists. Now ride a barge +> across.* + +**Concrete:** paideia's K7 (`BootstrapGradient`) re-encoded as a +literal cubical `Path` between two `MasteryProvenance` traces. +Planned as REL2 Phase 3 in the `paideia` repo (5–10 days, +depends on engine REL2 Phase 1+2 landing). Closes engine +issue #1. + +**Why it matters:** K7 was the *originating use case* — the issue +that filed against the engine in the first place. REL1 gave us +inductive types; REL2 Phase 1 gave us interval; REL2 Phase 2 gave +us the bridge. REL2 Phase 3 is the day the system actually +carries load. The poetry was always there; this is when it +arrives. + +--- + +## 7. The wake — `Trace.lean` and `TraceAt.lean` + +> *Every passage leaves a wake. Looking at the wake, you can read +> who has been here, when, and on what business.* + +**Concrete:** `Topolei/Trace.lean` (root) and +`Topolei/Cubical/{Trace,TraceAt}.lean` (engine-side). +`Trace.traceOf` records every sub-CTerm that participated in a +computation; `TraceAt.traceOfAt` does so face-aware (only +sub-CTerms whose enclosing face is active at a given assignment). + +**Why it matters:** Provenance is first-class. When debugging, +profiling, or auditing a cubical computation, the wake is the +record. The face-aware variant (`traceOfAt`) prunes inactive +clauses, so the wake reflects only what *actually flowed* under a +particular set of conditions — the trace of the currents that +fired. + +--- + +## 8. Confluence — HITs and Glue + +> *Multiple flows merge at a confluence; from there, a single +> larger river continues.* + +**Concrete:** Higher inductive types via `CTypeSchema` with path +constructors (`s1Schema`, `intervalHitC`, `propTruncSchema`); Glue +types (`CType.glue φ T … A`) that present the same value via two +different equivalence-related forms. + +**Why it matters:** Confluence is where the cubical universe +exhibits its non-trivial structure. S¹'s `loop` is a path +between `base` and itself — the river is non-trivial precisely +because of how the flow folds back. Glue is where two type +formulations become one type with a coherence witness. Both +encode the same architectural insight: *equality is structure*, +and the structure of equality is what cubical type theory makes +visible. + +--- + +## 9. The map — `Dev_Algebra` and the universal macro + +> *Above the rivers, a map. It shows every current, every +> confluence, every ferry crossing. A finger on the map can +> trace any path; a click can re-route.* + +**Concrete (planned REL2.5):** `Dev_Algebra` branch with the +universal macro `restructure` (one universal `comp`-shaped +operation lifted to the meta-Lean-source level), the +`@[macroAlias]` attribute (aliases accrue by usage), the +`@[methodology]` attribute (proof fragments tagged by classifier), +the `cubical_search` autodiscovery tactic (walks the methodology +library; transports methodologies along declared structural Paths +to derive new candidates from old ones), and a widget that renders +the question-graph for point-and-click navigation. See +`ALGEBRA_PLAN.md` for the full plan. + +**Why it matters:** The map is the visible face of the system's +closure under its own operations. Cubical primitives (transport, +comp, Path, Glue, …) at the object level — meta-primitives +(restructure, MetaPath, MetaClassifier, methodology-transport, …) +at the Lean-source level — same universal `comp` shape at both +strata. The codebase becomes navigable because the navigation +tools are built from the same algebra as what they navigate. + +--- + +## 10. The current's autodiscovery — methodology transport + +> *Once the map is drawn, knowing one passage is knowing many: +> every connection on the map is a recipe for following the +> current somewhere new.* + +**Concrete (planned REL2.5):** The methodology-transport clause +inside `cubical_search`. When a structural Path is declared in the +codebase (e.g., "Bool ≃ {0, 1}", "List α ≃ Vec n α with n free"), +every existing methodology fragment registered for one side of the +path automatically becomes a candidate for the other side via +`transp` at the methodology level. Twenty starting methodologies ++ a hundred declared paths → potentially thousands of derived +methodologies, each formally certified-by-construction. + +**Why it matters:** This is *autodiscovery*: the proof-search +library grows under structural-Path declarations alone, with no +extra authoring. A new equivalence in the codebase is also a new +chunk of proof automation — for free. The cubical engine's own +transport is what powers the proof-search engine. The system has +become reflexive. + +--- + +## 11. The discipline (one-page summary) + +| Stratum | River bed | River | Current | Ferry | Wake | Map / autodiscovery | +|-----------------|--------------------------|--------------------|--------------------|-----------------------|-----------------------|---------------------| +| Cubical (object)| `CType.interval` | `Path`, `transp` | comp filler | (within calc) | `Trace` | (no map yet) | +| Question (Layer 1) | classifiers | `CompQ` | `q.ask` | `Bridge` | `traceOfAt` | question-graph | +| Meta (Layer 3) | `MetaCType` | `MetaPath` | `restructure` | `treat_as_*` macros | `Edit` log | widget + `cubical_search` | +| Tactic (Layer 5) | methodology library | tactic chains | `cubical_search` | `tactic_from_methodology` | tactic trace | methodology-transport | + +Each row is the *same architectural pattern* applied at a higher +stratum. Reading the columns top-to-bottom, you see the +metaphor's lifeline through the system: the river bed has a meta- +river-bed (`MetaCType`), which has a tactic-river-bed +(methodology library); the river has a meta-river (`MetaPath`), +which has a tactic-river (chained tactic invocations); and so on. + +The discipline is **one universal pattern, applied at every +stratum, with each instance named according to its register.** + +--- + +## 12. What this discipline buys + +1. **Architectural coherence under refactoring.** Any + re-organisation that respects the universal pattern at one + stratum trivially respects it at every other stratum. No + layer-specific surprises. +2. **Vocabulary for newcomers.** A new contributor (human or AI) + reading the codebase encounters one canonical question shape + six times, not six different patterns once each. The cognitive + cost of orientation drops dramatically. +3. **Proofs as first-class data.** Because every theorem reduces + to a chain of classifier-conditioned `CompQ` equivalences, + proofs are *navigable* (the question-graph), *factorable* (any + theorem decomposes into elementary moves), and *recomposable* + (any structurally-valid composition is itself a valid proof). +4. **Tooling closure.** The macro layer that organises proofs is + itself made of the same universal `comp` shape. Tools manage + themselves. No tool sits *above* the algebra; everything lives + *inside* it. +5. **Aesthetic consistency.** Every artifact in the codebase has + a clean place to live, named in vocabulary that fits the + metaphor. Code that looks clean *is* clean — the visible + surface and the underlying algebra agree. + +--- + +## 13. Where the metaphor strains (and what to do about it) + +No metaphor is perfect. Three known strain points: + +1. **`Glue` is more than confluence.** It's a *coherence-witnessed + refactor between two formulations* — closer to "two roads + sharing a bridge that records why they are equivalent." The + confluence image gets the geometry but loses the witness; if a + reader is confused, the long form is the way out. +2. **The interval is not really a river bed.** It's a *de Morgan + lattice*. The river-bed image is right for "the medium under + the flow" but loses the algebraic structure + (meet/join/inversion). Acceptable for documentation; not for + formal reasoning. +3. **Autodiscovery is not magic.** The methodology-transport + clause is bounded by declared structural Paths. A path you + haven't declared cannot transport methodologies along itself. + The "thousands of derived methodologies" claim is real but + conditional — bounded by the user's own Path declarations. + Future REL3+ AI-prior work may relax this; until then, the + autodiscovery is *pattern-mechanical*, not pattern-imaginative. + +These strains are recorded so future readers don't over-extend the +metaphor in ways the underlying algebra wouldn't support. + +--- + +## 14. References + +- `INDUCTIVE_TYPES.md` — REL1 design: schema-based inductives + HITs. +- `REL2_PLAN.md` — three-phase plan: interval, Bridge, K7. +- `QUESTIONS.md` — philosophy: questions as types, classifiers, + three commitment levels. +- `ALGEBRA_PLAN.md` — `Dev_Algebra` branch: universal macro, + attributes, autodiscovery tactic, widget. +- `KERNEL_BOUNDARY.md` — long-horizon scope contract: what the + embedding can and cannot do without kernel changes. +- `FFI_DESIGN.md` / `FFI_COMPLETENESS.md` — Rust kernel ABI + contract and per-function axiom audit. +- `NUMERICAL.md` — REL3-onward numerical layer (out of scope for + these documents but on the same metaphorical map). + +--- + +*End of EULERIAN.md. This document is the project's record of +its own architectural metaphor. Update when the system grows a +new layer that fits the discipline; remove an entry only when the +underlying construct retires.* diff --git a/docs/QUESTIONS.md b/docs/QUESTIONS.md new file mode 100644 index 0000000..996e5ba --- /dev/null +++ b/docs/QUESTIONS.md @@ -0,0 +1,316 @@ +# QUESTIONS.md — The Universal Question Form + +*Drafted 2026-04-30 on `Dev_REL2`. Captures the design philosophy +behind the project's question-as-data discipline — first surfaced +mid-REL2 as the substrate underlying both `Bridge.lean` and the +planned `Dev_Algebra` macro layer. Companion to `REL2_PLAN.md` +(implementation) and `EULERIAN.md` (poetic register).* + +--- + +## 0. The motivation, in one paragraph + +In the discrete-math world, a clean Lean 4 file like +`differential_equations.lean` *first* defines a vocabulary of +question-shapes (`IsExact`, `IsBernoulli`, `IsHomogeneous`, …) as +predicates over the data of an ODE, and *then* states each problem +as a theorem whose **type** encodes the question. Solutions follow. +The crucial move is that questions are first-class types: you can +compare them, equivalence-class them, prove implications between +them, even before you answer any. + +The same discipline applies, with surprising force, to cubical type +theory — because cubical type theory has a **single canonical +universal question form**, and we already have the engine that +answers every instance of it. + +--- + +## 1. The universal question form + +> **Given a type-line `A(i)` along a dimension binder `i`, a face +> formula `φ`, a partial element `u : A` defined on `φ`, and a base +> `t : A(0)`, find a total element `v : A(1)` agreeing with `u` on +> `φ` and with `t` at `i = 0`.** + +This is the **partial-element-filler problem** (CCHM §3, §5). Its +universal answer is the cubical `comp` operator: + +``` +comp i A φ u t : A(1) +``` + +Every cubical operation we have is a specialisation of this +universal question: + +| Operation | Specialisation of `comp` | +|-------------------|---------------------------------------------------------------------| +| `transp i A φ t` | `comp i A φ t t` — base equals partial element (no side condition) | +| `hcomp A φ u t` | `comp i A φ u t` with `A` constant in `i` | +| `compN` | `comp` with a multi-clause partial element | +| Path β / η | `comp` instantiated at `Path` types with appropriate boundaries | +| Glue β / η | `comp` instantiated at `Glue` types with the equivalence's filler | +| Univalence | `comp` over `uaLine` evaluating an equivalence at an endpoint | + +Transport is the **degenerate** question: "extend `t` along `A(i)` +with no side constraints." All others add structure (a non-trivial +partial element on a non-trivial face) without changing the question +shape. The question is universal; only its parameters vary. + +--- + +## 2. Reifying the question as data + +The shape of `comp` becomes a Lean record: + +```lean +namespace Question + +structure CompQ where + env : CEnv + binder : DimVar + body : CType -- A(i) — the type-line + φ : FaceFormula -- where u lives + u : CTerm -- partial element on φ + t : CTerm -- base at i=0 + +/-- "Asking" a question runs the engine. -/ +def CompQ.ask (q : CompQ) : CVal := + vCompAtTerm q.env q.binder q.body q.φ q.u q.t + +/-- Two questions are equivalent if their answers coincide. -/ +def CompQ.Equiv (q₁ q₂ : CompQ) : Prop := + q₁.ask = q₂.ask + +/-- Subsumption: q₁ ≤ q₂ when q₂'s answer specialises to q₁'s. -/ +def CompQ.Refines (q₁ q₂ : CompQ) : Prop := … + +end Question +``` + +Transport is a derived shape: + +```lean +def TranspQ.toCompQ (env : CEnv) (i : DimVar) (A : CType) + (φ : FaceFormula) (t : CTerm) : CompQ := + { env := env, binder := i, body := A, φ := φ, u := t, t := t } +``` + +Equivalences, derivations, and witnesses become **morphisms** in the +implicit category of `CompQ` values. + +--- + +## 3. Classifiers — the meta-vocabulary of question shapes + +Mirroring `ODE.IsExact`, `ODE.IsBernoulli`, …, every cubical question +admits classifying predicates that pin its specific shape: + +```lean +namespace Question + +/-- The line is constant in its binder — transport / comp is identity + on the body. -/ +def IsConstLine (q : CompQ) : Prop := + q.body.dimAbsent q.binder = true + +/-- The face is the full face — partial element covers the whole + space. -/ +def IsFullFace (q : CompQ) : Prop := q.φ = .top + +/-- The face is the empty face — only the base contributes. -/ +def IsEmptyFace (q : CompQ) : Prop := q.φ = .bot + +/-- The base equals the partial element — this is a transport, not + a heterogeneous comp. -/ +def IsTransport (q : CompQ) : Prop := q.u = q.t + +/-- The line is a Path type — Path-specific reductions apply. -/ +def IsPathLine (q : CompQ) : Prop := + ∃ A₀ a b, q.body = .path A₀ a b + +/-- The line is a Glue type — Glue-specific reductions apply. -/ +def IsGlueLine (q : CompQ) : Prop := + ∃ ψ T f fInv s r c A, + q.body = .glue ψ T f fInv s r c A + +/-- The line is a Π type — CCHM Π reductions apply. -/ +def IsPiLine (q : CompQ) : Prop := + ∃ domA codA, q.body = .pi domA codA + +/-- The line is a schema-defined inductive — REL1 reductions apply. -/ +def IsIndLine (q : CompQ) : Prop := + ∃ S params, q.body = .ind S params + +/-- The line is the cubical interval — REL2 transport-on-𝕀 is + identity. -/ +def IsIntervalLine (q : CompQ) : Prop := + q.body = .interval + +end Question +``` + +Every existing reduction axiom in the codebase becomes a **theorem +about classifier-conditioned question equivalence**: + +```lean +-- eval_transp_top, today an axiom-side lemma: +-- eval env (.transp i A .top t) = eval env t +-- +-- becomes the question-equivalence theorem: +theorem CompQ.full_face_is_identity + (q : CompQ) (h : IsFullFace q) : + q.Equiv (CompQ.identity q.env q.t) + +-- eval_transp_const: +theorem CompQ.const_line_is_identity + (q : CompQ) (h₁ : IsConstLine q) (h₂ : IsTransport q) : + q.Equiv (CompQ.identity q.env q.t) + +-- eval_transp_pi (the full CCHM Π rule): +theorem CompQ.pi_line_is_vTranspFun + (q : CompQ) (h : IsPiLine q) (hT : IsTransport q) + (hφ : ¬ IsFullFace q) (hC : ¬ IsConstLine q) : + q.Equiv (CompQ.viaTranspFun …) +``` + +Each theorem is *one move in the question algebra*: applying a +classifier rewrites the question to a simpler one, in a way that +runs through `q.Equiv` and so chains under composition. + +--- + +## 4. Three levels of commitment + +The question discipline supports three escalating levels: + +### 4.1 Level 1 — Structural reification only + +Define `CompQ`, `ask`, `Equiv`, classifiers. Restate existing +axioms / theorems as classifier-conditioned equivalences. Existing +runtime / soundness behaviour unchanged. + +**Cost:** ~1–2 days. + +**Benefit:** a uniform vocabulary; new theorems are naturally stated +in question form; old theorems become derived corollaries. + +### 4.2 Level 2 — Routing through questions + +Every axiom and theorem in `Eval` / `TransportLaws` / `CompLaws` / +`Glue` re-stated in question shape. A `simp`-set rewrites question +equivalences. Call sites continue to work via `q.ask = …` lemmas. + +**Cost:** ~3–5 days on top of Level 1. + +**Benefit:** *question algebra* — compose, decompose, refine +mechanically. Refactors (rename a classifier, factor a question, +merge two questions into a join) become text-level operations that +preserve correctness. + +### 4.3 Level 3 — Question-driven proofs + +Proofs are *question reductions*: "this `CompQ` reduces to that +`CompQ`, which is identity by `IsConstLine`." A `cubical_simp` +tactic knows the reduction graph and finds reduction chains +automatically. + +**Cost:** ~10+ days on top of Level 2; co-equal with REL2 in scope. +Depends on a `cubical_simp` tactic +(KERNEL_BOUNDARY.md §3.7). + +**Benefit:** proofs become navigable graphs of classifier +applications; the engine essentially proves cubical-core theorems +automatically. + +--- + +## 5. The connection to `comp` lifted to the meta-level + +The deepest insight: **the same question-form algebra also describes +the macro layer that organises the codebase itself.** See +`ALGEBRA_PLAN.md` for the full plan; the headline: + +A meta-restructuring operation has signature + +``` +restructure + (i : MetaPosition) -- where in the source + (Context : MetaCType) -- what kind of artifact + (φ : MetaClassifier) -- when this restructuring applies + (witness : MetaArtifact) -- new content valid on φ + (fallback : MetaArtifact) -- existing content off-φ +``` + +— exactly the same five-field shape as `comp i A φ u t`, with each +field promoted from "cubical CTerm" to "structural Lean artifact." +The macro layer is `comp` reflecting itself one level up. + +Concretely, the **autodiscovery tactic `cubical_search`** is +`restructure` whose `(witness, fallback)` is computed by search over +a methodology library, with new methodologies derived automatically +from old ones via *transport along structural Paths in the +codebase* — `transp` lifted to the methodology level. + +The whole design discipline collapses to: **one universal question +form, used at three levels (cubical / question / meta), each level +the reflection of the level below.** + +--- + +## 6. Why this matters for downstream consumers + +### 6.1 Internal: cubical-core proofs + +Every existing axiom + theorem in the cubical engine +(`eval_transp_*`, `eval_comp_*`, the 9 Glue-transport face-disjoint +variants, `transp_ua`, `glue_beta`, …) is a **classifier-conditioned +question-equivalence**. Pulling them through `CompQ.Equiv` makes +the dependency graph visible: which classifiers chain to which +others, which questions are foundational vs. derived, where the +axiom-discharge load actually concentrates. + +### 6.2 External: paideia / topolei + +`Bridge.lean` already provides the `Eq ↔ Path` ferry between Lean's +`Eq` world and the cubical `Path` world. In the question-form +discipline, `Bridge`'s instances become **classifier libraries** — +"a question whose body is the Bool-schema-CType is answerable via +this discrete-equality chain." Future paideia / topolei / +cells-spec consumers register their own classifier libraries; the +core engine doesn't grow new code. + +### 6.3 Tooling: code actions, tactics, search + +A code action in the editor (REL2.5+ `Dev_Algebra`) operates on +`CompQ` values: "factor this question into two simpler ones," +"rename this classifier across all dependents," "transport this +methodology along that path." Every action is a typed operation in +the question algebra, and the tooling never has to special-case +arbitrary tactic scripts. + +--- + +## 7. Open questions (logged here, not blocking) + +1. **Schema for question-graph storage.** In-memory (computed each + LSP session) vs. persisted as Lean attributes (`@[question Foo]`, + `@[classifier IsConstLine]`) — REL2.5 design decision. +2. **Higher questions.** Equivalences between + classifier-equivalences (paths between paths) — natural to want; + probably out of scope until cells-spec §8 (n-cells). +3. **Question algebra completeness.** Is every cubical theorem + provable as a chain of classifier-conditioned equivalences? We + conjecture yes for the core axiom set; verifying is part of + Level 3 work. +4. **`Decide`-checkable classifiers.** Most classifiers are + syntactic (`q.φ = .top`, `q.body.dimAbsent q.binder = true`) and + thus `Decidable`. Some (`IsPathLine`, etc.) involve + existentials; need explicit `DecidableEq` / inversion lemmas. + Tracked in REL2.5 OQ list. + +--- + +*End of QUESTIONS.md. Companion to `REL2_PLAN.md` (Phase plan), +`ALGEBRA_PLAN.md` (macro / dev-branch design), and `EULERIAN.md` +(poetic record).*