Proof-discovery and verification contract

This note defines the measurement boundary for Fixture F-004. It operationalizes the versioned propose–challenge–decompose–prove–check–publish–invalidate lifecycle derived from the mathematical-practice audit. It is a shared benchmark contract for Candidates 004, 009, 010, 011, 014, 017, and 019.

Immutable identity envelope

Every episode starts with a sealed identity envelope

where $e$ identifies the episode; $h_p$ is the cryptographic hash of the exact problem statement; $h_d$ hashes its definitions and encodings; $h_\ell$ hashes the declared logic and semantics; $h_a$ hashes the admitted axioms; $h_L$ hashes the complete accessible library version; $h_C$ hashes the accessible corpus, retrieval index, and cutoff; $h_K$ hashes the checker, certificate calculus, and preprocessing reconstruction; and $h_s$ hashes the task-family generator and paired random seed. Every $h$ value is an immutable byte string. Hash equality establishes identity of registered bytes, not adequacy of the formalization or soundness of the implementation.

The accessible information record is

where each $A_e^x$ is a set of immutable artifact identifiers available through channel $x$. The channels respectively cover training, prompt/context, retrieval, proof or tactic traces, evaluation feedback, and human hints or formalization. Availability is recorded independently of whether an artifact is retrieved or used.

Versioned lifecycle state

At event time $t$ in seconds from episode start, define

where $G_t$ is the set of open typed goals, $Q_t$ is the queue of proposed operations, $L_t$ is the accessible immutable library view, $X_t$ is the set of examples and counterexamples, $D_t$ is the proof-and-dependency directed acyclic graph (DAG), $C_t$ is the set of proof, refutation, model, or test certificates, $R_t$ is the append-only event record, and $\sigma_t$ is the typed publication state. The finite state space is

An event $a_t$ may transform the state only when its typed preconditions hold:

where $T$ is the versioned transition function and $\mathcal A(S_t)$ is the set of admissible events in state $S_t$. Tested records finite support only; proved records acceptance of a derivation relative to $I_e$; refuted requires an admissible counterexample or checked refutation; unknown preserves timeouts, unsupported theories, and incomplete searches; disputed records an unresolved challenge to formalization, assumptions, checking, or significance; and retracted records invalidation or supersession without deleting history.

A published version is

where $h_i$ is the version hash, $P_i$ is the set of parent-version hashes, $o_i$ is the typed transformation, $u_i$ is the actor or process identifier, $t_i$ is the event time in seconds, $\sigma_i\in\Sigma$ is the state, $E_i$ is the evidence-and-certificate set, and $B_i$ is the measured cost record. A new version never overwrites its parents.

Proposals, tests, and counterexamples

Let $p_i$ be candidate proposition $i$, $\theta_i$ its explicit definitions and parameters, $O_i$ its set of proof obligations, $H_i$ its declared source and transformation ancestry, and $q_i$ its proposal method. The proposal record is

For a universally quantified candidate $p_i\equiv\forall x\in\mathcal X_i:P_i(x)$, an exact counterexample is an element $x^*\in\mathcal X_i$ such that

$\mathcal X_i$ is the declared admissible domain and $P_i$ is the encoded Boolean predicate. The counterexample record must prove or independently check both domain membership and predicate failure. Its size $s(x^*)\in\mathbb R_{\ge0}$ is measured under a preregistered task-native order; smallest-counterexample claims compare $s(x^*)$, not discovery time alone.

For a finite test multiset $U_i=\{x_1,\ldots,x_n\}$, empirical support is

where $n$ is the test count, $\mathbf 1[\cdot]$ is an indicator, and $\widehat q_i$ is dimensionless. The record also names the generator, distribution or enumeration boundary, random seed, arithmetic precision in bits, and error interval in the predicate's native unit. Even $\widehat q_i=1$ leaves the state tested unless a checked exhaustive reduction or proof closes the universal obligation.

Abstraction obligations

