> For the complete documentation index, see [llms.txt](https://docs.nexus.xyz/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.nexus.xyz/math-engine/engine.md). # The Engine, Formally The corpus you are reading is produced by a machine. This page documents and formalizes that machine: its AI actors, its pipeline, what each stage guarantees, and — just as important — what is *not* yet verified. ## The engine as a composition Let $$\Sigma$$ be the Exchange's source code (the ground truth) and $$\mathcal{M}$$ the space of structured mathematical models. The corpus is the image of the source under a composition of maps: $$ \mathcal{C} ;=; R \circ P \circ J \circ G,(\Sigma) $$ * $$G$$ **— the Generator** (LLM): per system, $$G\_k : \Sigma\_k \to M\_k$$ reads the Rust source and derives a structured model — expressions with LaTeX and an *executable* Python form, typed domains and units, test vectors extracted from the code's own tests, chart and figure specifications. $$G$$ runs under two locks that stabilize re-derivation: the corpus-wide **notation lock** and the **prior-model baseline**. * $$J$$ **— the Judge** (LLM, adversarial): $$J\_k : (M\_k, \Sigma\_k) \to$$ verdicts. Its only goal is to *refute* the Generator — formula vs. cited code, rounding semantics, edge regimes — and to extract further test vectors. Vectors merge only if they pass numeric evaluation; a refutation trumps passing vectors. The Judge has caught two real derivation bugs to date (the partial-liquidation full-close branch; the settlement merge summation). * $$P$$ **— the composition passes** (LLM): the relationship graph $$P\_{\text{sys}} : {M\_k} \to \mathcal{G}$$, the global state-space model $$P\_{\text{glob}} : ({M\_k}, \mathcal{G}) \to M\_\ast$$ (rendered as the Exchange Engine and the closed loop), the **state-space classifier** $$P\_{\text{ss}} : {M\_k} \to \mathcal{S}$$ (v0.0.9: every corpus quantity classified state / input / parameter / derived; the full hierarchical state vector; the completed event alphabet — rendered as the formal appendix, its totality enforced mechanically), and the specification passes for surfaces, structural figures, and the analytical performance model. These run strictly *after* $$G$$ and $$J$$ — the composition reads verified inputs. * $$R$$ **— the renderers** (mechanical, no LLM): deterministic Markdown with numbered equations and resolved citations, 1-D response curves, sensitivity elasticities, 2-D surfaces and regime maps, lane diagrams, performance fits. Models are the single source of truth; $$R$$ never adds content. Gates sit between the stages: source-hash **staleness**, numeric **test vectors** (every expression must carry passing vectors), **dimensional analysis** (units balance, ast-checked), the **notation** and **coherence** gates (one symbol → one quantity → one dimension; duplicated quantities agree numerically), and since v0.0.9 the **closure gate** — the completeness of the formal appendix as a checked property: no orphan expressions, every state coordinate written by an event and read somewhere, every event map citing only defined coordinates. A corpus release is an immutable snapshot of $$\mathcal{C}$$ with a semantic changelog. The residue that survives every adversarial pass without being attributable to a modeling error exits the pipeline as a **design finding** — the engine's second product, alongside the corpus itself. ## What each stage guarantees — and what it does not | Layer | Verified by | Status | | ------------------------------ | --------------------------------------------------------------------------- | ----------------------- | | Expression ↔ code | Judge (adversarial) + vectors + dims | strong | | Re-derivation stability | notation lock + baseline + semantic differ | strong | | Cross-model coherence | coherence gate (numeric agreement of duplicated quantities) + notation gate | strong | | Graph / global / closed loop | composition Judge (adversarial) + reconciliation audit | strong | | System-wide invariants | property-tested (simulator, 512 trials each) or Judge-ruled if structural | strong\* | | Completeness of the definition | closure gate over the state-space classification (mechanical) | strong — v0.0.9 | | Design quality (vs. peers) | not evaluated | v0.0.10 (Market Critic) | \*with an honest caveat: the composition Judge *refuted* both closed-loop invariants as originally stated, and the corpus now states them **conditionally** — the equity-shock bound covers the anchor leg on non-re-anchor prints, and staleness fail-closed holds only with the trade-reference leg frozen and settlement suspended, assumptions no component expression yet witnesses. The unresolved residue was not hidden inside a weaker claim: it became the first entries of the findings log, the engine's channel for design-level observations that belong to engineering rather than to the corpus. Since v0.0.8 the composition layer is no longer trusting: components still derive in parallel, but a coherence gate checks their duplicated quantities numerically, a composition Judge attacks the graph and global model, an invariant simulator property-tests every numeric claim, and a final reconciliation audit closes each cycle — its directives (and any new design findings) feed the next one. ## Actor configuration All actors run headless against a single pinned large language model and a fixed, versioned prompt per actor, and every run is recorded with its model, duration, token usage, and cost. * **Model**: every run to date has executed on the same pinned model. Effort has been pinned at the highest tier since v0.0.8. * **Prompts**: each actor's full prompt is versioned with the engine, so every corpus release is attributable to an exact prompt + model pair via the engine's own history. ## The trust loop, end to end $$ \Sigma \xrightarrow{;G;} M \xrightarrow{;J;} M^{\checkmark} \xrightarrow{;P;} (\mathcal{G}, M\_\ast) \xrightarrow{;R;} \text{docs, charts, figures} \xrightarrow{;\text{gates};} \text{release } v\_n $$ A source change breaks the staleness gate → re-derivation under the locks → the Judge re-verifies → the semantic differ writes the changelog: only real mathematical change is flagged; renames and refactors are recognized as equivalent. The reader-facing promise is that every equation on this site is (1) pinned to the exact source it describes, (2) numerically tested against that source's own test suite plus adversarially extracted vectors, and (3) dimensionally consistent — with the composition layers explicitly labeled as the current frontier of verification. ## References * Derived from and adversarially verified against the Exchange's Rust implementation and its test suite. --- # Agent Instructions This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com. ## Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter, and the optional `goal` query parameter: ``` GET https://docs.nexus.xyz/math-engine/engine.md?ask=&goal= ``` `ask` is the immediate question: it should be specific, self-contained, and written in natural language. `goal` is optional and describes the broader end goal you are ultimately trying to accomplish on behalf of the user. GitBook uses it to tailor the answer towards what is most useful for that goal. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.