mathgraph_full_vision_design_spec.tex

\documentclass[11pt,a4paper]{article}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{enumitem}
\usepackage{hyperref}
\usepackage{xcolor}
\usepackage{booktabs}
\usepackage{array}
\usepackage{longtable}
\usepackage{listings}
\usepackage{titlesec}
\usepackage{microtype}
\newcommand{\MG}{\textsc{MathGraph}}
\newcommand{\LOGOS}{\textsc{LOGOS}}
\newcommand{\Chora}{\textsc{Chora}}
\newcommand{\Lawbook}{\textsc{Lawbook}}
\newcommand{\ObstructionAtlas}{\textsc{Obstruction Atlas}}
\newcommand{\ReasonAtlas}{\textsc{Reason Atlas}}
\newcommand{\RootAtlas}{\textsc{Root Node Atlas}}
\newcommand{\HTilt}{\textsc{H-Tilt}}
\newcommand{\Lean}{\textsc{Lean}}
\newcommand{\Isabelle}{\textsc{Isabelle}}
\newcommand{\ETP}{\textsc{ETP}}
\newcommand{\SAIR}{\textsc{SAIR}}
\title{\textbf{MathGraph}\\A Full Vision, Design, and Technical Specification\\\large A Generative Verification Kernel for Lawful Mathematical Continuation}
\author{Heath Sanchez}
\date{}
\begin{document}
\maketitle
\begin{abstract}
\MG{} is a lightweight generative verification kernel for lawful mathematical continuation. It separates proposal from the verifier boundary and accepts claims only through a proof, finite countermodel, or named obstruction terminal contract. Around that boundary it builds proof digestion, process memory, \Lawbook{} acceptance and query, typed projection, role-based object introduction, and structural analogy with exposition. These layers improve reuse, explanation, and compounding discovery while remaining advisory unless verifier, trusted-importer, finite-validation, or chain-audit evidence promotes truth.
\end{abstract}

\section{One-Line Vision}
\MG{} is a lightweight generative verification kernel where models propose, \MG{} constrains, verifiers decide, digestion assimilates, the \Lawbook{} remembers, and projection scales.

\noindent LLMs dream. \Chora{} receives. Agents explore. \HTilt{} selects. Alchemy transforms. \LOGOS{} constrains. Verifiers decide. The \Lawbook{} remembers. Projection scales.

\section{Core Doctrine}
\begin{description}[style=nextline]
\item[Continuation Under Constraint] Search may be generative, but continuation is lawful only under explicit typed constraints.
\item[Verifier Boundary] Only verifier, trusted importer, finite validator, and chain audit boundaries promote truth.
\item[Terminal Contract] Accepted claims end in exactly one terminal form.
\item[Compounding] Verified work should become reusable memory that improves future work.
\item[Advisory / Truth Separation] All non-verifier artifacts are advisory: a thing can guide search without being true, explain without verifying, schedule without proving, and be accepted as advisory memory without becoming a theorem.
\end{description}

\section{Why MathGraph Exists Now}
AI proof generation is becoming abundant. Verification is necessary but insufficient; proof digestion is the missing third stage. Mathematical workflows need infrastructure, not merely faster theorem generation. Correct but indigestible proofs can fail the system-level goal. The relevant metric is not merely ``proved,'' but ``verified, digested, reusable, explainable, and able to improve future work.'' \MG{} is infrastructure for the proof-abundance era.

\section{Formal Terrain}
The universal proof hypergraph contains possible objects, claims, transformations, witnesses, and derivations. A structural hypergraph records reusable shapes across that space. Human mathematics is a small ribbon through proof space, selected by importance rather than raw reachability. Importance combines compression, reuse, projection gain, digestion value, and explanation value.

\section{Terminal Forms and Trust Contract}
\begin{itemize}
\item \texttt{VERIFIED\_PROOF}: proof artifact accepted by a formal boundary.
\item \texttt{FINITE\_COUNTERMODEL}: checked finite witness preserving source and separating target.
\item \texttt{NAMED\_OBSTRUCTION}: structured accepted obstruction memory.
\item residual/advisory status: useful history or pressure that has not crossed truth boundaries.
\end{itemize}

