All subsystem theories follow Laurent Lafforgue's geometric theory framework:
- Vocabulary (Σ): Sorts, function symbols, relation symbols
- Theory (T): Geometric sequents (axioms) — antecedents use only ∃, ∧ (no ¬, ∀, →)
- Model (M): Runtime session state implementing the theory
- Extractor (f): Morphism
f: E_T → E_Tctxextracting a context string (~256 char budget)
Per Lafforgue §2.1, axiom antecedents must be positive — only existential quantification (∃) and conjunction (∧). No negation (¬), universal quantification (∀), or implication (→) in antecedents.
This is enforced throughout the codebase. Example (PATCH_4):
# WRONG (negation in antecedent):
¬GlobalCoherent(pt) ⊢ Obstruction
# CORRECT (positive witness):
ObstructionWitness(pt) ∧ InterferenceHigh(pt) ⊢ Obstruction
Package: mneme/
| Sort | Description |
|---|---|
| NODE | Memory node |
| TURN | Conversation turn index |
| TOPIC | Topic label |
| LEVEL | Compression level |
| PAYLOAD | Content at each compression level |
| QUERY | Retrieval query |
| CONTEXT | Extracted context |
| SCORE | Salience/retrieval count |
| FLAG | Node flags (pinned, savant, boundary) |
L0_VERBATIM → L1_SUMMARY → L2_GIST → L3_TAG
Forgetting = movement toward coarser description, never deletion.
Pinned(n) ⊢ Stored(n)— pinned nodes always storedSavantLock(n) ⊢ Stored(n)— savant-locked never compressedBoundary(n) ⊢ Stored(n)— topic boundaries preserved
E_mem = [C_time_topic^op, Set] — presheaf over time×topic category with sheaf condition.
Package: calibration/
9 sorts, 6 function symbols, 5 relation symbols.
| Fiber | Range | Description |
|---|---|---|
| temperature | 0–2 | LLM sampling temperature |
| topP | 0.01–1 | Nucleus sampling |
| maxTokens | 16–4096 | Max generation tokens |
| dmnInterval | 2000–30000ms | DMN tick interval |
| κBudget | 32–2048 | Energy budget |
| regenRate | 0.1–10 | κ regeneration rate |
| tickRate | 10–1000ms | Tape tick rate |
| cyclePeriod | 100–50000 | Angular indexing period |
| fusionα | 0–1 | Dense/sparse fusion |
UNIFORM → SPECIALIZING → SPECIALIZED → EVOLVING → SATURATED
16-entry ring buffer tracking calibration vector changes.
Package: mltm/
8 sorts, 6 function symbols, 7 relation symbols.
The MLTM is an octuple (Q, Σ, Γ, δ₀, q₀, F, Φ, C) where Φ is a mutation oracle and the Literary Acceptance Problem (LAP) is NP-complete.
| # | Name | Sequent |
|---|---|---|
| 3 | obstruction_witness | ObstructionWitness(pt) ∧ InterferenceHigh(pt) ⊢ Obstruction |
| 4 | witness_np_member | Witness(π) ∧ PolyCertified(π) ⊢ NPWitnessed |
InterpretationPoint: snapshot with fibers, holonomy, Kolmogorov estimateisPolyCertified: Boolean— positive flag replacing arithmetic inequalitywitnessStepCostEstimate: Float— NP witness cost
Package: pipeline/
19 sorts, 7 function symbols, 10 relation symbols.
ING → EMB → LOC → CHR → SEM → INF → GLU → STA → JUS → CHK
CMT ⊕ BLK ⊕ RLB (total partition — every inference terminates in exactly one)
- CMT (Commit): successful inference
- BLK (Block): blocked by obstruction
- RLB (Rollback): reverted due to inconsistency
- σ vector: 6 invariants (2 OPEN:
gluing_sound,fixed_point_strict) - κ vector: energy/token/depth bounds
- π: Proof-of-execution bundle (replayable witness)
Package: hott/
10 sorts, 6 function symbols, 7 relation symbols.
DISCRETE → FIBRATING → FLOWING → CONTRACTING → AUTOPOIETIC
- Paths = reasoning traces (identity type between states)
- Horns = Kan horn gaps (missing data in simplicial structure)
- Fibers = subsystem sections (§0-§9 as fibration fibers)
- Univalence: identity ≃ equivalence
- Autopoietic: self-authored axioms (the system writes its own rules)
pathCoherence > 0.6 ∧ hornFill > 0.7 ∧ UA > 0.5
Activation: §10|AWAKE
Package: trasgo/
10 sorts: Morphism, Fibration, Retraction, Witness, Collapse.
The geometric sequents encode the syntactic constraints of the TRASGO meta-language — fibration tracking, σ retraction, and witness/collapse dynamics.
Package: reservoir/
10 sorts (ESN dynamics over token stream).
- Echo State Property: spectral radius < 1
- Fading Memory: past inputs decay exponentially
- Lyapunov Stability: bounded divergence of nearby trajectories
Gray-Scott reaction-diffusion over a 1D ring topology:
∂U/∂t = D_u ∇²U - UV² + F(1-U)
∂V/∂t = D_v ∇²V + UV² - (F+k)V
Maintains standing wave patterns even when the token stream pauses.
Routes §N|OP patterns via 6 strategies: DIRECT, MULTIPLEX, THREAD, QFMA, BROADCAST, DIFFUSE.
Package: society/
| Sort | Description |
|---|---|
| BeeRole | QUEEN, WORKER, SCOUT, NURSE |
| PheromoneType | ALARM, TRAIL, BROOD, QUEEN_SUBSTANCE |
| Bee | Individual agent in the hive |
| HiveTask | Task assignment |
| PheromoneField | Chemical signaling field |
QueenImmortal: Queen bee cannot dieEnergyDeath: Bee with 0 energy dies- Max 16 bees, Greek identifiers α-θ
ToposSociety.kt — §9|SOCIETY: N agents with inter-topos morphisms.
Package: lisp/
8 sorts, 8 geometric sequents.
- β-progress: β-redex always reduces
- Y-fixed: Y-combinator reaches fixed point
- Curvature-bound: reduction cost bounded by hyperbolic curvature
See Lisp & Lambda Calculus for engine details.