Let $\mathcal X$ be a concrete domain, $\mathcal A$ an abstract domain, $\alpha:\mathcal X\rightarrow\mathcal A$ an abstraction map, and $\gamma:\mathcal A\rightarrow2^{\mathcal X}$ a concretization map. For a concrete property $P:\mathcal X\rightarrow\{\mathrm{true},\mathrm{false}\}$ and abstract property $P^{\sharp}:\mathcal A\rightarrow\{\mathrm{true},\mathrm{false}\}$, using the abstraction to prove $P$ requires the soundness obligation

When a claimed transfer also requires preservation of operation $f:\mathcal X\rightarrow\mathcal X$, declare an abstract operation $f^{\sharp}:\mathcal A\rightarrow\mathcal A$ and check

for the stated subset of $x\in\mathcal X$. The equality is an exact semantic claim unless a typed approximation relation and tolerance are registered. Excluded cases, failed concretizations, reconstruction loss, and the human time used to choose $\alpha$ are part of the result.

Decomposition and proof-DAG reconstruction

For target goal $g_0$, let the proof DAG be

where $V_{\pi}$ is a set of goal, lemma, definition, axiom, or certificate nodes; $E_{\pi}\subseteq V_{\pi}\times V_{\pi}$ contains directed dependency edges from a conclusion to each required premise; $r\in V_{\pi}$ is the root node encoding $g_0$; and $\kappa_v$ is the typed local reconstruction function stored for node $v$. For each non-leaf node $v$ with dependency set $\operatorname{dep}(v)$, reconstruction requires

where $\pi_u$ is a checked artifact proving node $u$ and $\pi_v$ is the constructed artifact for node $v$. Leaves must resolve to hashed axioms, definitions, admitted theorems, exact decision procedures, or independently checked certificates in $I_e$.

Let $\operatorname{topo}(D_{\pi})$ be a topological ordering from leaves to root. Full-DAG reconstruction succeeds when every $\kappa_v$ executes in that order and the independent checker accepts the resulting root artifact against $h_p$ and $h_L$. A list of plausible lemmas, a cyclic graph, or individually checked children without a parent reconstruction function does not close $g_0$.

Proof-dependency economy is reported, not assumed. If $N_{\mathrm{all}}$ is the number of accessible library nodes and $N_{\mathrm{cl}}$ is the number in the root's transitive dependency closure, then

is a dimensionless dependency ratio. Smaller is useful only if reconstruction, robustness, and transfer remain non-inferior.

Generator, certificate, and checker separation

For instance bytes $F$, generator $G$, claimed verdict $y$, certificate $c$, preprocessing trace $r_F$, and independent checker $K$, acceptance is

where $h(\cdot)$ is the registered hash function and both indicator factors are dimensionless. Generator $G$ cannot set the checker's verdict. The identities, code lineage, parsers, libraries, axioms, hardware, and people shared by $G$ and $K$ are published as a shared-trust-root set $W_{GK}$; process separation is not described as independent when $W_{GK}$ contains the relevant possible fault.

For accepted artifact $i$, record certificate size $b_i^{\mathrm{cert}}$ in bytes, generation time $t_i^{\mathrm{gen}}$ in seconds, checking time $t_i^{\mathrm{check}}$ in seconds, checker peak memory $m_i^{\mathrm{check}}$ in bytes, and certificate lifecycle energy $E_i^{\mathrm{cert}}$ in joules. An unsupported solver exit code or a certificate that does not bind the exact instance and preprocessing trace cannot produce proved or refuted.

Leakage-safe task partitions

Let $\mathcal U$ be the universe of theorem, proof, definition, example, counterexample, generated sibling, and source artifacts. Define a symmetric ancestor-related relation $\sim_A$ over $\mathcal U$ that groups exact duplicates, renamings, restatements, specializations, isomorphic generated siblings, proof ancestors, and source-equivalent formalizations under the frozen detection protocol. Let $[u]_A$ denote the group containing artifact $u$.