\section{Kernel Architecture}
\begin{lstlisting}
Domain Claim
  -> Formal-World Adapter Registry
  -> Adapter Capability / Parse / Normalize / Validate
  -> Continuation Actions
  -> Continuation Curriculum
  -> Verification Episode
  -> Verifier / Importer / Finite Validator / Chain Audit
  -> Proof Digestion
  -> Verifier Feedback / Repair
  -> Discovery Value
  -> Lawbook Acceptance
  -> Lawbook Query / Known Skip
  -> Structural Identity
  -> Habit Rules
  -> Reason Compression
  -> Process Memory
  -> Structure Registry / Typed Projection
  -> Role-Based Object Introduction
  -> Structural Analogy / Exposition
  -> Projection
  -> Telemetry
\end{lstlisting}

\section{Alchemical Process}
Raw Matter, Calcination, Solution, Sublimation, Descension, Distillation, Coagulation, Fixation, Ceration, Conjunction, Multiplication, Projection, and Perfection name process stages. Alchemical traces are process records. They may record fixation, but only verifier, trusted importer, finite validator, or chain audit evidence promotes truth.

\section{H-Tilt and Route Pressure}
Soft tilt ranks work heuristically. Killed-dynamics or spectral \HTilt{} estimates survival from route telemetry. \HTilt{} Lite uses taste, scars, cost, compression, and projection gain. Discovery value adds route-level utility signals. All are scheduling pressure, not truth.

\section{Agentic Layer}
\texttt{AgentProfile} and \texttt{AgentExperience} record lightweight agents, taste, scars, and biography. Current agents are advisory policies, not truth authorities. Existential agents remain future work.

\section{Lawbook and Accepted Memory}
The \Lawbook{} is the accepted public-memory boundary. Candidate entries differ from accepted entries. Accepted truth entries require boundary evidence; digestion, projection, and discovery value may recommend entries but cannot turn themselves into truth.

\section{Lawbook Query and Known-Skip Service}
Accepted verified proofs can skip, accepted finite countermodels can skip, and accepted obstructions can skip only as accepted obstruction memory. Candidate-only, digestion-only, projection-only, analogy-only, and role-only records cannot skip as truth.

\section{Proof Digestion}
The workflow is proof generation, proof verification, then proof digestion. Digestion produces dependency maps, step classification, key idea candidates, reusable schema candidates, exposition notes, and projection hints. It inherits verified boundaries; it does not create them.

\section{Verifier Feedback and Repair}
Feedback records flaw severity. Repair plans may locally revise, reroute, emit proof tasks, emit obstruction tasks, hold in \Chora{}, or residualize. Feedback and repair plans do not verify claims.

\section{Continuation Actions and Curricula}
Hard targets decompose into warm-ups, simplified cases, finite examples, proof tasks, countermodel tasks, projection tasks, repair tasks, and replayable episode inputs. Curricula are planning artifacts only.

\section{Discovery Value}
Discovery value scores curricula, digestion, feedback, repair, projection, actions, alchemy, agents, and telemetry. Value is route pressure, not proof.

\section{Structural Identity and Canonicalization}
Typed structural graph views, deterministic signatures, duplicate detection, and advisory merge/conflict candidates keep memory tidy. Signature matches or isomorphism-looking matches are not equality or proof.

\section{Habit Rules and Route Promotion}
Repeated successful route outcomes become habit candidates. Reviewed habits adjust scheduling pressure advisably; habits do not verify claims.

\section{Reason Compression}
Reason compression proposes minimal sufficient reasons, distinguishes load-bearing atoms from decorative atoms, and emits reason nodes. Reasons are explanatory pressure, not theorem proofs.

\section{Process Memory}
Process episodes retain included context, excluded context, transitions, eliminations, inherited boundaries, and route/process summaries. Process memory records how work unfolded; it does not verify.

