15.5 Admission records and formal certificates

Proofs, countermodels, independence results, conservative extensions, and machine-checked definitions form the principal admission artifacts.

A certificate here is positive, checkable evidence for a particular obligation: a proof term, a countermodel, a successful type check, or a verified transport. The enclosing admission record is broader. It names the contract, collects applicable certificates and failures, and returns admit, reject, or unresolved. This distinction prevents an abstention or failed construction from being described as though it possessed a positive certificate.

Admission should be plural. A definition can be conservative but vacuous; a theorem can be correct but unrelated to the obstruction; a useful heuristic can lack proof. Reports therefore separate formal validity, novelty relative to the frozen language, explanatory or generative value, and persistence. An oracle translation into the evaluator’s hidden theory is used for scoring, not shown to the proposal system.

Exact source syntax is generally the wrong equality criterion. Two definitions may differ by a renaming, a basis permutation, a common scale, an algebraic identity, or a different but equivalent presentation. Admission must therefore declare its quotient before proposals are scored. This issue arose concretely in the symbolic experiments below: a strict string-matching protocol rejected several mathematically equivalent generator definitions. The corrected protocol preserved that failed record and replaced textual identity by typed semantic equivalence on hidden points. This is not a favorable scoring adjustment; it is part of specifying what mathematical object the experiment claims to recover.