Mathematics needs metabolism, not more storage. MathGraph is a generative verification kernel: claims enter, constructors propose lawful continuations, verifiers decide, certificates are promoted, and the lawbook remembers.
Every accepted claim must collapse into one terminal form:
VERIFIED_PROOF, FINITE_COUNTERMODEL, or NAMED_OBSTRUCTION. In the public
language, a finite countermodel is the first concrete refutation certificate.
Models propose. MathGraph constrains. Verifiers decide. Reasons compress. Scheduler scores, route cards, root pressure, and advisory output are search pressure only; they are not truth.
A certificate is the atom of verification. A root node is the atom of discovery. A reason node is the atom of understanding. An obstruction is a named residual that makes the next constructor sharper.
The compounding architecture is:
Claim -> Normalize -> Route -> Construct -> Verify -> Promote -> Lawbook
-> Derived Closure -> Outcome Dataset -> Route Pressure -> Residual Split
The Certificate Universe records survivor certificates. The Obstruction Atlas names failures. The Root Node Atlas identifies load-bearing motifs. The Reason Atlas compresses why those motifs matter. H-tilt is proposal pressure, not mathematical authority.
LOGOS middleware means a model can propose, but the verifier boundary decides. MathGraph is the bridge between generative imagination and lawful continuation.
Typed predication gives MathGraph a safer metaphysical grammar: encoding is not exemplification, denotation matters, semantic embeddings carry artifact risk, and same extension is not same law. Formal worlds are context boundaries, not proof objects.
The formal workbench adds engineering memory around those worlds: embedding strategies, faithfulness assessments, backend profiles, benchmarks, correspondence claims, and interpretation choices. It makes bridge risk visible without pretending that metadata is proof.
The proof motif atlas does the same for TRUE-side proof discovery: motifs, proof roots, and lemma candidates shape the next cut, but Lean or another verifier must validate the theorem before it becomes authority.
Near term: root-aware oracle advice, reason compression, richer objectification, workbench-aware verifier routing, and finite-countermodel constructor improvement. Later: Lean/Isabelle proof importers, domain-agnostic claims, and spectral H-tilt.