15.1 The AGENTIC mathematical contract

The maintained state contains a presented mathematical theory, an executable construction and proof language, and a sequential policy over conjectures, examples, transformations, and countermodels. The three workflows specialize as follows.

The joint creative object is not an isolated theorem. It is a new primitive or presentation together with models, executable operations, nontrivial consequences, and a curriculum showing that later reasoning can reuse it. The meta-sketch records how a structural proposal becomes an OPTIC constructor and how that constructor becomes an available RELIC decision.

In the common artifact-dossier convention of Section 10.4.1, the primitive or presentation is the structural delta, its models and executable operations are the transported realization, proof and countermodel checks supply admission evidence, and the curriculum supplies persistence and reuse. The controlled experiments below fill bounded parts of that dossier. They should not be read as admitting a historically important mathematical field merely because a withheld constructor was recovered in a generated world.

For this testbed, the enclosing package \(\mathfrak R_{\mathrm{math}}\) contains the mathematical presentation, model and proof semantics, executable constructor language, query policy, equivalence criterion, observers, and admission rules. A change is recorded by

with the theory map as its presentation component when applicable. The registered controls \(\mathsf{Ctl}_{\mathrm{math}}\) include no change, parameter recovery, family selection, stronger search in the current constructor grammar, matched proposal search without the structural diagnostic, shuffled queries or countermodels, and evaluator oracles used only as ceilings. Each evidence rung declares the applicable subset. Failure of a weaker control is evidence for opening a construction branch, not evidence that the resulting concept is valuable or transformational.

This chapter also fixes the provenance convention for Part III. Each named experiment denotes an archived unit containing a frozen registration or protocol, executable implementation, output records, and a result summary. An admission verdict applies only to that unit’s declared world family, observer, candidate language, data split, and gates. The successive evidence sequences withhold progressively more structure; unless a table explicitly pools them, their percentages are not entries in one common benchmark.

. Exact proof can admit a theorem relative to formal axioms. It cannot establish that the theorem introduces a valuable concept, nor that a transformation of a formal object has the semantics of a causal intervention. Those are separate admission questions and require separate evidence records.