MathGraph's first agentic layer is deliberately small. It records discovery pressure without changing the verifier boundary:
Chora -> AlchemicalTrace -> AgentExperience -> H-tilt-lite pressure
-> Verifier boundary -> Terminal Form -> Lawbook -> Projection
Models propose. MathGraph constrains. Verifiers decide. Digestion assimilates. The Lawbook remembers. Projection scales.
The current loop now includes continuation actions, curricula, verification episodes, proof digestion, verifier feedback and repair, discovery value, Lawbook acceptance and query, structural identity, habit rules, reason compression, process memory, structure registry and typed projection, role-based object introduction, structural analogy/exposition, formal-world adapters, proof-system integration, semantic intake, and the API service. These layers may improve search, replay, understanding, and scheduling, but they remain advisory unless an explicit truth boundary is crossed.
Existential agents are explorers inside MathGraph, not truth authorities. Their finite resources, scars, wounds, values, narratives, lineage, and death shape route pressure and scheduling only. Public verified artifacts survive agent death. Private unresolved biography may be sealed, summarized, or burned. The kernel remains audit-stable; agents may be mortal.
Hardening is the discipline that tests whether the metabolism remains safe under replay. It checks that every advisory layer stays advisory, that docs match implementation, that API responses carry boundary fields, that agents remain mortal, and that no smoke run becomes a proof.
The recurring ordeal can now run from a fresh clone without manual PYTHONPATH
setup: public scripts bootstrap the repository root, and the read-only
Colab/local test drive replays the verifier, corpus, project, hardening, and
alignment path while leaving truth promotion to the same explicit boundaries.
Mathlib micro-subset ingestion is the first rehearsal for proof-library scale. It treats a proof library as structured memory only after the verifier or trusted-import boundary, while declarations and dependency graphs remain advisory.
The API service is the outer membrane of MathGraph. It lets clients submit text, query accepted memory, request advisory routing, and inspect audit state while preserving the verifier boundary. Every response says whether it is advisory, accepted memory, or backed by already-existing boundary evidence. The service may route work, but it may not create truth.
The operational loop is:
H-tilt selects.
Alchemy transforms.
LOGOS constrains.
Verifiers decide.
Lawbook remembers.
Projection scales.
Biography updates.
AlchemicalTrace records staged transformation, not truth. Its phases are raw
matter, calcination, solution, sublimation, descension, distillation,
coagulation, fixation, ceration, conjunction, multiplication, projection, and
perfection.
Fixation is still advisory unless a verifier/importer promotes a certificate. A trace crosses the verifier boundary only when it has:
- a terminal form in
VERIFIED_PROOF,FINITE_COUNTERMODEL, orNAMED_OBSTRUCTION; - a non-empty promoted certificate id;
- at least one step marked
PROMOTED_BY_VERIFIER.
Finite-search failure is not proof. It may produce residual structure, scars, obstruction pressure, or future route pressure, but it does not establish a theorem.
Agents are lightweight persistent policies with memory. They are not chatbot
personas and not autonomous LLM loops. AgentProfile, AgentExperience, and
AgentBiography store route preferences, taste weights, costs, scars,
compression gains, projection gains, and derived amplification.
Taste updates are deterministic advisory pressure. They can change future scheduling, but cannot change terminal truth.
H-tilt-lite is viability-conditioned advisory pressure. It combines base route
score, agent taste, scar penalty, expected cost, expected projection gain, and
expected compression gain. Spectral H-tilt adds telemetry-derived killed
dynamics through K = L - V, h, q, and pi*; both remain scheduling
pressure rather than truth.
H-tilt-lite does not promote claims. It only helps decide what to try next.
RoadmapAlignmentReport checks traces, experiences, and summary metrics for
doctrine drift:
- advisory objects must not claim terminal truth;
- terminal forms require verifier promotion;
- finite-search misses must not become proofs;
- route scores, H-tilt scores, roots, motifs, plans, scars, and narratives stay advisory;
- residual compression, projection, derived amplification, and scars should be recorded when available.
Projection is the bridge from Lawbook to smaller residual. It applies fixed lawbook artifacts and chain-safe derived certificate rules back onto unresolved pairs, producing known skips, derived certificate results, residual splits, obstruction pressure, and scheduling pressure.
Projection scales verified memory into future search, but projection itself is not truth. A projection result crosses the truth boundary only when it is backed by an existing verifier/importer boundary, an already verified primitive certificate, or an explicitly chain-audited derived certificate id.
Advisory similarity, basin expansion, constructor replay pressure, and residual splits remain Chora-facing pressure until LOGOS and a verifier/importer make them lawful.
Root signals are SAT/UNSAT boundary pressure. They mark where residual basins, obstruction surfaces, motifs, or projection hints suggest a narrow continuation may be worth trying.
Constructor plans descend root pressure into concrete attempts. This is the descension phase: a basin-shaped idea becomes a bounded finite-table attempt or a dry-run record. The plan is still advisory.
Candidate artifacts must be distilled and fixed before entering the Lawbook. A candidate finite table is only a candidate until an importer/revalidator checks that the source holds and the target fails, records the witness, and promotes a finite-countermodel certificate.
Failed attempts should become named obstruction pressure or sharper residuals. A search miss is never a TRUE proof; it only says that a bounded attempt did not find a countermodel.
Proof motifs sublime: repeated proof patterns rise from traces as advisory structure. Lemma candidates, cut candidates, and theorem schemas are still pressure, not law.
Lean skeletons descend: a motif or candidate can become a concrete file or skeleton artifact, but syntax is not verification.
Verifier execution distills: Lean, another verifier, a trusted importer, or a chain auditor may check the artifact. Failures become residual proof pressure. Not-run results stay advisory.
Verified proof fixes: only a passed verifier, verified import, or explicit
chain-safe audit with certificate id can produce VERIFIED_PROOF.
Theorem schemas cerate: usable proof shapes become reusable material only after their boundary status is clear. Projection applies verified proof back to residuals; unverified skeletons produce only advisory projection pressure.
The unified episode loop is:
claim enters
route selected
projection checks lawbook
root constructors attempt FALSE-side descent
proof verification attempts TRUE-side descent
alchemy records phases
agent biography records experience
alignment checker protects boundary
lawbook/projection receives terminal artifacts only
Episode routing is telemetry, not truth. The episode becomes terminal only when a subtrace already crossed a verifier/importer/chain-audit boundary with a certificate id. Candidate tables, proof skeletons, search misses, route scores, and H-tilt-lite decisions remain advisory.
Episode traces become route telemetry. A telemetry event records the route kind, outcome, transition, kill state, cost, residual delta, compression gain, projection gain, support weight, and survival weight observed during a run.
Route telemetry records transitions and kills:
- transitions approximate the future
Ltransition structure; - killed route events approximate future
Vkilling pressure; - cost/gain summaries estimate where route pressure compounds;
- route scores remain advisory scheduling pressure.
Telemetry feeds future H-tilt, but it is not full spectral H-tilt. Full spectral
H-tilt remains future work until L, V, K = L - V, h, q, and pi* are
explicitly estimated. Telemetry cannot promote claims across the verifier
boundary.
Route telemetry now estimates L and V: L records observed continuation
transitions, while V records killing pressure from failed, rejected, missed,
or alignment-failed route events.
K = L - V gives killed continuation pressure. A lightweight positive
iteration estimates h as forward survival amplitude and q as structural
support. Their product gives pi*, an advisory survivor distribution, and
mu_beta gives the multiplicative H-tilt bridge used for scheduling pressure.
All of these remain advisory until some actual artifact crosses a verifier, importer, or chain-audit boundary. H-tilt can rank where MathGraph looks next; it cannot decide what is true.
Chora receives raw claims from many worlds: magma equations, Lean-looking
theorems, program properties, scientific hypotheses, semantic assertions, and
ordinary language. DomainClaim IR calcines raw claims into routable structure
when a conservative parser can do so.
The FormalWorld registry records what can be parsed, normalized, routed, or
eventually verified. Magma equational claims can descend into existing episode
inputs; Lean-looking theorem statements can descend into proof skeletons.
Natural-language and unsupported worlds remain advisory/residual.
LOGOS still requires a verifier boundary before truth. Parsing, normalization,
world selection, and semantic resemblance do not create VERIFIED_PROOF,
FINITE_COUNTERMODEL, or NAMED_OBSTRUCTION.
Lean skeletons descend into Lean files. The adapter records imports, theorem names, file content, local environment availability, and the exact command that would be run without using a shell.
Lean checks distill proof artifacts. When Lean is available, a file can be
checked through the proof verification boundary. Passed Lean checks or trusted
imports may fix VERIFIED_PROOF only when a certificate id and verifier
boundary are recorded.
Proof-system integration is where adapter-ready tasks become auditable project artifacts and check requests. It records theorem files, import graphs, safe command contracts, parsed check results, and trusted imports, but it only crosses the truth boundary when explicit boundary evidence exists. A file, import graph, check request, or proof-looking text may guide repair and digestion without becoming verification.
Semantic intake is the front door from human language into MathGraph. It turns informal text into segmented claims, ambiguity records, extraction records, formalization requests, routing hints, and tasks. It never crosses the truth boundary; it exists to prevent informal language from slipping into the Lawbook as proof.
Failed or unavailable Lean checks remain residual/advisory. A theorem name, parseable file, or generated skeleton is not truth.
Continuation actions generate candidate next moves. They are Chora outputs until constrained by LOGOS: possible implications, equivalences, duals, proof tasks, countermodel tasks, projection tasks, and obstruction names.
Proof, countermodel, and projection tasks must descend into the existing verifier-bound episode machinery before they can matter as terminal artifacts. Action output is not Lawbook memory until it is verified, refuted, or named through an explicit boundary.
Proof generation and proof verification are not the end. Verified artifacts must be digested into reusable mathematical memory before they can meaningfully improve future search, projection, and explanation.
Digestion distills dependencies, separates routine and load-bearing steps, extracts key idea and reusable schema candidates, creates exposition notes, and emits projection hints. Digestion and exposition are human-understanding layers. The Lawbook should store truth artifacts and digestion links separately: a proof certificate records survival through a verifier boundary, while digestion records compressed intelligibility around that survival.
Failed verification is not dead output. It becomes repair pressure, obstruction pressure, or residual structure. Minor flaws may be locally revised; structural gaps should reroute or emit new proof tasks; critical invalidations should become obstruction or residual candidates.
Repair traces remain advisory until a repaired artifact crosses a verifier, importer, or chain-audit boundary. A repair hint is not proof, a failed proof is not a countermodel, and a failed finite search is not a proof of TRUE.
A difficult continuation should not be attacked all at once. Curriculum building creates staged descent:
target -> warmups -> simplified cases -> finite examples
-> proof/countermodel tasks -> episode inputs
This gives agents and route policies a lawful ladder without corrupting truth. Curriculum stages remain advisory until their artifacts cross verifier boundaries.
Discovery value is the taste layer over the existing loop. It ranks what to try next using certificate potential, proof potential, countermodel potential, obstruction potential, digestion value, projection value, repair value, route survival, residual compression, root-likeness, cost, risk, and overfit penalties.
Value is not truth. A high-value continuation still needs a verifier boundary.
The Lawbook is the public-memory boundary:
candidate -> reviewed entry -> accepted entry -> projection rule
Certificates, proof digestion traces, lawbook assimilation candidates, projection candidates, and discovery value scores may recommend memory. They do not create it. The Lawbook remembers only what has been accepted under explicit conditions, and acceptance cannot create truth that was not already established by a verifier, trusted importer, finite validator, chain auditor, or structured named-obstruction boundary.
Accepted entries can power projection and known-skip behavior. Digestion and value may recommend entries; they do not write public memory by themselves.
Accepted memory can be queried. Known skips reduce wasted work by reporting an already accepted answer, but known skips are not new proofs. Candidate and advisory memory can schedule review or projection; they cannot skip verification.
Structural identity prevents memory bloat. Duplicate-looking roots, schemas, obstructions, and projection rules become review tasks, not automatic merges. Canonicalization is part of memory hygiene, not verification: digest matches may suggest a review, but they do not prove equality or mutate public memory.
Habit formation is how repeated successful routes become reusable advisory practice. It is the system's memory of what tends to work, not a truth boundary. Habit candidates require support, low risk, explicit conditions, and review before they become accepted habit rules.
Reason compression is how MathGraph moves from repeated success to reviewable explanation. It extracts atoms, tests which are load-bearing, identifies decorative conditions, and proposes minimal sufficient reason candidates. Reason nodes help humans and schedulers understand why families work, but remain advisory unless formalized and verified.
Process memory is replayed experience: the durable trace of the alchemical loop. It records what was included, what was excluded, what was killed, what was repaired, what became digestion, what became habit, what became reason, and what was projected forward. It gives agents a replayable history without confusing history with truth.
Structure registry gives the alchemical loop typed memory. It records what kind of structure an artifact appears to express and which projection routes are compatible, blocked, or require adapters. It prevents projection from becoming broad analogy by forcing every transfer through typed compatibility before scheduling.
Role-based object introduction is how MathGraph turns repeated structure into candidate concepts. It observes recurring roles, proposes definitions, searches for witnesses, and emits proof, countermodel, or formalization tasks. The role remains in Chora until reviewed, and even accepted role objects are advisory concepts unless their consequences are separately verified.
Structural analogy and exposition are how MathGraph makes its growing memory intelligible. The system compares roles and structures, records where the analogy works, records where it breaks, and emits human-readable notes plus review, projection, or digestion tasks. The analogy may guide discovery, but it remains in Chora until separately verified or accepted as advisory exposition. It cannot verify claims.
Formal-world adapters are the typed gate between advisory discovery and concrete formal systems. They parse, normalize, validate shape, and emit handoff tasks. They prevent typed projection, role objects, and analogies from jumping directly into truth by making required verifier, trusted-importer, finite-validator, or chain-audit boundaries explicit.
Verifier execution is the first point where MathGraph may pass from advisory artifact to boundary evidence. It is guarded by explicit execution flags, command contracts, unsafe-marker rejection, and alignment checks. The test drive exists to prove that advisory layers remain advisory and that only the verifier creates boundary-backed truth.
The fixture suite is the system's recurring ordeal: safe proofs may cross the verifier boundary, unsafe proofs must be rejected, missing verifiers must skip cleanly, and advisory layers must remain advisory.
Verified corpus ingestion is the first transition from isolated proof fixtures to a reusable verified-memory substrate. The corpus ordeal checks that declarations and dependency graphs remain advisory until verifier or trusted-import boundary evidence exists.
The Lawbook is not Plato's Realm of Forms itself. It is the finite, computational, verified shadow of Forms inside MathGraph: the growing record of where Chora has been ordered by LOGOS into stable, reusable structure.
- Forms = invariant lawful structure.
- Chora = receptive possibility-space.
- LOGOS = ordering principle / lawful continuation.
- MathGraph = executable process that tests continuation.
- Verifier = tribunal of lawful survival.
- Lawbook = crystallized finite verified participation in Forms.
- Projection = applying crystallized form back into becoming.
A bad lawbook is storage. A good lawbook is compressed intelligibility.
A Lawbook entry becomes Form-like when it has generality, invariance, compression, generativity, necessity, stability, and clarity.
Existential Agent Ecology is an optional higher layer above the verification kernel.
Core doctrine:
- The kernel is immortal and audit-stable.
- Agents may be mortal and biography-bearing.
- Truth remains verifier-bound.
- Discovery may become biography-bound.
Future concepts include irreversible mortality policy, agent wounds,
self-forged values, narrative identity, HeldInChora / strategic
non-verification, resource economy, and lineage / inheritance rules.
Hard guardrail: no agent wound, value, narrative, reputation, mortality status, lineage, or scar may promote a claim across the verifier boundary.
MathGraph should not become a self. It should become the world in which selves can risk themselves without corrupting truth.
Final death matters because agent death turns search into commitment. Without irreversible loss, agents have memory but not biography, cost but not sacrifice, preference but not value, exploration but not courage.
Lean project ingestion is the first transition from flat verified files to structured verified-memory substrate. The project ordeal checks that local imports and declaration references can guide dependency graphs while remaining advisory until verifier or trusted-import boundary evidence exists.
The local Mathlib allowlist layer is the first real external proof-library membrane. It treats a local proof library as structured advisory memory until verifier evidence and Lawbook review make specific declarations reusable.
Declaration discovery is a Chora-stage operation: it finds possible declarations and possible dependencies, then distills them into an allowlist manifest. Truth still enters only downstream through verifier evidence.
The proof-library demo is the recurring public ordeal: discovery enters Chora, selected declarations become an allowlist, verifier evidence fixes only what checks, and Lawbook replay demonstrates reusable memory without corrupting the boundary.
The public demo is the recurring ordeal made legible: it gathers the synthetic proof-library path, release checks, and reports into one repeatable account without pretending that successful presentation is proof.
The real Mathlib revision demo is an external proof-library membrane: it records local revision and toolchain context, then keeps every discovered declaration advisory until downstream verifier evidence arrives.