Document the question-form algebra + Dev_Algebra plan + Eulerian record
Some checks are pending
Lean Action CI / build (push) Waiting to run
Some checks are pending
Lean Action CI / build (push) Waiting to run
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) <noreply@anthropic.com>
This commit is contained in:
Maximus Gorog
parent
7152807b66
commit
95f11020d7
3 changed files with 1129 additions and 0 deletions
484
docs/ALGEBRA_PLAN.md
Normal file
484
docs/ALGEBRA_PLAN.md
Normal file
|
|
@ -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).*
|
||||
329
docs/EULERIAN.md
Normal file
329
docs/EULERIAN.md
Normal file
|
|
@ -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.*
|
||||
316
docs/QUESTIONS.md
Normal file
316
docs/QUESTIONS.md
Normal file
|
|
@ -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).*
|
||||
Loading…
Add table
Reference in a new issue