\section{Structure Registry and Typed Projection}
Broad families include algebraic, order, topological, combinatorial, logical, computational, graphical, dynamical, probabilistic, categorical, and mixed structures. Compatibility may be exact or same-family, require cross-family review, need an adapter, need formalization, block on type mismatch, or block on conflict. Typed projection is advisory.

\section{Role-Based Object Introduction}
Recurring role signatures yield definition candidates, witness candidates, conjecture/task candidates, review, and accepted advisory role objects. Role objects are concepts, not proofs or certificates.

\section{Structural Analogy and Exposition}
Analogy sources are compared through feature maps. Breaks, candidates, exposition notes, and review create projection, digestion, formalization, adapter, and review tasks. Analogy and exposition are understanding aids, not verification.

\section{Richer Formal-World Adapters}
M7 adds a lightweight typed gate between advisory metabolism and concrete
formal systems. Formal-world adapters detect broad world kinds, expose adapter
specifications and capability reports, parse raw inputs, normalize
representations, validate formal shape, and generate proof, countermodel,
formalization, finite-validation, adapter, and review tasks. They prepare
explicit handoffs to a verifier, trusted importer from verified external
artifacts, finite validator, or chain audit. Adapter-aware typed projection,
role, and analogy tasks can now state when an adapter, formalization step, or
external boundary is required. Parse, normalize, and validate success remains
advisory; an adapter does not verify unless an external boundary result is
returned with explicit evidence.

\section{Deeper Proof-System Integration}
M8 turns adapter-ready formal work into explicit, replayable proof-system
contracts. It records proof-system specifications, project manifests, artifact
manifests, import graphs, safe tokenized check-command contracts, check
requests, parsed check results, trusted import records, and proof boundary
evidence. Placeholder tokens such as sorry or admit block proof-check readiness
rather than masquerading as success. Theorem files, import graphs, check
requests, and proof-looking text remain advisory until a verifier, trusted
importer from verified external artifacts, finite validator, or chain audit
returns explicit boundary evidence.

\section{Semantic and Natural-Language Claim Handling}
M9 adds deterministic intake for informal mathematical and scientific text.
Natural-language source records are segmented, classified by claim kind,
domain, and risk, examined for ambiguity, and mined for lightweight symbol,
object, relation, hypothesis, and conclusion candidates. The layer emits
formalization requests, routing hints, and review, digestion, clarification,
adapter, and proof-system tasks. These records bridge human prose into
formal-world adapters and proof-system integration, but no natural-language
sentence, extracted candidate, or semantic score promotes truth.

\section{API Service Hardening}
M10 adds stable local request and response contracts around the backend. The
surface includes a local SDK client and optional localhost JSON service with
health, audit, query, submit, semantic-intake, formal-world-adapter,
proof-system-integration, schedule, project, explain, process-memory,
discovery-value, and advisory review routes. Every response exposes truth
status, safety level, boundary policy, certificate ids, terminal forms, and
whether an already-existing verifier boundary was crossed. API success is not
mathematical truth: no route executes external tools by default, no route
mutates accepted Lawbook memory by default, and only verifier, trusted importer
from verified external artifacts, finite-validator, or chain-audit evidence may
report terminal truth.

\section{Existential Agent Ecology}
M11 places finite-resource discovery agents above the verification kernel. Each
agent has a mortality policy, resource account, wound history, value profile,
narrative identity, Held-in-Chora records, lineage summaries, daemonized skills,
and advisory route pressure. Agents may become wounded, exhausted, retired,
archived, or dead; dead agents cannot act, resume, receive budget, mutate, or
spawn. Exact resurrection is forbidden: only public artifacts, compressed
lineage seeds, or advisory daemons may continue after death. This ecology shapes
scheduling and discovery behavior, never truth promotion.

\section{Post-M11 Hardening and Evaluation}
Post-M11 work stops broad ontology expansion and tests the existing system as a
whole. The hardening harness runs end-to-end advisory smoke scenarios,
serialization checks, CLI smoke checks, API contract checks, documentation and
spec synchronization, public-term scans, truth-boundary checks, agent lifecycle
checks, lightweight performance probes, and replay manifests. These artifacts
improve auditability and reproducibility, but hardening does not verify claims:
smoke success, docs sync, API success, and replay manifests remain advisory.