For training artifacts $\mathcal T\subset\mathcal U$ and confirmatory artifacts $\mathcal H\subset\mathcal U$, the dependency-safe split condition is

Additionally, if $\operatorname{cl}_D(u)$ is the transitive proof and library dependency closure of $u$, require

unless the overlapping artifacts are explicitly declared as common premises available to every arm. Public benchmark queries, human corrections, and model updates after the split freeze are added to $\Lambda_e$ and disqualify the affected hidden family from confirmatory use.

Publication and reverse-dependency invalidation

Let the release dependency graph be $D_v=(N_v,E_v)$, with edge $(a,b)\in E_v$ meaning artifact $a$ depends on artifact $b$. If changed or invalid artifact set $J\subseteq N_v$ is detected, its reverse-dependency invalidation set is

Every artifact in $\operatorname{Inv}(J)$ is quarantined from proved release status until its exact version is rechecked or rebuilt against a replacement. The prior record remains addressable and becomes retracted when its published acceptance claim no longer holds; a challenge to formalization or significance may instead enter disputed while the checked derivation remains recorded.

For planted invalidation set $J^*$ and submitted set $\widehat J$, invalidation precision and recall are

Both are dimensionless; an empty submitted set receives zero precision and recall. Also report time to quarantine in seconds, stale artifact-hours before quarantine, rebuild time in seconds, repair human-hours, and recurrent bad acceptances after release.

Equal lifecycle budget

For method $m$, the binding resource vector is

The first seven terms count training items, retrieval calls, proposals, tested instances, solver calls, checker calls, and search nodes. $B_{\mathrm{state}}$ and $B_{\mathrm{cert}}$ are retained-state and certificate bytes; $t_{\mathrm{wall}}$ and $t_{\mathrm{cpu}}$ are seconds; $h_{\mathrm{human}}$ is person-hours; $E_{\mathrm{life}}$ is joules at the declared measurement boundary; and $M_{\mathrm{peak}}$ is peak working memory in bytes.

Lifecycle energy is

with every term measured in joules across one declared hardware and facility boundary. Human formalization, steering, review, and repair remain person-hours and are not silently converted to joules. A method that exceeds any binding ceiling is infeasible for that paired instance; otherwise report a preregistered Pareto frontier rather than post-hoc cost normalization.

Outcome vector and component effects

For method $m$, report

where the first five terms are artifact counts; $R_{\mathrm{recon}}$ is the dimensionless proportion of published proof DAGs reconstructed and rechecked from their retained dependencies; $P_{\mathrm{inv}}$ and $R_{\mathrm{inv}}$ are defined above; $t_{\mathrm{first}}$ is seconds to the first checked result; $b_{\mathrm{median}}$ is median certificate size in bytes; $h_{\mathrm{human}}$ is person-hours; and $E_{\mathrm{life}}$ is joules. Results are stratified by task family, state, and hidden regime rather than collapsed into a universal reasoning score.

Checked-result energy efficiency may be reported as

but only beside the full outcome vector, because a system can inflate $\eta_E$ with trivial tasks or low coverage. For component $c$ and outcome $Y_j$, the paired ablation effect is

where $m_{-c}$ removes component $c$ without reallocating its unused budget. Report paired 95% uncertainty intervals over frozen problem-family and random- seed strata.

Contract retirement

The composed residual is retired when the strongest complete ordinary stack matches its checked closure, bad-acceptance rate, hidden-family transfer, proof-DAG reconstruction, invalidation quality, and lifecycle resource vector; when any gain disappears under ancestor- and dependency-safe splits; when counterexamples, abstraction obligations, certificates, or reverse-dependency events cannot be reconstructed independently; or when omitted formalization, review, checking, storage, repair, human-hour, or joule costs explain the gain.

Editable lifecycle diagram: versioned-proof-discovery-lifecycle.mmd.