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.