\section{Derived Closure and Projection}
Derived closure uses transitivity, source weakening, target strengthening, equivalence collapse, duality where justified, and constructor replay. FALSE-side certificate directionality must be preserved: projection may reuse verified memory, never reverse an invalid implication into truth.

\section{SAIR / ETP Nursery World}
\ETP{} over magmas is the nursery and \SAIR{} proving ground. The FALSE side uses finite countermodels. The TRUE side requires proof verification. Finite-search failure is not TRUE. \SAIR{} is the first proving ground, not the whole product.

\section{API Surfaces}
Current backend-first surfaces include lawbook query, verification episode, projection, roadmap alignment, proof digestion, verifier feedback, continuation curriculum, discovery value, structural identity, habit rules, reason compression, process memory, structure registry, role objects, and structural analogy.

\section{Roadmap Alignment Checker}
Criticals include advisory output claiming \texttt{VERIFIED\_PROOF} or \texttt{FINITE\_COUNTERMODEL}; finite-search miss represented as proof; route score treated as truth; digestion treated as proof; feedback text treated as boundary; curriculum warm-up treated as target proof; discovery value treated as truth; structural signature treated as equality; habit treated as verifier; reason node treated as theorem; process memory treated as verifier; typed projection treated as implication; role object treated as theorem; analogy or exposition treated as verification; and terminal form without boundary evidence. Positive signals preserve advisory boundaries and record lawful reuse.

\section{Metrics}
\begin{longtable}{ll}
\toprule
Metric & Purpose\\
\midrule
CertificateYieldPerCompute & terminal yield per cost\\
ResidualCompressionGain & residual reduction\\
DerivedAmplificationFactor & lawful reuse expansion\\
ProjectionGain & verified memory reuse\\
KnownSkipRate & accepted-memory avoidance\\
RoutePrecision & useful route selection\\
ObstructionNamingRate & structured failure capture\\
ConstructorReuseRate & constructor compounding\\
ProofDigestionYield & intelligibility gain\\
RepairLoopYield & repair productivity\\
CurriculumStageYield & staged task productivity\\
DiscoveryValueCalibration & value-score reliability\\
StructuralDuplicateAvoidance & memory hygiene\\
HabitPrecision & habit usefulness\\
ReasonCompressionGain & explanation compression\\
ProcessReplayCoverage & replayable history\\
TypedProjectionSafety & unsafe transfer avoidance\\
RoleReuseRate & concept reuse\\
AnalogyExpositionYield & readable relation yield\\
LawbookCompression & accepted-memory density\\
\bottomrule
\end{longtable}

\section{Efficiency Discipline}
Documentation must not overclaim code. Every advisory layer must be deletable without breaking truth. Expensive frontier models are not the first line of defense: use cheap deterministic filters first and formal verifiers where boundary crossing is required. Keep public terminology clean and remain API/backend first.

\section{External Verifier Execution and Full Test Drive}
External verifier execution is disabled by default and only runs behind explicit allow flags. Contracts use allowlisted tokenized commands, forbid shell and network execution, constrain workspace paths, cap timeouts, and reject unsafe proof markers before boundary evidence is considered. Raw success text and return code are not enough: the boundary record must include the accepted artifact, theorem names, contract hash, certificate, and verifier-crossed status. The full test drive has advisory-only and optional live-verifier modes, exercises the architecture end to end, and feeds hardening without turning smoke success into proof.

\section{Rich Verifier Fixtures and Replay}
MathGraph includes a safe Lean fixture pack with passing theorems, unsafe-marker fixtures, expected-theorem validation, type-error and import-error fixtures, optional in-memory Lawbook replay, dry-run and live-verifier modes, and a Markdown human report. Unsafe fixtures, missing verifiers, dry-runs, and expected-name mismatches create no boundary evidence.

\section{Verified Corpus Micro-Ingestion}
Verified corpus micro-ingestion moves from isolated fixtures to a tiny local Lean corpus governed by a manifest. It extracts declarations, imports, and dependency metadata; runs the local verifier boundary only when explicitly allowed; reserves trusted import for later pinned policies; emits dependency-graph output and proof-digestion inputs; supports optional in-memory Lawbook review/query replay; and distinguishes dry-run from live-verifier mode. Extraction alone is not proof.

\section{Lean Project Micro-Subset Ingestion}
Lean project subset ingestion adds a local project manifest, module-path
extraction, declaration extraction, import dependency edges, and declaration
reference dependency edges. Files are checked from the local project root only
when execution is explicitly allowed, so local imports can resolve without
network or package-manager download. Valid verifier boundary evidence may map
back only to expected declarations; dry-runs, unsafe entries, expected-name
mismatches, failed imports, module graphs, and reference graphs do not promote
truth. The layer emits dependency graphs, proof-digestion inputs, Lawbook
review/query replay artifacts, and dry-run versus live-verifier summaries while
remaining advisory until boundary evidence exists.

\subsection{Reproducible Local Test Drive}
Public scripts bootstrap a fresh clone without manual import-path setup, and a
read-only local or Colab test drive can replay the focused verifier, corpus,
project, end-to-end, hardening, and alignment workflow into report artifacts.
Fresh-clone usability, read-only replay, and successful test execution do not
promote truth; live verifier execution remains opt-in, and only explicit
boundary evidence may cross into terminal proof.

\section{Mathlib Micro-Subset Ingestion}
Mathlib micro-subset ingestion uses a local allowlisted manifest in either
synthetic fixture mode or external local-project mode. It diagnoses the local
environment, extracts module paths, declarations, imports, and reference
dependency edges, runs the local verifier boundary only when execution is
explicitly allowed, emits dependency graphs and Lawbook review/query replay
artifacts, and preserves the rule that extraction alone is not proof. The pilot
performs no downloads or package-manager operations by default.

\section{Real Local Mathlib Allowlist}
The real local allowlist pilot accepts a user-supplied local project path and an
explicit manifest. It diagnoses Lean, Lake, project markers, and empty
allowlists without downloads or package-manager execution. Local verification
remains opt-in, dependency graphs remain advisory, Lawbook replay requires
review before reuse, and extraction or environment readiness alone never
promotes truth.

\section{Declaration Discovery and Allowlist Construction}
Declaration discovery inspects explicitly selected local module files, applies a
conservative text extractor, records reference hints, and builds an advisory
allowlist manifest. The manifest may be handed to downstream allowlist
verification, but discovery alone never promotes truth.

\section{Implementation Roadmap}
\begin{longtable}{ll}
\toprule
Milestone & Scope\\
\midrule
M0 & Closed-Loop Certificate Smoke\\
M1 & Agentic Alchemical Loop\\
M2 & Projection Engine\\
M3 & Root-Aware Constructors\\
M4 & TRUE-Side Proof Verification\\
M4.5 & Unified Verification Episode\\
M5 & Route Telemetry and Spectral H-Tilt\\
M6 & Domain-General Claim IR\\
M6.5 & Lean Adapter Hardening\\
M6.6 & Continuation Actions\\
M6.7 & Proof Digestion\\
M6.8 & Verifier Feedback / Repair\\
M6.9 & Continuation Curriculum\\
M6.10 & Discovery Value\\
M6.11 & Lawbook Acceptance Boundary\\
M6.12 & Lawbook Query / Known Skip\\
M6.13 & Structural Identity\\
M6.14 & Habit Rules\\
M6.15 & Reason Compression\\
M6.16 & Process Memory\\
M6.17 & Structure Registry / Typed Projection\\
M6.18 & Role-Based Object Introduction\\
M6.19 & Structural Analogy / Exposition\\
M6.20 & Documentation / Spec Synchronization and Publication Refresh\\
M7 & Richer Formal-World Adapters\\
M8 & Deeper Proof-System Integration\\
M9 & Semantic and Natural-Language Claim Handling with Strict Boundaries\\
M10 & API Service Hardening\\
M11 & Existential Agent Ecology\\
Post-M11 & Hardening and Evaluation\\
Post-M11+ & External Verifier Execution and Full End-to-End Test Drive\\
Post-M11+ & Rich Verifier Fixtures and Replay\\
Post-M11+ & Verified Corpus Micro-Ingestion\\
Post-M11+ & Lean Project Micro-Subset Ingestion\\
Post-M11+ & CLI Import-Path Hardening and Colab Test Drive Script\\
Post-M11+ & Mathlib Micro-Subset Ingestion\\
Post-M11+ & Proof-Library Demo Pack\\
\midrule
Future & Mathlib micro-subset pilot, trusted importer policy for pinned external corpora, larger fixture-driven release gates, persistent Lawbook storage workflow, richer dependency extraction, package/release workflow\\
\bottomrule
\end{longtable}

\section{Risks and Guardrails}
Guard against proof generation without digestion; verification without understanding; advisory pressure mistaken for proof; route scores treated as truth; finite-search failure mistaken for TRUE; natural-language feedback treated as verifier boundary; proof digestion treated as proof; warm-up curricula treated as target proof; discovery value treated as truth; structural identity treated as proof equality; habits treated as authority; reasons treated as theorems; process memory treated as verification; typed projection treated as implication; role objects treated as definitions or theorems; analogy treated as proof; exposition treated as verification; stale docs causing public overclaim; and external branded terms confusing \MG{}'s identity.

\section{Proof-Library Demo Pack}
The proof-library demo pack combines a synthetic demo with an optional real local Mathlib configuration. It rehearses declaration discovery, allowlist manifest generation, verifier-bound ingestion, dependency/reference graph output, in-memory Lawbook replay, known-skip replay, and polished reporting. Demo reports, discovery output, generated manifests, and graphs remain advisory; only explicit verifier/importer/finite-validator/chain-audit evidence promotes truth.

\section{Public Demo and Release Readiness}
The public demo wraps the synthetic proof-library path in one repeatable command,
notebook-equivalent helper, polished reports, and lightweight release checks.
Demo success, release checks, reports, graphs, and API success remain advisory;
only explicit verifier/importer/finite-validator/chain-audit evidence promotes truth.

\section{Optional Real Mathlib Revision Demo}
Users may point \MG{} at an already-working local Mathlib checkout, record local
revision and toolchain metadata, inspect explicitly selected modules, generate a
curated manifest, and optionally invoke the downstream verifier-bound allowlist
flow. Missing environments skip cleanly and no package-manager operation is
performed.

\section{Curated Real Mathlib Manifest Demo}
The curated real Mathlib demo is local-path-only and explicitly selects a tiny
module/declaration set before generating an advisory allowlist manifest. Local
paths, revisions, toolchains, discovery output, dependency graphs, and reports
do not create proof evidence; only verifier-bound allowlisted declarations can
cross the truth boundary.

\section{v0.1 Release Candidate Hardening}
The release-candidate surface adds explicit version metadata, changelog and
release notes, concise CLI output, canonical artifact layouts, quickstart and
release-process documentation, and a canonical release gate. Release metadata,
release-check success, generated reports, and artifact generation remain
advisory and do not promote truth.

\section{Real Mathlib Module-Aware Verification}
Selected real Mathlib modules can be imported into generated temporary Lean
files and selected declaration names checked with \texttt{\#check}. A successful
check can create imported-declaration availability evidence only after the local
verifier runs; it is not source-proof reconstruction.
For Lake projects, generated checks are run with \texttt{lake env lean} from the
supplied project root so imports resolve through the real project environment
rather than a temporary workspace.

\section{Final Compression}
\MG{} is the world. Agents are the explorers. \HTilt{} is the compass. Alchemy is the method. \LOGOS{} is the law. Verification is the tribunal. Digestion is understanding. Process memory is biography. The \Lawbook{} is memory. Projection is scaling. Analogy is exposition, not truth.

\MG{} should not scale by becoming bigger. It should scale by making every verified thing reusable and every failure informative.
\end{document}