# Training a Peano policy without trusting it

Can a small language model learn to help with Peano Lab proofs?  Yes—but the interesting part is
not merely fine-tuning a decoder on tactic strings.  The interesting part is arranging the
experiment so that a useful model can never become a source of mathematical authority, and so
that a high score cannot be manufactured by data leakage, an accidentally stronger tactic
environment, or a stale checkpoint.

M19 turns that problem into an explicit research pipeline.  It adds a compact headless runner,
a replay-validating dataset compiler, a repository-owned next-tactic prompt, a BF16 LoRA training
runtime, a kernel-judged evaluator, and guarded Helios job controls.  These pieces are deliberately
outside the kernel.  They can make proof search faster; they cannot make an invalid certificate
valid.

```{admonition} Experiment status, 2026-08-02
:class: important
The local execution, prompt, training-runtime, evaluation, provenance, and guarded cluster paths
are implemented. Historical model-v1 WMI training produced a deliberately narrow result: 0/4
frozen goals at pass@4 and one checked direct-witness proof among eight samples. Model-v2 remains
an auditable design stage. Model-v3 supersedes it with the frozen first-247
declaration-order prefix of the current 384-theorem checked ladder,
leakage-safe predecessor-prefix trajectories, a whole-session root-balanced synthetic curriculum,
indexed completion loss, an immutable corpus seal, and a native 32,768-token no-truncation gate.

Fresh same-source sealed preparation `217851` completed in 4h01m09s under clean commit
`4d44609ee32d5d28726c082ef7b5649c0a1107a6`. It passed eligibility, the exact
20,765-row/73,446,475-token audit, representative LoRA updates, a real Trainer step and evaluation,
restored-bare-forward saved-policy admission, fresh reload, and independent report verification.
Production job `217859` completed and its admitted rank-32 adapter entered the paired frozen-goal
experiment. Trained job `218171` and revision/configuration-pinned pretrained comparison `218172`,
whose report declares no PEFT adapter, finished sequentially in 3m51s and 4m20s. Their immutable
raw `k=1` reports say 3/4 versus 0/4. The three trained scripts
also replay individually through the independent kernel, but the induction-heavy fourth goal was
not solved. The canonical whole-report replay rejected the trained report because its nested policy
identity omitted four full-library fields, and the ordinary replay remains unchanged. A separate
version-pinned historical attestation has now passed and independently replayed all 3/3 claims; a
dedicated base attestation also passed declared control identity, provenance, search accounting, and
zero-claim validation. The narrow four-goal `k=1` result is therefore admitted as 3/4 versus 0/4.
The cross-binding paired artifact records `paired_launch_smoke_admitted`. No bit-for-bit base-weight,
statistical, broad PA, non-trivial induction, causal-superiority, 4B, or expert-iteration claim
follows.
```

The binding research protocol is
[`docs/PEANO_TRAINING.md`](https://github.com/nasqret/vietnam2026/blob/peano-lab/docs/PEANO_TRAINING.md).
This chapter explains why that protocol has its present shape.

## Watching training without steering it

A long cluster job should be observable without giving a web page scheduler authority. Peano Lab's
Training Observatory therefore keeps SSH in a small loopback Python process:

```text
browser → localhost JSON cache → fixed read-only SSH reader → WMI evidence
```

The browser polls every five seconds while visible. The collector serializes remote reads, accepts
one explicit decimal job number, reads only fixed Slurm commands, bounded artifact reads, and log
tails, and
retains the last good snapshot when the VPN drops. There is no cancel, submit, arbitrary-command,
path, or write endpoint. Remote values enter the document as text, and the server sends a strict
same-origin content-security policy.

The more subtle design problem is semantic honesty. The active Trainer shuffles rows and is
configured to accumulate up to 32 microbatches per optimizer step; its final partial window has 29.
The corpus inspector therefore says *representative reported sample*, not *current batch*.
Likewise, while job `217859` was active it emitted carriage-return progress immediately but buffered
its periodic loss dictionaries in redirected stdout. The dashboard plots only exact flushed or
terminal-manifest loss records. Before one existed, it left the production curve empty and labelled
the preparation loss `2.8299612998962402` as a one-step admission-smoke diagnostic. GPU activity,
step time, or a falling ETA can never be repackaged as learning evidence.

Run the view with:

```bash
make peano-training-dashboard PEANO_TRAIN_JOB=217859
```

The complete architecture, field meanings, security boundary, and test contract are in
[`docs/PEANO_TRAINING_DASHBOARD.md`](https://github.com/nasqret/vietnam2026/blob/peano-lab/docs/PEANO_TRAINING_DASHBOARD.md).

## The useful interpretation of “a compact Peano Lab”

Starting a browser, loading Pyodide, importing thirty-odd Python modules, and rendering terminal
panels for every generated proof would be a poor data-generation loop.  A long-lived Python process
can import the prover once and execute many JSONL requests much faster.

There are two ways to obtain such a process:

1. write a second, reduced parser, tactic interpreter, and checker; or
2. remove the browser while retaining the production parser, tactic surface, proof engine, and
   checker.

Only the second is Peano Lab.  The first would create a *shadow prover*.  A generated proof could
succeed under the shadow semantics and fail on the website; worse, a bug in the shadow checker
could label false training examples as proved.  Testing two implementations against one another
would reduce the risk, but it would not remove the duplicated source of truth.

The implemented runner is therefore an **adapter**, not a miniature prover:

```text
JSONL request
    │
    ▼
strict request validation
    │
    ▼
production formula parser ── original target and logic mode retained by owner
    │
    ▼
production run_surface grammar ── immutable ProofState transactions
    │
    ├── raw version-1 transition trace
    │
    ▼
checked_surface_final
    │
    ▼
independent kernel checker(original target, exact logic mode)
    │
    └── only here may the result say kernel_checked=true
```

The browser and the batch runner differ in transport and presentation.  They do not differ in
proof rules.  The headless path omits the DOM, terminal panels, Pyodide routing, and routine
certificate rendering.  It reuses `parse_formula_with_names`, `ProofSession`, `run_surface`, the
checked theorem library, certificate finalization, and the independent checker.

This gives a useful engineering principle:

> Optimize around the trusted boundary before optimizing through it.

Keeping one Python interpreter warm removes avoidable startup work.  Omitting display rendering
removes avoidable formatting work.  Omitting the final kernel call would change the meaning of the
result, so it is never a performance option.

## Two modes, only one data mode

The Python API makes the distinction visible in its names:

- `run_proof(...)` executes a proof with binding version-1 transition tracing;
- `verify_proof(...)` checks an already-authored script without retaining transition data.

Both build the certificate and perform the same final kernel check.  The quiet path is useful for
filtering known scripts and regression checks.  Synthetic generation and policy search use the
traced path, because the desired training object is not just a Boolean QED.  It is an auditable
sequence

$$
  (s_0,a_0,s_1), (s_1,a_1,s_2),\ldots,(s_{r-1},a_{r-1},s_r)
$$

whose last state is closed and whose complete certificate checks for the original theorem.

The command-line process reads one strict request per physical line.  For example, a request file
may contain:

```json
{"v":1,"id":"add-zero","theorem":"forall n. n + 0 = n","tactics":["intro n","rewrite PA3","refl"]}
```

The generation form is:

```bash
python3 scripts/peano_batch.py --environment model-v1 \
  --trace-output run.trace.jsonl < requests.jsonl > results.jsonl
```

This is a finite transactional file interface, not an interactive duplex protocol.  Results are
withheld until EOF and, in trace mode, until the trace name has committed.  The default transaction
ceilings are 10,000 requests, 256 MiB input, 128 MiB result envelopes, and 512 MiB raw trace;
larger corpora are sharded or use an explicitly reviewed limit.  Exit zero means the transport
completed, while each row carries its proof status.  Verification jobs add `--require-proved` when
every executed request must close.

The normal per-proof trace ceiling remains 16 MB. The exact model-v3 library generator is one
reviewed exception: it selects a host-owned 128 MiB ceiling because a valid large certificate
crosses the ordinary bound. The Python API caps this override; it does not change the JSONL
transport's separate 512 MiB aggregate default, and an input JSON record cannot request it.

`run.trace.jsonl` contains only the binding raw trace stream.  `results.jsonl` contains compact
per-request outcomes.  They are separate on purpose: the trace exporter must never have to guess
whether a JSON object is a transition, a footer, or a convenience response.

The command owns the execution mode and tactic environment.  A request cannot ask for a more
powerful surface.  Inputs have bounded physical lines, strict UTF-8, strict JSON with no duplicate
keys, bounded integers, or floating-point values, closed one-line theorems, and complete one-line
tactics.  Output is
staged before publication.  An empty, all-invalid, fail-fast, or unexpectedly interrupted batch
before the hard-link commit does not leave a final trace at the requested path.  The hard link is
the explicit commit point: an interruption after it may leave the complete, already-fsynced trace
while stdout is absent or incomplete.  That trace is valid; discard the result redirection and
reconstruct or rerun it.  A caller that needs an atomic result file redirects stdout to its own
temporary name and renames it only after a successful process exit.

The status vocabulary also refuses to blur distinct events:

| Status | Meaning | A proved theorem? |
|---|---|---:|
| `proved` | all goals closed and the final kernel check accepted | yes |
| `open` | the supplied tactics ended with goals remaining | no |
| `tactic_error` | a legal execution attempt failed transactionally | no |
| `tactic_limit` | an explicit resource bound stopped the attempt | no |
| `kernel_rejection` | final evidence failed independent checking | no; fail stop |
| `request_error` | the JSON request never entered a proof session | no |

A failing tactic must emit one error transition with identical before and after goals and the same
diagnostic as the raised tactic error, and must
leave the entire immutable state unchanged.  A successful command must produce the transition or
transitions, replay journal, and engine transaction that its real execution produced.  In
particular, top-level `auto` is not allowed to
claim one opaque transition after secretly replaying a different primitive history.  The finite
model surface currently excludes `auto` until that replay can itself be capability-scoped.

## Where soundness lives

It is tempting to call the whole pipeline “verified” because it ends in a checker.  That is too
coarse.  Different components justify different claims.

| Component | May choose | May certify |
|---|---|---|
| generator | theorem templates, proof scripts, mutations | nothing |
| language model | one candidate tactic line | nothing |
| tactic engine | proof-state transformation and certificate candidate | nothing globally |
| dataset compiler | whether a trace satisfies the data contract | replay integrity, not PA truth by itself |
| independent kernel | whether a certificate derives a formula in the selected logic | the exact PA judgment it checks |

For every QED the session owner retains four pieces of authority independently of the tactic layer:
the parsed original theorem, its display-name table, the exact intuitionistic/classical mode, and
the trace owner.  The adapter rejects a returned session that replaces any of them.  Finalization
submits the finished certificate against that retained theorem—not against the tactic layer's last
rendered goal.

The model does not emit certificate constructors, Python, theorem declarations, mode changes, or
`qed`.  It emits text in the same public tactic language a student uses.  This is not enough by
itself to guarantee a proof: a buggy tactic could still build malformed evidence.  It is enough to
keep model inference outside the trusted computing base because malformed evidence still reaches
the independent checker.

There is also a narrower scientific boundary.  The checker establishes

$$
  \Gamma \vdash_{\mathrm{PA}} p : P.
$$

It does not establish that an English sentence was faithfully translated as $P$, that the dataset
split was fair, or that a benchmark environment matched training.  Those are separate contracts
with separate evidence.

## A trace is not positive data until it survives replay

The raw trace is retained unchanged.  A sidecar supplies research metadata such as theorem family,
lineage, logic mode, and the exact tactic capabilities.  The dataset compiler then accepts positive
cross-entropy rows only from sessions satisfying all of these conditions:

1. the raw footer says `qed: true`;
2. the ordered successful tactic sequence replays through the current public surface;
3. the replay closes and the independent kernel accepts the rebuilt certificate;
4. each canonical before state, focus, tactic, after state, status, and error agrees with the raw
   transition;
5. the replayed proof-tree size agrees with the raw footer; and
6. family and lineage metadata permit a split assignment before transition expansion; and
7. sessions with the same canonical theorem formula belong to the same connected split component,
   even if their genealogy labels disagree; and
8. sessions sharing any exact rendered policy prompt belong to the same component, even when their
   original theorems and genealogy differ.

This is stricter than checking each transition locally.  A prefix can contain many correct steps
without proving its theorem.  Such a prefix is useful search telemetry, but training it as if QED
were guaranteed would teach survival rather than proving.  Similarly, failed tactics are useful
future ranking data; they are not positive completion targets.

The compiler publishes `train.jsonl`, `val.jsonl`, `test.jsonl`, and one manifest as a coherent
artifact set.  The trainer refuses raw trace files and accepts only rows whose byte digest, row
count, prompt contract, environment preimage, and replay counts agree with that adjacent manifest.
This deliberately duplicates some fields.  Redundancy is useful when disagreement is treated as an
error rather than silently resolved in favor of whichever copy is convenient.

### Attestation recompiles the data instead of trusting the manifest

A self-description is not independent evidence.  A malicious or stale builder could write matching
hash fields for the wrong bytes, or a later code change could make an old split impossible to
reproduce.  Before model import or output-directory creation, the training attestor therefore starts
again from the committed raw trace and metadata artifacts.

It checks their hashes, requires the recorded compiler inventory to match the current compiler and
Peano source tree, reconstructs the fixed `model-v1` capability preimage, scans every split for the
four frozen held-out formulas, and confirms that canonical theorem formulas and exact rendered
policy prompts are both disjoint across train, validation, and test.  It then invokes the current
replay compiler in a fresh temporary directory.  The rebuilt `train.jsonl`, `val.jsonl`, and
`test.jsonl` must have exactly the same sizes and SHA-256 digests as the release files.  For the
first M19 release this independent rebuild is byte-identical and the held-out contamination count
is zero.

This attestation is stronger than loading and rehashing the final rows: it demonstrates that the raw
kernel-checked sessions, current code, fixed environment, split algorithm, and prompt compiler lead
back to those exact bytes.  It is still not a proof of broad mathematical coverage or good model
performance.  It certifies the identity and replay contract of one dataset.

## Three prompt-design bugs that looked harmless

The final prompt is short:

```text
<task>next_tactic</task>
<env>peano-lab-v1;surface=model-v1;logic=intuitionistic;capability_sha256=…</env>
<state>{"focus":0,"goals":["⊢ ∀ n. n + 0 = n"]}</state>
<tactic>
```

The completion is one tactic line.  The stored dataset envelope adds the terminal delimiter
`</tactic>` so malformed records are easy to reject.  The loader strips that delimiter and
supervises exactly the tactic tokens followed by the tokenizer's EOS token; every prompt token is
masked from the causal loss.  At inference time the adapter returns the bare tactic, not XML and
not an explanation.

Arriving at this small format exposed three surprisingly general lessons.

### 1. A surface label is not an authority description

Suppose both training and evaluation say `surface=model-v1`.  One process might allow theorem
`add_comm`; another might accidentally allow the held-out target itself.  The strings match, but
the proof problems do not.

Peano Lab therefore canonically serializes the capability preimage

$$
  C=(\text{label},\text{allowed commands},\text{allowed theorems})
$$

and computes $h=\operatorname{SHA256}(C)$.  The prompt carries $h$; the row and manifest retain the
complete $C$; the trainer recomputes the digest; and evaluation checks that the adapter's preimage
equals the goal's actual execution environment.  The logic mode is displayed separately in the
prompt and is also owner-held.  Thus the full authority is the pair of exact logic mode and exact
capability object, not the friendly label and not the hash alone.

This fixed a real class of *authority-hash mismatch*: it is not sufficient to hash a name for an
environment, nor to record a digest without retaining and validating its preimage.  The same rule
applies recursively to tacticals.  A forbidden theorem inside an unselected `first [...]` or
`orelse` branch is still forbidden; syntax hidden in a dead branch must not smuggle capabilities.

### 2. Raw trace focus can leak the action

Version-1 `ProofState` has no persistent cursor.  A raw trace's `focus` is computed from the
submitted command.  If the action is

```text
focus 2 refl
```

then the trace records zero-based focus `1`.  Feeding that `1` into the policy input while asking
the model to predict `focus 2 refl` reveals part of the answer.  The feature looks like state, but
it was produced by the label.

Policy rows therefore render the runner-owned default focus `0` and preserve all goals in their
canonical order.  Goal selection remains part of the tactic action.  A future prover with a genuine
persistent user cursor may expose that cursor, but it must come from the pre-action state rather
than from parsing the target completion.

This is a useful causal test for every proposed feature:

> Could this field be known before the action was chosen?

If not, it belongs in the label, the successor state, or evaluation metadata—not in the input.

### 3. Kernel alpha-equivalence does not erase surface trajectories

The kernel represents bound variables by De Bruijn index, so renaming a binder changes no kernel
formula.  The interactive language, however, lets later tactics mention visible names:

```text
intro n
induction n
```

Changing the first line to `intro k` while retaining the second line does not preserve an
executable script.  Likewise, generated names such as `IH`, `h_witness`, and renamed collision
variants influence later tactic text even when the underlying certificate is alpha-equivalent.

The version-1 dataset consequently declares an **exact authored binder trajectory**.  It preserves
the visible names in each state and the exact successful tactic line that reaches the stored next
state.  Replay verifies the whole trajectory.  Synthetic generators must choose their binder names
deterministically within a lineage; they may not independently alpha-rename states and actions.

This choice solves executability, not every statistical problem.  Two independently generated
proofs can still present the same mathematical state with different arbitrary naming actions.  A
later prompt version may canonicalize binder-introducing actions or expose an explicit name-binding
map, but such a change must be versioned and replayed.  “Names do not matter to the kernel” is not a
license to make the policy's input/output pairs inconsistent.

## Synthetic data needs a family tree

Randomly splitting transition rows is almost guaranteed to leak.  Adjacent rows from one proof
would appear on both sides of the split.  Renamed copies, commuted equations, altered numerals, and
alternative proofs of the same generated theorem can be only marginally less obvious duplicates.

The compiler therefore splits *before* expanding sessions into rows.  It connects family, lineage,
canonical theorem-formula, and exact rendered policy-prompt nodes:

```text
family ── lineage
   ├── canonical theorem formula
   └── exact rendered policy prompt(s)
```

Sessions sharing a family or lineage belong to one connected component.  The canonical-formula
edge provides an independent defense against false genealogy metadata: two sessions proving the
same printed kernel formula cannot cross splits merely because a producer assigned different
labels.  The policy-prompt edge handles a different leak: proofs of different original theorems can
reach the same model input, which must not appear in both training and evaluation.  Components are
ranked by a SHA-256 value derived from a declared split seed, then assigned deterministically to
train, validation, or test while reserving a training component.  Every transition from every
member of a component follows that assignment.

The consequence can look inconvenient: a small, highly connected corpus may yield a tiny or empty
validation split.  That is more honest than manufacturing validation rows by cutting a proof family
in half.  Scaling the generator should create genuinely distinct components, not weaken the split.

The initial 18-session catalog remains a useful end-to-end smoke fixture.  The first frozen
training-scale release is now larger and exact:

| Property | Released value |
|---|---:|
| kernel-checked sessions / independent roots | 2,522 |
| unique canonical statements | 2,522 |
| positive next-tactic rows | 10,000 |
| train / validation / test rows | 8,149 / 926 / 925 |
| proof-first schemas | 29 |
| domains | 5 |
| frozen held-out target occurrences | 0 |

The five domains are logic, equality, PA recurrence, witnesses, and arithmetic.  The combined split
digest is
`1fa98caa2e0528d39c1b9003c4ee153dfbe633cb1ee4505e8f5b28eb837465dd`.
All 2,522 source statements are distinct canonical formulas, and every session reaches QED through
the ordinary headless surface and independent kernel before contributing rows.
The raw traces, sidecar, source manifest, compiled splits, attestation, and concise reproduction
instructions live together in
[`data/peano-policy-v1/`](https://github.com/nasqret/vietnam2026/tree/peano-lab/data/peano-policy-v1).

This is a supervised-policy baseline, not unrestricted PA conjecture generation.  Its 29 schemas
do not include induction or planner-generated invariants, negative preference examples, or
natural-language formalization pairs.  Schema similarity also remains across IID roots; a genuine
family-OOD evaluation must withhold whole templates.

The implemented model-v2 generator addresses the most damaging coverage failure without weakening
genealogy.  It schedules complete, checked roots by *emitted transition rows* in three lanes:
foundation, induction, and library, with weights $2:1:1$.  A pre-reconciliation capacity exercise
under the former 45-import authority produced 50,002 foundation, 25,000 induction, and 24,998
library rows from 22,706 distinct roots.  That historical result establishes the scheduler's
100,000-row mechanics, not the current authority's capacity.  At 10,000 rows or more the current
publication contract refuses a corpus unless all 25 public tactic heads and all 56 permitted
theorem imports occur.  The four benchmark roots are excluded by name and canonical formula from
generated targets, while their seven-name reverse-dependency closure is excluded from imports and
retrieval.  Every accepted root still reaches independent kernel-checked QED
before it contributes even one row, and a session is never cut to repair a quota.  This is an
implemented generation capability, not yet an attested final model-v2 release or a training
result.  Executed failures will remain a separate ranking/value corpus.

A useful curriculum measures more than source length.  Relevant coordinates include formula AST
size and depth, tactic steps, certificate nodes and depth, verifier calls, automation used, branch
factor, and whether a witness, induction invariant, or local lemma had to be invented.  These
measurements let us ask whether a model learned a new proof pattern rather than memorized another
spelling of an easy one.

## Supervised learning: one decision at a time

The primary artifact is a next-tactic policy, not a whole-script chatbot.  Given canonical open
goals and a fixed environment, it predicts one complete public tactic line.  Peano Lab executes the
line and supplies the next real state.  This choice has several advantages:

- every decision can be checked immediately and transactionally;
- search can branch at a proof state without regenerating a long common prefix;
- deterministic tactics can handle routine arithmetic leaves;
- failures have a precise state/action interpretation; and
- token cost can be attributed to individual search choices.

The first smoke configuration used `Qwen/Qwen3-1.7B-Base` with BF16 rank-8 LoRA for 100 optimizer
steps.  Model-v2 has a separate heavy configuration for the same pinned 1.7B base: BF16 SDPA,
rank-16/alpha-32 LoRA over the attention and MLP projections, effective batch 32, learning rate
$10^{-4}$, a 2,048-token input budget, and three full epochs over the 100,000-row curriculum.  The
same configuration is consumed by the Helios GH200 and WMI A100 launch paths.  It has not yet
produced a trained model-v2 adapter.  Comparisons with `Qwen/Qwen3-4B-Base` and
`Pythagoras-LM/Pythagoras-Prover-4B` are deferred until the 1.7B baseline is evaluated.

The runtime uses a repository-owned non-chat prompt, right padding, completion-only loss, PyTorch
SDPA, deterministic seeds, and no tokenizer vocabulary modification.  It rejects an over-length
example rather than truncating the environment header or the start of a proof state.  The model-v2
preparation gate tokenizes every selected train and validation row with the exact pinned tokenizer
and 2,048-token limit, checks the resolved revision and EOS token, and records minimum, median,
p95, p99, maximum, mean, and headroom together with config and input hashes.  Both cluster paths
run this audit offline before training.
`PYTHONHASHSEED` must be set before interpreter startup; Python, NumPy when present, PyTorch, CUDA,
Transformers, and dataset shuffle seeds are recorded or derived deterministically.

Training loss is useful for debugging optimization.  It is not the primary model-selection
metric.  A policy that predicts common easy tactics can have a pleasant loss and still solve no new
theorem.  Checkpoint selection must ultimately be based on kernel-judged validation under frozen
budgets.

## Evaluation and transactional verifier-guided search

The implemented evaluator performs independent bounded rollouts.  At each step it renders the
canonical goals, asks the policy for one line, validates the text, executes it under the goal's
capability object, and classifies the outcome as proof, invalid output, failing tactic, or resource
limit.  A rollout counts only when `checked_surface_final` accepts the full certificate for the
externally retained theorem and logic mode.

The small protocol regression set contains `le_trans`, `le_antisymm`, `le_total`, and
`mul_eq_zero`.  All four run under one reported foundation theorem set; their own target names and
canonical formulas are absent from the attested 10,000-row release, their theorem names are not
importable, and `auto` is unavailable.  Four problems are not a credible final benchmark.  Before
any broad generalization claim, M19 must additionally freeze a larger set covering held-out
lineages, held-out whole templates, larger depths, unseen lemma/witness compositions, and a small
human-authored set.

Verifier-guided search is now an implemented host layer.  Its basic shape is:

1. place the initial real proof session in a frontier;
2. ask the policy for several complete tactic lines;
3. execute each line transactionally through the production surface;
4. discard invalid or failing actions, and retain successful successor sessions;
5. prioritize fewer and smaller remaining obligations, then proposal rank and stable path order;
6. hash the ordered canonical goal tuple and deduplicate canonical successors;
7. retain only a bounded beam and stop at host-owned model-call, candidate, state, text, and depth
   limits; and
8. count success only after the final independent kernel check against the original target.

Every candidate edge is reconstructed by replaying its entire command prefix in a fresh
`ProofSession`.  That choice is less memory-efficient than cloning engine internals, but makes the
transactional guarantee obvious: a malformed or failing sibling cannot damage its parent or
another branch.  The policy may return several ranked tactic lines in one physical model call;
multiline text, envelopes, session commands, and tactic failures are discarded without repair.
Search depth has a hard maximum of 32.  Canonical-goal deduplication is an efficiency heuristic: a
mistake there could lose a useful route, but it cannot manufacture QED because publication still
passes the independent checker.  The interactive client adds a second fresh replay before showing
or saving the ordinary proof script.

Once a trained model-v2 search finds new checked proofs, expert iteration may add their
trajectories to the positive set.  Failed actions and dominated successful successors can support
a separate ranking objective.
They should not be mixed into SFT labels merely because they were produced by the same run.  Any
later reward optimization receives terminal proof reward only from independent QED; a certificate
size bonus is conditional on QED and cannot compensate for an invalid theorem.

### The first paired model-v3 smoke—and why it needed a historical bridge

The first frozen comparison ran the trained adapter and a revision/configuration-pinned pretrained
Qwen3-1.7B comparison under the same four goals, seed, depth-32 beam-16 search, eight candidates per
state, and host-owned budgets. The comparison report declares that no PEFT adapter was attached.
The single-session-owner rule made the GPU jobs sequential: trained job `218171` took 3m51s, and
pretrained job `218172` took 4m20s. At `k=1`, their immutable raw reports say 3/4 and 0/4
respectively.

The trained policy found three compact tactic routes:

| Goal shape | Route | Certificate nodes |
|---|---|---:|
| closed numeral arithmetic | `norm_num` | 98 |
| existential witness | `exists 5`; `norm_num` | 29 |
| quantified right-zero calculation | `intro n`; `rewrite PA3`; `simp` | 10 |

All three scripts replay independently through `verify_proof` against their original formulas and
the actual model-v3 surface. The pretrained comparison emitted 32 malformed sequences and executed
no tactics. The
fourth theorem, `forall x. exists y. x * (x + 1) = 2 * y`, remained unsolved. Because it is the only
genuinely induction-heavy goal, the narrow pedagogical reading is clear: the adapter displayed
useful syntax and shallow tactic composition, but this run did not demonstrate induction planning.

There is also a provenance lesson. The evaluator used the real full 247-theorem environment for
prompting and listed that authority elsewhere in the report, yet the nested base-policy identity
serialized a legacy reduced projection. Four required fields were absent:
`library_identity_sha256`, `library_full_identity_sha256`, `library_prefix_length`, and
`library_size`. The canonical model-free replay compared this nested record with the exact full
authority and rejected it. That refusal is the system working: three kernel-valid certificates do
not excuse a structurally incomplete experiment identity.

The original report remains immutable, and the ordinary replay gate remains strict. The separate
compatibility attestation recovers this historical case by pinning the exact
report hash, source commit, evaluation job, historical evaluator sources, legacy four-field
projection, and reconstructed full-library values, and then independently replaying every claimed
proof. `trained-compatibility-replay.json` passed with all 3/3 proof claims independently replayed;
its embedded attestation SHA-256 is
`e900a10241db0451992313eb2a7b0341911a7a71cd8af91e831a279874afda56`.
The dedicated `pretrained-base-replay.json` passed declared pretrained identity, provenance, and
search-accounting validation with zero proof claims; its embedded attestation SHA-256 is
`056519bc3598a390526fdf9054aa38090d499f7f837af0a2ace7af8caaa560e7`.

One final paired artifact joins the two conditions rather than leaving their agreement implicit.
It binds the exact training manifest—SHA-256
`caa5569c98ed9ea048d413301b803c39011957d1c97307e5b109846989e18569`, with 649 expected and 649
actual optimizer steps—the two reports, both producer attestations, source commit, three job
records, goal set, seed, and search budgets. Historical Git lookup verified 36 trained-semantic,
36 pretrained-semantic, 61 trained-evaluation, and 62 pretrained-evaluation entries, with 62 unique
source blobs and agreement on every overlap. `paired-launch-smoke-attestation.json` passed with
result `paired_launch_smoke_admitted`; its embedded attestation SHA-256 is
`9b33b4e488f14e38fc7c5a122410d53e9e1123409dcccafdc73e0a8ab1a14bae`, and its file SHA-256 is
`cdd20cc6e97ff442cff1c476135963f726b740372223f6eac72335543f6c11ba`.

The pairing is strong, but deliberately not stronger than its inputs. The pretrained condition is
revision/configuration-pinned and reports no PEFT adapter, yet its base weight shards were not
content-hashed before and after model loading. It is therefore not a bit-for-bit base-weight
attestation. Neither evaluation report retains complete raw generation transcripts, so the paired
layer cannot replay the model's raw text, host extraction, or every executed search edge.
Attribution of candidates to the two producers rests on byte-pinned historical
producer/source/job records; certificate validity rests separately on the consumed trained
attestation's three kernel replays. Retained WMI `sacct` and log-bundle artifacts additionally
record completion, but Slurm does not cryptographically authenticate those scheduler observations.

Thus the narrow frozen four-goal `k=1` launch smoke is admitted as 3/4 versus 0/4. The ordinary
trained-report replay still rejects the historical incomplete identity and has not been weakened;
the bridge is version-pinned and separately scoped. This distinction is as important to students
as the tactics: kernel soundness and scientific provenance are related, but neither substitutes
for the other. Three shallow proofs on four goals, with the induction theorem unsolved, establish
neither broad PA ability, induction capability, bit-for-bit pretrained-weight identity,
statistical reliability, nor causal superiority.

## What to measure

One scalar cannot describe this experiment.  At minimum every model/search condition should report:

| Question | Measurement |
|---|---|
| Does it solve problems? | independently checked pass@1, pass@4, and pass@16 |
| Is it cheap? | solved goals per generated token, kernel call, and second |
| Is search wasteful? | proposals, unique states, duplicate states, frontier peak |
| Are proofs compact? | certificate nodes and depth, conditional on QED |
| How does it fail? | invalid text, tactic failure, explicit limit, kernel rejection |
| Does it generalize? | per-family and per-difficulty outcomes on frozen splits |
| Is the estimate stable? | exact counts and bootstrap confidence intervals |

The budgets are part of the metric.  “Pass@16” is ambiguous unless sampling temperature, maximum
tactic steps, maximum generated tokens, theorem capabilities, deterministic closers, and verifier
calls are all fixed.  Wall time should be reported alongside hardware and batching because it is
not portable by itself.

Mandatory baselines include deterministic Peano tactics, the untrained base model, SFT greedy
decoding, SFT sampled pass@$k$, and SFT plus the now-implemented bounded beam search.  Comparisons
between 1.7B and 4B models must use the same data and verifier/token budgets, but the 4B run remains
deferred until the narrow four-goal smoke is replaced by a larger, repeated,
adequately attested 1.7B benchmark. A formal-prover prior and a general base model of
similar size should be compared as model families, not under selectively tuned settings.

Formalization remains a separate experiment.  The kernel can decide whether a proof derives the
formula a model emitted.  It cannot decide whether that formula faithfully expresses an English
sentence.  Exact AST checks work for templated synthetic pairs; human language requires semantic
review and must never be folded invisibly into the proof success rate.

## Helios: guarded operations, not a magic benchmark

The cluster workflow selectively adapts operational patterns from the SAIR Helios repository, but
Peano Lab owns its prompt and experiment contract.  The current target is the
`plgccaiautore2026` grant, the `plgrid-gpu-gh200` partition, one GH200 GPU job at a time during the
pilot, and the `ML-bundle/25.10` module baseline.  The fixed project root is
`$SCRATCH/codex-control/projects/peano-lab-training`.

The historical model-v1 progression was deliberately staged:

1. verify the committed 10,000-row release from its raw traces with the independent attestor;
2. inspect the source, dataset, and attestation manifests;
3. run the read-only Helios probe;
4. synchronize source while preserving remote checkpoints, results, caches, and the submission
   ledger;
5. test each Slurm script with `sbatch --test-only`;
6. run the CPU environment smoke;
7. prepare the pinned isolated Python environment and run its full GH200 smoke;
8. run the 1.7B, 100-step adapter smoke;
9. reload/resume it and run kernel-judged evaluation; and
10. use that result to decide whether the next controlled experiment should change data, search,
    or model scale.

The negative induction/order result selected data and search: model-v2 is the next experiment.
The 4B comparison was therefore not scheduled and remains deferred until the heavy 1.7B v2
baseline is evaluated.

The wrappers default to test-only.  A real submission requires both `--submit` and the explicit
confirmation token `PEANO-LAB-TRAINING`.  Every accepted submission appends timestamp, job ID,
script path, work directory, git commit, and script SHA-256 to `logs/submissions.tsv`.  Scheduler
logs are evidence that a job ran; they are not a substitute for the dataset, training, and
evaluation manifests.

The GH200 is an ARM machine.  `ML-bundle/25.10` loads CUDA libraries and advertises an immutable
ARM wheel directory through `PIP_FIND_LINKS`; it does not itself make `torch` importable.  The
preparation job therefore clears an isolated venv, installs the exact `torch==2.9.1+cu129` wheel
and a fully version-pinned Python dependency closure using binary wheels and no resolver freedom,
then requires `pip check`.  Scheduled jobs replace inherited `PYTHONPATH` with the two reviewed
repository roots, disable the user site, and assert the exact Torch/CUDA build.  The standalone
short GPU job consumes that prepared environment and therefore requires an `afterok` preparation
dependency.  It checks `aarch64`, CUDA visibility, the loaded PyTorch build, and Peano kernel
execution.  Versions and the resolved runtime inventory are recorded, but the current lock does not
use `--require-hashes`; this is not yet a claim of byte-identical wheel reproduction.  Before a
longer job is trusted, the full smoke sequence must also demonstrate BF16 forward/backward
execution, the relevant Python packages, adapter save/reload, tokenizer round trips, and evaluation
through the Peano kernel.  FlashAttention, vLLM, DeepSpeed, bitsandbytes, and QLoRA may later be
measured optimizations; none is a prerequisite for the first correctness run.

The corrected preparation job `20029964` subsequently passed this entire gate from clean commit
`41683e2`. It resolved the pinned Qwen3-1.7B model and tokenizer revision, performed a finite BF16
LoRA optimizer step on a GH200, saved and hashed the adapter and tokenizer, reloaded them, and
obtained another finite loss. That is evidence for the runtime boundary, not evidence that a useful
policy has been trained. Job `20029970` then completed the registered 100 steps in 9m51s. Its
teacher-forced train loss was 0.78446 and final validation loss 0.13518. Those figures show that the
adapter fit the next-tactic distribution; they do not measure complete proof success.

Evaluator `20029980` stopped after three seconds, before generation. Canonical manifest JSON uses
`sort_keys=True`, whereas the loader accidentally applied the construction-order rule designed for
raw dataset rows to the nested capability mapping. The repair reconstructs the exact three semantic
fields from sorted JSON and still checks their values, the environment preimage/hash, and equality
with the fixed `model-v1` authority.

## WMI A100: reproduce the gate, do not rename the environment

The WMI cluster provides a useful second path when Helios queues are long. Its
[published resource table](https://cluster.wmi.amu.edu.pl/02_02_zasoby_klastra.html) lists a node
with four NVIDIA A100 80GB GPUs. Live scheduler inspection confirmed that the owner belongs to
`hw_csi` and can use the non-preemptible `gpu_csi` partition. The lower-priority `gpu_spot` and
`gpu_idle` partitions can be requeued; they are inappropriate until the training loop explicitly
handles that lifecycle.

The important lesson is that “NVIDIA cluster” is not one environment. Helios is ARM with the
CUDA-12.9 wheel lock described above. WMI is x86-64 and exposes an official
`anaconda/2025.12-1` module whose `pytorch-gpu` environment contains Python 3.12, PyTorch 2.5.1,
and CUDA 12.4. Reusing the Helios lock would be both technically wrong and provenance laundering.

The corrected WMI probe `171369` requested one *typed* A100 and installed nothing. In thirteen
seconds it verified exactly one visible A100-SXM4-80GB, BF16, a finite backward pass, Python
3.12.12, Torch 2.5.1/CUDA 12.4, driver 610.43.02, outbound access, and 18 TB free storage.

The resulting environment is a two-layer contract. A canonical manifest names the central Python,
`ensurepip`, Torch/CUDA, numeric stack, and delegated dependency versions; live preparation proves
each distribution still resolves below the fixed central prefix. A twelve-wheel overlay then pins
Transformers, PEFT, Accelerate, safetensors, and their missing or incompatible dependencies by
exact x86-64 wheel SHA-256. The content-addressed environment ID hashes both records. Every overlay
distribution must resolve below that release, and a `current` pointer is rejected when its ID no
longer matches the freshly revalidated base.

Source deployment follows the same idea. A clean `git archive` excludes ignored and uncommitted
files. WMI reconstructs its Git tree, then publishes under an exclusive deployment lock only after
the tree matches; source-dependent preparation, training, and evaluation jobs hold the shared lock,
and sync removes valid provenance before it touches the live tree. Preparation moves the
environment pointer last, after package checks,
independent dataset attestation, a real LoRA optimizer step, adapter/tokenizer save and reload, and
finite losses. Replacement job `171395` passed that complete A100 gate in 8m39s. It reproduced
dataset digest `1fa98caa…`, recorded the exact commit and A100/Python/Torch environment, and saw
finite losses `6.06434` before save and `5.53506` after reload.

The next failure was deliberately cheaper. The training controller refused to call `sbatch`
because its Bash `IFS` reader collapsed the preparation row's empty dependency field, shifting the
remaining TSV columns. Empty fields are data, so a bounded strict UTF-8 parser now validates nine
columns exactly and rejects malformed or duplicate job rows. Since that repair changes source
identity, the passed preparation report could not be relabeled as its predecessor; a fresh
same-source chain was required. Moving the computation does not move the trust boundary: every generated proof
is still replayed by Peano Lab and every QED is checked against its original theorem.

Fresh preparation `171414` then passed from clean commit `0c84fc3`; dependent training `171421`
completed 100 steps, and evaluator `171423` reached a terminal kernel-judged report. The training
manifest binds adapter `ff187542…`, 2,048/256 selected examples, and train/validation losses
0.78301/0.13615. The attractive second number is teacher-forced next-token loss. The theorem result
is 0/4 at pass@4: all sixteen rollouts failed before QED.

Two arbitrary requests sharpen the diagnosis. The parity goal failed sixteen times; fifteen runs
proposed division as a direct existential witness. A new direct-witness theorem absent exactly from
all three splits succeeded once in eight samples and replayed to a seven-node checked proof. The
adapter therefore demonstrated one within-template success, but not the missing induction frontier.
Whether fine-tuning caused that success remains open until the pretrained base is evaluated.

That behavior is predicted by the corpus. Its 8,149 train rows use only sixteen of twenty-five
allowed tactic heads, contain no IH state or foundation-lemma use, and contain no `induction`,
`simp`, `have`, `suffices`, `specialize`, or `use` action. Every source proof is at most seven
steps. Under exact model-v1 authority, known checked held-out routes require 10, 10, 23, and 13
commands; the old 16-step evaluation cap does not even fit the known `le_total` route. More
parameters alone do not address absent actions and proof shapes; scaling now would confound the
intended curriculum experiment.

A separately maintained candidate lemma library was authorized for publication. Its 26
dependency-ordered entries extend the public-catalog source from 23 to 49 theorems. All replayed
deterministically; the immutable pre-integration report records a largest fully expanded
certificate of 21,515 nodes at depth 66. Reconciliation with the first M20 branch then yielded the
historical 63-entry local snapshot because fourteen post-core records overlapped exactly. Later
native arithmetic passes and self-contained Cut packaging extend the current local candidate to
247 unique checked theorems: 23 baseline entries, 212 general foundational entries, and twelve
unique modular capstones. A twelve-rung tranche adds constructive equality, divisibility,
and primality decisions, bounded factor-pair search, proper-factor descent, and prime-divisor
existence. The next seven add modular-congruence transitivity and addition plus
functional single-position Gödel-β decoding. Five pre-CRT successors add
modular multiplication, decomposition-to-congruence transport, and the bridge
from a decoded β value to balanced congruence. Three reverse bridges add
bounded congruence uniqueness, reconstruction of the directed remainder, and
the converse β interface. The result is a checked equivalence between `At`
and bounded balanced congruence. Six CRT successors add the two modular
consequences of balanced Bézout, successor-modulus predecessor cancellation,
constructive binary CRT, its bounded-remainder form, and one code realizing
two bounded β positions under an explicit modulus-coprimality premise. Their
certificates contain no DNE. Six more checked entries prove each beta modulus
coprime to its base, reduce a common divisor of two beta moduli to the scaled
index gap, derive pairwise coprimality when $j=i+\mathit{gap}$ and
$\mathit{gap}\mid c$, apply that theorem to the two-position CRT client, and
construct bounded nonzero common multiples. The condition is essential:
$c=1$ gives moduli $3$ and $6$. Seven further entries convert the bounded
common-multiple invariant into bounded-prefix pairwise coprimality, close
coprimality under accumulated products, descend congruence from a product
modulus, and check the universal preservation step for a future bounded CRT
fold. Six more certificates add right-factor divisibility, the product and
decoded-congruence successor steps, their combined prefix step, and an
ordinary-induction theorem carrying the four-part invariant through every
bounded prefix. Its full-bound wrapper concerns residues already decoded from
the input code and is extensionally satisfied by choosing that code itself;
it was not yet an arbitrary finite-sequence recoding theorem. Later checked
layers add independent β finite-prefix recoding, exact Product traces,
greatest-prime-divisor descent, and canonical factorization existence and
extensional uniqueness. The native FTA certificate has 73,767 nodes, depth 99,
and 2,184 Cuts. The checked `prime_unbounded` client then closes the last
planned prime endpoint constructively from a bounded common multiple and a
prime divisor of its successor. None of those local snapshot counts claims that
production has already
been promoted.

The 247-theorem source-bound corpus has fingerprint
`6fc52e25f17dc2ff0c0e7a141c350430d6aa1d0a7a87b82e22840f442f666939`.
Its full-library smoke has 494 sessions, 9,235 raw/9,232 unique transitions,
and all 247 authored QEDs. Browser build `2026-07-29k`, application
`a-77df7c0860bc`, records the local candidate and does not claim deployment.

For training, the historical frozen first-247 declaration-order prefix is
registered as the distinct content-addressed `model-v3` authority inside the
current 384-theorem native runtime, not as a silent extension of model-v1 or
model-v2. The prompt
exposes bounded retrieved lemma names and canonical statements, and the library corpus contains
downstream `use` and authored proof trajectories. Once an exact capstone theorem is importable,
its three-line application is a usability test rather than an unseen proving test; different
theorem families must remain sealed.

## Why the first run failed

The 0/4 result initially looks surprising beside validation loss 0.13615. It stops being surprising
once the two measurements are aligned. Validation asked, roughly, “can the model continue a tactic
line from another instantiation of a familiar short template?” The benchmark asked, “can it plan a
10--23-step proof using induction and named lemmas, sustain one error-free trajectory, and remain inside
Peano Lab's language?” Those are different tasks.

The exact audit is:

| Quantity | First model-v1 run | Evaluation contrast |
|---|---:|---|
| Train rows available | 8,149 | diverse proof states |
| Rows actually consumed | 1,600 (19.6%) | multiple full balanced epochs |
| Permitted tactic heads represented | 16/25 | all relevant heads |
| `induction`, `simp`, `have`, `specialize`, `use` labels | 0 | required by reference routes |
| IH states / order states / foundation-lemma uses | 0 / 0 / 0 | each occurs somewhere in the suite or its reference routes |
| Authored proof length | 1--7, mean 3.97 | known checked routes use 10, 10, 23, and 13 actions |
| Distinct generator schemas | 29 | whole-family OOD diversity |
| Validation schemas also present in train | 27/27 | held-out theorem families |

The labels are sharply imbalanced too. `intro` accounts for 40.52% of training rows; `intro`,
`exact`, and `refl` together account for 66.76%. Every one of 513 comparable context-free
existential states says to choose a witness immediately. The parity model's repeated attempt to use
the mathematically suggestive but syntactically unavailable witness `n * (n + 1) / 2` is therefore
not mysterious: the corpus taught “introduce, then witness”, but never taught the induction that
constructs a legal recursive witness.

The raw action interface compounds the curriculum problem. The prompt contains a capability hash,
not the PA grammar or the statements of the available lemmas. Of the 40 recorded evaluation
attempts, 24 stopped on language-interface mistakes: division or subtraction in a PA term,
unavailable commands or tactics, or malformed tactic arity. Only 84 of 123 proposed prefix actions were accepted
by the surface at all, and acceptance still does not mean progress.

Finally, each rollout is a brittle path. It dies on its first rejected action even though Peano Lab
already guarantees transactional failure. If the right action probability were 90% at every step,
a 23-step route would survive with probability only $0.9^{23}\approx0.089$; at 80% it falls below
0.006. The 16-step cap made the known 23-step `le_total` route impossible regardless of model
quality. These facts strongly explain the failure. They do **not** yet prove that 1.7B parameters or
rank-8 LoRA are sufficient; those are later controlled ablations, as is causal attribution of the
one shallow success to fine-tuning rather than the pretrained base.

## What the public catalog contributes—and what it does not

A reproducible local audit replayed the new 26 entries over the full tactic surface with each
dependency made into an explicit `use`. It produced 474 distinct checked state-to-tactic rows: 427
authored commands plus 47 imports. The authored bodies average 16.4 commands and reach 52. In
442/474 transitions (93.3%) the focused goal has a nonempty context; the replay also exposes IH
states, witness contexts, multiple goals, and lemma composition. These are candidate model-v2 rows,
not data available to the frozen seven-theorem model-v1 environment.

It is not a complete curriculum. The 474 labels contain only one `induction`, one `suffices`, four
`have`, eight `simp`, and 47 `use` decisions; `assumption` and `forall_elim` are still absent. If we
simply appended these rows and kept the old 2,048-row/100-step sampler, only about 113 catalog rows
would enter the selected subset and about 88 would actually be consumed. The lone induction row
would have only about an 18.6% chance of being seen. A larger theorem catalog without a balanced
sampler is not a learning algorithm.

The catalog also changes the leakage boundary. A training replay for a rung may see only the 23
core facts and earlier extension entries, never its own theorem or a later one. Its 47 dependency
edges are positive retrieval examples. Other earlier lemmas are not automatically negatives:
transitive ancestors and alternative proofs may still be useful. Negative ranking data must come
from actual transactional attempts whose failure is recorded separately. Since
`mod5_fourth_power_one` belongs to the authorized public catalog and the current local candidate,
applying it in an environment that exposes it measures retrieval and application, not discovery
of the fourth-power theorem.

Some audited full states are also substantially longer than model-v1 data: median 323 characters
and maximum 4,869. Much of the excess repeats context across sibling goals. The model-v2 representation
retains the complete canonical goal array, adds the grammar, and retrieves only eight
name/statement records. A later observation ablation may compact sibling descriptions, but policy
sufficiency of that representation must be measured rather than assumed.

## Model-v2: the historical correction design

This design correction was implemented, although its heavy experiment did not run. Its most important
idea is that **what identifies the theorem authority is not what must fit in every prompt**.

1. Freeze 50--100 or more sealed roots across induction, order, divisibility, residues, lemma
   composition, and human-authored problems. Replay every reference within a 32-step oracle budget.
2. Run the pretrained Qwen3-1.7B base, current adapter, deterministic tactics, and a simple
   state-shape baseline under identical token, model-call, and kernel-call budgets.
3. Bind a content-addressed successor snapshot under a new prompt version. Show compact PA syntax
   and retrieved lemma names with canonical statements instead of only an opaque hash.
4. Generate 100,000--150,000 positive transitions from at least 10,000 checked roots, with every
   tactic head represented, 20--30% induction/IH trajectories, 20--30% lemma retrieval and
   composition, and proof-length strata 1--7, 8--15, and 16--32.
5. Store two to four actually executed rejected candidates per positive state in a separate
   ranking/value corpus. Never relabel them as successful SFT examples.
6. Train the 1.7B model for two or three complete balanced epochs and select checkpoints by
   kernel-judged development QED, not token loss alone.
7. At each immutable state, sample 8--16 candidates, execute them transactionally, discard failures,
   deduplicate canonical successor states, and retain siblings in a bounded best-first frontier.
8. Only then compare LoRA ranks or a 4B model under fixed data, seeds, update counts, and search
   budgets.

The highest-leverage interface ablation is raw free-form tactic generation versus a hierarchical
legal-action policy: first choose one of the 25 heads, then point to an in-scope hypothesis,
variable, or retrieved lemma, and generate free PA terms only where a witness or intermediate
formula genuinely requires it. That design should reduce `/`, `lia`, and arity hallucinations while
remaining a tactic policy whose final product is an ordinary portable Peano Lab script.

## Model-v3: checked prefixes and balanced roots

Model-v2 identified the right ingredients but was designed around a much smaller library. Model-v3
turns the complete declaration-ordered 247-theorem ladder into the training authority. The identity
gate binds every theorem's canonical statement, direct dependencies, source specification, authored
script, reconstructed certificate, node count, and depth. It then reconstructs every certificate
from the authored tactics and asks the independent kernel to check it from the empty context against
the original closed proposition. A catalog row is therefore evidence to be verified, not an oracle
that can attest itself.

Library supervision follows a strict predecessor-prefix rule. For theorem number $i$, both the
executable capability and prompt library are exactly the declaration prefix
$\mathrm{THEOREMS}[:i]$. The target and all later theorems are unavailable. Its trajectory first
imports only its declared direct dependencies with ordinary `use` commands and then executes the
authored tactic script unchanged. The dataset compiler replays that complete QED again before
emitting next-tactic rows. This produces useful theorem-composition examples without letting the
policy retrieve the answer it is being taught to prove.

The observation remains compact. Prompt v3 includes a compact inventory of every allowed theorem
name in the current prefix, then deterministically scores the full propositions and displays at
most twelve detailed `name : statement` records. This distinction matters: an audit of statement
retrieval alone exposed only 242 of 640 direct-dependency `use` labels at $K=12$. The name inventory
keeps every legal dependency selectable without copying every large proposition into every prompt.
Very large displayed statements use a bounded canonical excerpt with a content marker; the full
checked identity and prefix digest remain in the environment record. Thus the prompt can be small
without weakening the authority that the dataset, adapter, evaluator, and replay attestation bind.

Large proof states needed a different kind of sharing. Prompt v3 encodes canonical one-line goals
with `shared-declarations-v1`: one deterministic first-occurrence table contains every exact
comma-delimited context chunk, a second contains every exact target, and each visible goal contains
only a vector of declaration indices and a target index. The parser reconstructs every original
goal byte-for-byte and rejects duplicate, unused, reordered, non-integer, or out-of-range table
claims. This is a lossless structural encoding, not target truncation and not a lossy model
observation. Raw trace states, row `state` fields, held-out structural checks, replay, and kernel
inputs remain unchanged; prompt versions 1 and 2 remain byte-identical.

The encoded state JSON must fit 44,000 Unicode characters or prompt construction fails. No exact
target, hypothesis, or visible name is shortened to satisfy this limit. A retained audit of all 443
states around the index-230 stress theorem measured a maximum of 39,423 encoded characters; its
step-115 state shrank structurally from 196,457 legacy characters to 37,259. The exact largest-state
check is 29,111 tokens including tactic and EOS, leaving 3,657 tokens below Qwen's 32,768 native
window. All 222 exact transition prompts for this stress proof pass (median 17,444, p95 26,662,
p99 28,537, maximum 29,111). The complete pinned-tokenizer combined-corpus scan remains the final
acceptance gate.

The synthetic half corrects a subtler model-v2 failure. Artificial implications had wrapped many
otherwise different roots, making `intro gate` the first label far too often and even hiding real
induction roots. Model-v3 removes those induction gates by one checked immutable transformation and
schedules complete kernel-checked sessions by their genuine first tactic head. The catalog has 51
proof-first schemas across 14 root heads; root-session imbalance is bounded and `intro` may account
for at most 20% of emitted sessions. Library schemas are deliberately absent here because the exact
247 predecessor-prefix trajectories provide that supervision separately.

That gate removal exposed a useful generator-design trap. The implication was not only a proof
obstacle: it was also the sole index-varying text in each inherited induction statement. Deleting
it therefore collapsed thousands of intended examples to four canonical roots. The repair adds a
six-digit base-4 expression made entirely from terms `d * 0`. It has 4,096 syntactically distinct
values per induction schema, remains arithmetically zero, and leaves `induction` as the first
tactic. Closed-zero syntax creates statement diversity here without pretending to add new
mathematical difficulty.

The first WMI preparation run, job `172536`, found a separate finite-domain defect. It completed
all 247 checked library trajectories—8,494 transitions and 247 QED footers—then failed after
1:02:34 when `root-equality-ring` generated a product with normalized coefficient 132. The `ring`
tactic correctly rejected it because its reviewed limit is 128. The corrected domain enumerates
the 2,396 safe base-7 tuples, excluding the four coefficient-132 tuples and the one
coefficient-144 tuple. Pairing those tuples with sixteen compact two-digit base-4 zero tags yields
38,336 distinct safe ring statements. Because the failed run had already exercised schema catalog
version 1, this repaired catalog is explicitly version 2 rather than silently changing the meaning
of an old identity.

The deeper repair treats scheduling like a compiler prepass. Before executing any proof or
creating output files, a model-free planner canonicalizes every proposed statement, enforces
uniqueness and finite-domain capacity, checks the exact row total, the `intro` cap, and root-head
balance, and hashes the ordered schedule. A valid candidate that exactly equals a sealed evaluation
formula follows one narrow typed exclusion path and is counted; malformed candidates still abort.
The expensive execution must reproduce the planned counts, skip counts, and digest exactly. A
final-row edge case required one more rule: among equally deficient heads, prefer the
heads whose shortest sessions are longer, reserving one-row heads for exact completion. For seed
`peano-policy-v3-balanced-wmi-20260729`, this prepass gives exactly 70,000 rows in 32,600 distinct
sessions, covers all 51 schemas, and assigns 2,328 or 2,329 sessions to every one of the fourteen
heads. The pinned sequence digest is
`79d2704eab6eb73205ff2234f55f0d4a7e034176fe8dc8649c6950ff499d547b`. The registered version-2
plan needs no duplicate or overlong-session skips; both closed-`norm_num` schema families contribute
1,164 distinct roots. At the advertised 100,000-row maximum, the same prepass produces 46,574
unique sessions and safely counts and omits the one numeric candidate equal to a sealed target.
WMI now invokes the synthetic generator before the library generator, allowing this seconds-long
prepass to reject a bad launch before either corpus begins expensive proof replay. An upfront
empty-data-directory gate likewise rejects stale partial-run artifacts before either generator
starts.

Job `172536` exited with status 2 before dataset construction, attestation, tokenization, A100
smoke, training, or evaluation. Transactional staging published no partial synthetic corpus. The
figures above describe the corrected deterministic plan, not a completed corpus or learned-model
result.

Attestation accepts the combined release only if it reconstructs every prefix from 0 through 247,
finds the exact predecessor-prefix plus full-synthetic schedule, rebuilds the dataset from raw
traces, and observes zero held-out contamination. Tokenization is another fail-closed gate: every
selected train and validation sequence must fit the pinned Qwen tokenizer under its native
32,768-token position limit. A root-probe audit already found 57 of 247 full-prefix theorem prompts
above the invalid 4,096-token draft ceiling, with a maximum of 6,235. The complete-data audit may
still reject the native limit; there is no truncation path.

The old model-v2 regression targets now occur in the training ladder, so reusing them would measure
library retrieval rather than theorem discovery. Model-v3 therefore seals four different formulas:
one closed arithmetic equality, one existential subtraction witness, a doubled right-zero identity,
and the consecutive-product-even theorem. Their exact names and canonical formulas are bound in the
attestation, and the generator rejects them before execution.

These four are a launch smoke, not a comprehensive benchmark: three deliberately calibrate short
arithmetic behavior and only consecutive-product-even requires multistep induction. General proof
quality requires a larger hidden post-training suite covering induction, theorem composition,
order, divisibility, and quantified witnesses under the same kernel-checked search budget.

The original draft registered two epochs over a row-prefix-capped population. The implementation
audit rejected both choices for the first model-v3 run. A row prefix can cut a proof session or
discard a small theorem rung, and a second traversal doubles the dominant long-context cost before
one exact pass has established a baseline. The successor protocol below retains every library
transition, selects synthetic data by whole proof sessions, derives one pass from the selected row
count, and records the exact optimizer-step total before loading the model. At
the time this protocol was frozen, it was still a run specification rather
than a result: no model-v3 optimizer step, adapter, solve rate, or comparison
had yet been produced. Later sections record the completed run and its
narrowly admitted four-goal launch smoke.

## From a checked population to one auditable training run

The long model-v3 build revealed that “the dataset” names three different objects:

1. a **historical replay population**, whose proofs and transitions were produced under one clean
   source commit;
2. a **selected curriculum**, which admits all library rows and a balanced subset of complete
   synthetic sessions; and
3. a **tokenized optimization schedule**, whose linear and quadratic costs depend on one pinned
   tokenizer.

Conflating these objects creates subtle scientific errors. Replaying 78,494 transition rows does
not mean all of them should be trained equally; choosing the first $N$ rows is not neutral; and a
row count is a poor compute measure when sequence lengths range over orders of magnitude. Model-v3
therefore gives each object its own canonical, self-digested attestation.

### Whole-session selection

All 8,494 exact catalog-prefix transitions are mandatory. Synthetic data is selected under a
12,288-row ceiling, but a session is indivisible: either every one of its tactic transitions is
present or none is. The selector first places one complete anchor for each of the 51 schemas. It
then adds complete rounds across all 14 genuine root heads, using a seed-derived content rank and
stopping before the next round would exceed the ceiling. The algorithm is independent of input
file order and binds both the entire candidate population and the chosen rows.

This means the final number of synthetic rows need not equal 12,288 exactly. A few unused slots are
evidence that the proof boundary was respected, not wasted data. A second `max_train_samples` cap
would be dangerous because it could slice the already audited selection; model-v3 configurations
reject it. The selection seed must also equal the training seed, so there is one declared source of
randomness rather than two identities that happen to agree in a particular run.

The tokenizer pass then records, for every selected row, its token IDs, sequence length $L_i$, and
number of supervised completion tokens $C_i$. It enforces explicit ceilings on

$$
  \sum_i L_i, \qquad \sum_i L_i^2, \qquad \max_i L_i,
  \qquad \text{and} \qquad \max_i C_i.
$$

The squared term is a deliberately conservative proxy for attention work. These bounds prevent a
small-looking row budget from hiding an accidental long-context explosion. No tokenizer result may
be truncated to pass the gate.

The first current-source scan is a useful example of why these are measured gates rather than
decorative configuration. WMI job `214264` selected 20,765 rows---8,494 catalog rows and 12,271
synthetic rows, with 17 synthetic slots deliberately unused at the next whole-session boundary---
but counted 73,446,475 train tokens, 4.92% above the registered 70-million limit, and stopped before
runtime smoke or optimization. That selection implies 649 one-epoch optimizer updates at
microbatch one and accumulation 32. The revision to 74 million is deliberately narrow: it gives the observed
immutable selection 553,525 tokens (0.754%) of headroom while preserving the 12,288 synthetic-row
ceiling and every other gate. The earlier full-population audit measured a 29,111-token maximum
under the same tokenizer and unchanged tokenization code, so
$\sum_i L_i^2 \leq 29{,}111\sum_i L_i = 2{,}138{,}100{,}333{,}725$, below the unchanged
2.3-trillion quadratic ceiling. The retry must still publish the actual self-digested audit before
this evidence can authorize training.

### Indexed completion logits preserve the objective

Each example is still the repository-owned prompt followed by one tactic line and EOS. Prompt
labels use the ignore index, and the completion is one contiguous suffix. In a causal language
model, the logit vector $z_i$ predicts token $y_{i+1}$. If $S$ is the set of supervised labels,
ordinary completion-only cross entropy is

$$
  \mathcal{L}
  = \frac{1}{|S|}
    \sum_{(b,j)\in S}
      \operatorname{CE}\!\left(z_{b,j-1}, y_{b,j}\right).
$$

Most model-v3 prompt positions are masked, yet a conventional forward pass materializes a
vocabulary-sized logit vector at every one of them. Qwen3 exposes `logits_to_keep`; Peano Lab asks
for only the union of positions $j-1$ appearing in the sum above. Targets for shorter rows remain
ignored after right padding. Cross-entropy numerators are accumulated in FP32 and divided by the
exact number of supervised tokens across the whole gradient-accumulation window.

Nothing in the equation changes. This is the same loss and the same gradient with a smaller final
activation tensor. The implementation fails closed if the model does not explicitly advertise the
indexed-logit argument, a row violates the suffix/right-padding contract, multiple GPUs are hidden
behind `DataParallel`, or distributed token accounting is ambiguous. A pinned Qwen3-1.7B LoRA
probe compared the full and projected forms and found matching loss and gradients to numerical
precision.

### Why a historical corpus needs a seal

Proof generation and independent replay can take hours. Trainer code may improve while that job is
running. Two tempting responses are both wrong: mutating the old deployment destroys provenance,
while copying an untracked `data/` directory into new code asks the new trainer to trust anonymous
bytes.

The model-v3 corpus seal preserves the useful separation. It accepts exactly twelve dataset files
and the historical preparation's three reports, validates their internal source/job/authority
relations, copies them into a private directory, fsyncs and re-hashes them, publishes with a
non-replacing rename, and makes the closed tree read-only. Symlinks, hard-link aliases, non-regular
files, unexpected names, malformed JSON, mixed Slurm jobs, or a changed source during copying are
fatal. The last source-path comparison includes mode and link count as well as identity, size, and
timestamps. A failed creation retains its visibly partial stage: pathname-based cleanup could both
mask the original I/O failure and delete a replacement installed after inspection. One
`content_sha256` binds the complete result.

There is a bootstrapping wrinkle: the first seal must preserve the old unsealed corpus and reports
while using the newer sealing code. Deployment explicitly protects those historical paths. The
tracked one-time CPU job `peano_wmi_seal_v3_corpus.sbatch` pins job `173040`, its clean source
commit, destination, manifest, all twelve artifacts, and both reviewed source hashes. The
authenticated dataset-attestation report is now pinned at
`4e1cf0d00725a739d6f371062ff2079cfb9bc3e36daf4f4219cbbe1399a68a12`;
the token audit is now pinned at
`c290b285eabcf9d39ab13b4d6f0f194588541484390d35c00681041979e2f8d8` after checking all 64,500
train and 6,000 validation rows. The A100 runtime smoke is pinned at
`86cc35bfcf2d5ff51931c140f3eb7168e3f641e1f80d54a3984dba9e49e40749`; it passed on the immutable
Qwen3-1.7B revision with rank-32 LoRA and 34,865,152 trainable parameters. All three report anchors
are therefore installed. A reviewed WMI Python verifies all inputs and retains a no-replace probe
on the target filesystem.
The job then makes and retains a fresh private bootstrap containing only the CLI and standard-
library seal module; its staged inventory forbids package markers and bytecode caches. A launcher
embedded in the submission-hashed job stable-reads and hashes the CLI, then compiles exactly those
verified bytes with isolated Python; the CLI performs the same closed-tree and external-anchor
checks on the module and corpus. Thus neither `__init__.py`, `.pyc`, nor a replaced pathname
silently joins the trusted program. Seal recovery verifies an existing destination and atomically
publishes only a canonical same-job report, closing the crash window without replacing the seal.
The destination is classified before the mutable historical paths are inspected, so recovery reads
only sealed copies and literal anchors even if the originals have since been retired. The retained
no-replace probe covers both atomic publications only after the seal and report parents are proven
to share one filesystem device. Existing reports are freshly verified, fsynced with their parent,
and verified again; a failed publication retains its read-only sibling stage rather than risking
deletion of a pathname that changed after inspection.

A seal is not a signature. The expected historical commit, job ID, and content digest must be
obtained independently. Current code first verifies those external anchors and every sealed byte,
then compares its compiler/kernel source inventory, prompt contract, held-out formulas, and
247-theorem authority against the historical manifest. The old attestation proves how the corpus
was produced; the new eligibility record proves that current code assigns the same meaning. This
avoids a second multi-hour proof replay without turning mutable artifacts into authority.

### The four-stage WMI chain

The new GPU path is intentionally split:

1. **Sealed preparation** performs no theorem generation. It verifies current-source eligibility,
   tokenizes every selected row, and runs a real BF16 LoRA optimizer/save/reload smoke. The smoke
   exercises the longest active sequence and the largest supervised completion together: when no
   natural row realizes both maxima, it inserts attended, label-masked prompt tokens immediately
   before the longest completion's supervised suffix. This reaches the maximum active length even
   for attention implementations that discard zero-attention padding. After freeing the manual
   optimizer state, the smoke also executes one real `CompletionOnlyTrainer` optimizer step and one
   explicit evaluation on the same envelope. Every trainable LoRA parameter must receive a finite
   gradient, adapter tensors must change, and deterministic post-update logits/loss must equal those
   from the reloaded adapter. A shared runtime gate also rejects every distributed/plugin path:
   exactly one process and visible GPU, matching `cuda:0` Trainer and Accelerator devices, BF16,
   `DistributedType.NO`, `DynamoBackend.NO`, no DeepSpeed/FSDP/tensor parallelism, exact Trainer
   accumulation, and Accelerator backward divisor one. The last condition prevents a second
   environment-driven division of an objective already normalized over its complete token
   accumulation window. Training rejects a missing whole-window `num_items_in_batch`, while
   evaluation uses the local supervised-token mean. Non-reentrant checkpointing, AdamW constants,
   and unfiltered non-finite logging are explicit arguments rather than inherited defaults.
   Trainer's built-in clip is disabled because it precedes `on_pre_optimizer_step` and permits a
   non-finite norm; the callback audits raw gradients, clips to norm 1.0 with
   `error_if_nonfinite=True`, and audits the post-clip population before optimization.
2. **Training** depends on that exact preparation job and verifies its three reports again. It
   requires one visible A100, one process, fresh output, no resume, and one row-count-derived pass.
   Trainer checkpointing and periodic evaluation are disabled outright; intervals beyond the run
   are insufficient because the default callback can still request a terminal checkpoint at
   `max_steps`. The trainer's actual optimizer-step count must equal the precomputed count. The
   adapter and tokenizer are
   saved before the explicit full validation pass, preserving the learned tensors if that late
   pass reaches a wall-time or runtime failure. Stock Trainer evaluation averages per-batch token
   means, so this pass is finite lifecycle evidence rather than a corpus-global completion-token
   NLL. The final manifest remains stricter: it appears
   only after validation and all identity rechecks succeed.
3. **Evaluation** depends on that exact training job. Four frozen goals use sampled
   kernel-guided search with depth 32, beam width 16, eight candidates per state, 512 model calls,
   4,096 states, and 256 generated tokens per candidate. Before loading weights, the evaluator
   equates the manifest's training-job ID, the exported predecessor ID, and the submission-ledger
   predecessor; independent replay checks the recorded binding. Later interactive proof requests
   are labelled separately because they consume an already completed adapter and have no false
   `afterok` edge.
4. **Independent replay** loads no model. It accepts only the exact evaluator-v4 authority and
   search budget, checks all duplicated counters and proof payloads, and sends every attempt marked
   `proof` through a fresh `verify_proof` call against its original goal. It emits a canonical
   non-overwriting attestation.

### A logical predecessor is not always a live Slurm edge

WMI's Slurm controller retains a finished job only for its configured `MinJobAge` (observed as
300 seconds), although `sacct` keeps the accounting record much longer. Slurm therefore rejects a
new `afterok` dependency once a successful producer has aged out of the controller. That happened
after preparation `217768`: `sacct` still reported exactly
`217768|COMPLETED|0:0|0:0`, while a new scheduler dependency was no longer legal.

The launch API now represents the distinction directly. `--afterok JOB` is accepted only for a
live `PENDING`, `CONFIGURING`, `RUNNING`, or `COMPLETING` predecessor and emits exactly one Slurm
edge. `--completed-predecessor JOB` requires one canonical matching `sacct` allocation row,
`COMPLETED`, and zero ordinary and derived exit codes; it emits no scheduler edge. Both modes still
bind the same job ID into the environment and the append-only ledger. Real submission also verifies
the predecessor's same-source ledger row and script/helper digest, plus the terminal preparation
reports where the handoff requires them, then rechecks accounting immediately before the
held-submit → durable-ledger-append → release transaction. The
historical ledger field remains named `dependency_job_id` for compatibility, but its durable
meaning is the logical predecessor, not proof that Slurm still carried an edge.

That same-source check had a real operational cost: changing this submitter was a repository source
transition. Preparation `217768` could not be relabelled as the predecessor of training from the
new commit, even though none of its mathematical data changed. The required continuation was fresh
sealed preparation `217851`; guarded training `217859` followed without an intervening source sync.

### What “training completed” means

A Trainer return value is not itself an admissible model. In the one-pass model-v3 run, the final
manifest requires five copies of the optimizer-step count to agree: the preflight schedule,
top-level result, `TrainOutput`, `TrainerState.global_step`, and `TrainerState.max_steps`. Its
gradient callback observes the still-unincremented state at every boundary, so event $k$ must see
state $k-1$. Every raw trainable gradient must exist and be finite. Trainer's earlier permissive
clip is disabled; the callback performs the only clip with max norm $1$ and
`error_if_nonfinite=True`, checks the post-clip tensors, and retains all finite pre-clip norms.

The adapter itself supplies a second independent completion test. Before the first update and after
the last, the runner sorts the trainable names and hashes canonical records containing each name,
dtype, shape, and raw-content SHA-256. The population must remain identical, every final tensor must
be finite, and at least one tensor record must change. Thus 649 callback events around a no-op or
miswired optimizer do not become a usable adapter.

That still identifies a Python object, not the directory students will later load. Model-v3 adds a
third test: **saved-policy admission**. Before releasing the live model it chooses three
deterministic SHA-ranked probes from the admitted train and validation populations. The selection
binds the complete candidate population and the run identity, but never sees the four frozen
theorem-discovery goals. For each probe the runner stores compact fingerprints of the exact
tokenization, indexed completion loss, and projected-logit tensor. It also fingerprints PEFT's
canonical save-format tensor map, including every sorted name, dtype, shape, and raw-content hash.

The Trainer, optimizer, original tokenizer, and original model are then released. One fresh,
local-only load reconstructs the pinned Qwen commit, saved tokenizer, and single `default` adapter.
The admission gate reads the actual safetensors directly and requires three identities to agree:
the terminal in-memory PEFT population, the persisted tensor population, and the freshly populated
PEFT model. It retokenizes every probe and requires byte-exact projected logits and exact finite
losses. Finally it disables the adapter and requires at least one probe to change. This last check
distinguishes “LoRA files were attached” from “LoRA participates in the policy.” The compact result
is joined to the base configuration, run identity, `cuda:0` runtime, individual adapter files,
closed adapter/tokenizer trees, and completed-training hashes. A v3 manifest lacking any join is
not loadable.

This exact gate exposed a lifecycle distinction that tensor hashes alone could not show. In WMI
job `217123`, the terminal in-memory, saved, and freshly loaded adapter populations agreed byte for
byte, yet the semantic comparison failed. Accelerate 1.8.1 had prepared the BF16 Trainer by
mutating the live model's `forward`: it retained `_original_forward`, entered autocast, and
converted returned tensors to FP32. Releasing the Trainer did not undo that mutation. The
in-memory snapshot therefore used a prepared FP32-output path, while the newly loaded PEFT model
used bare BF16 inference. Since the fingerprint includes dtype and every raw projected-logit byte,
those outputs could never be identical.

The correction is normalization, not tolerance. Immediately after the final Trainer evaluation,
the shared helper calls Accelerate's public `unwrap_model` with
`keep_fp32_wrapper=False` and `keep_torch_compile=False`. It requires the exact same
single-process model, disappearance of `_original_forward`, and restoration of the original
forward function. Snapshot capture has a second guard against retained wrappers. Both the smoke
and the production runner now compare bare terminal inference with bare fresh inference, matching
the proof-service loader. The exact tensor, tokenization, loss/logit-byte, and
adapter-versus-disabled-base checks remain unchanged. An `allclose`, loss-only, or argmax-only fix
would have hidden the bug and weakened future corruption detection.

The lifecycle audit found why these comparisons must surround evaluation as well as saving. In the
[pinned Transformers 4.53.3 implementation](https://github.com/huggingface/transformers/blob/v4.53.3/src/transformers/trainer.py),
`bf16_full_eval=True` calls
`model.to(dtype=bfloat16)` before the full evaluation loop. PEFT 0.16 normally keeps LoRA weights in
FP32, so that flag would mutate the learned policy after its terminal fingerprint and
serialization. Production keeps BF16 autocast but pins `bf16_full_eval=False`, then fingerprints
the trainable population after serialization and again after explicit evaluation. Equality is
required at both boundaries.

The exact Trainer history has 59 periodic records at steps 11 through 649, followed by one final
training summary and one explicit validation summary, both at step 649. The interval is 11 because
the measured schedule is $649 = 11 \times 59$; this preserves the reviewed requirement that the
last optimizer update has its own periodic loss record. Extra, reordered,
non-finite, or inconsistent records are rejected. The reported `train_loss` is a mean of
optimizer-window completion-token means; with evaluation batch size one, `eval_loss` is a mean of
per-example completion-token means. These are useful diagnostics, but neither is mislabeled as the
corpus-global token NLL.

All this evidence, the observed single-GPU runtime and Trainer arguments, and the closed adapter
and tokenizer hashes enter one canonical `training_evidence` object. Model-v3 inference and the
same-base comparison validate it before importing a model framework. The strict manifest reader
rejects duplicate keys, NaN/Infinity, links, and a file that changes while being read. Earlier
prompt-v1/v2 artifacts preserve their historical contract; they cannot manufacture a v3
completion record.

Recovery publication has an environmental premise as well as a code proof. Immediately before
scheduled training, publication-preflight v2 exercises both a protected directory and a protected
regular file on the exact output filesystem. Its retained tree and exclusive report bind modes,
inodes, device, byte hashes, the attempted native syscall, and one profile selected for both node
types. The trainer includes that record in its run identity, threads the selected profile through
every authoritative publication, and checks the live probes again before final publication. This
turns “the shared filesystem probably supports our publication rule” into a tested precondition.

The preferred profile remains `renamex_np(RENAME_EXCL)` on macOS or
`renameat2(RENAME_NOREPLACE)` on Linux. WMI's Ceph filesystem returns `EINVAL` for the Linux flag.
Only `EINVAL`, `EOPNOTSUPP`/`ENOTSUP`, or `ENOSYS` permits the Linux fallback. It atomically claims
the absent final name with a type-matched empty object: an owned `0700` directory or a zero-length,
single-link `0600` regular file. Parent and claim descriptors stay open while device, inode, type,
owner, mode, and emptiness are checked, fsynced, and checked again. A descriptor-relative plain
rename then atomically replaces only that owned claim with the complete stage. Success requires
source disappearance, staging-inode continuity at the canonical name, claim-inode displacement,
and a final parent fsync.

That fallback is not mislabeled as atomic no-replace. Its claim is briefly visible, and a crash
may leave a permanent empty canonical reservation plus a complete private stage. Existence alone
is therefore never authority; all readers require the complete protected tree or canonical
manifest. Failures remain for manual audit and are never cleaned up or automatically adopted. The
last identity-check-to-rename interval is not secure against a malicious same-UID process, so the
contract explicitly retains the project's non-hostile-same-owner premise. The preflight-selected
profile is passed to run identity, recovery snapshots, adapter, tokenizer, and final manifest; a
production call never silently renegotiates it.

The corpus seal's canonical verification report uses schema v2 to make the distinction
machine-readable. It binds the admitted profile, both exercised source types, whether the final
operation had true atomic destination-no-replace semantics, and whether a transient exclusive
claim was used. Existing-report recovery recomputes that exact record from the requested profile,
so a retry cannot reinterpret claim publication as native publication (or the reverse).

Final artifacts use the same primitive rather than an overwriting library rename. The runner first
claims a fresh output directory with exclusive `mkdir` and records the output and parent devices,
inodes, and modes. Adapter and tokenizer are serialized into private `.partial-…` siblings, made
read-only, fsynced, closed-tree checked, and atomically installed without replacement. The run
identity and final manifest are exclusive read-only files; the output identity is checked again
immediately before the manifest is published. A crash may leave conspicuously partial bytes, but a
retry or competing writer cannot silently turn them into a different completed run.

“Closed tree” includes filesystem objects, not merely the files returned by a convenient glob. The
hash pass rejects symlinked components and directories, special nodes, cross-device children, and
hard links. Every file is opened with `O_NOFOLLOW` and its device, inode, mode, link count, size,
mtime, and ctime must remain equal before, during, and after descriptor-bound hashing; a second tree
inventory detects concurrent insertion. Model-v3 finalization and loading additionally require
directories to be `0555` and files `0444`. The opt-in protection rule leaves historical v1/v2
artifacts loadable under their original contract.

The mode switch is tied to semantics, not to an optional filename convention. A prompt-v3 dataset
is accepted if and only if the model-v3 curriculum is configured, and this relation is checked
before framework imports. After saved-policy admission, training repeats the protected-tree
verification at the last possible boundary before the no-replace manifest publication. Direct
inference and the pretrained-base control likewise verify the adapter and tokenizer snapshots both
before and after loading them. Recovery uses the same exact `0555`/`0444` contract. These checks
close accidental mutation and provenance gaps; they do not create a hostile-same-owner security
boundary, because such an owner can chmod and race path observations.

The relevant entry points are
[`scripts/seal_peano_v3_corpus.py`](https://github.com/nasqret/vietnam2026/blob/peano-lab/scripts/seal_peano_v3_corpus.py),
[`scripts/verify_peano_v3_corpus_eligibility.py`](https://github.com/nasqret/vietnam2026/blob/peano-lab/scripts/verify_peano_v3_corpus_eligibility.py),
[`slurm/peano_wmi_prepare_v3_sealed_training.sbatch`](https://github.com/nasqret/vietnam2026/blob/peano-lab/slurm/peano_wmi_prepare_v3_sealed_training.sbatch),
and
[`scripts/replay_peano_v3_evaluation.py`](https://github.com/nasqret/vietnam2026/blob/peano-lab/scripts/replay_peano_v3_evaluation.py).
The binding command sequence and result ledger live in
[`docs/PEANO_TRAINING.md`](https://github.com/nasqret/vietnam2026/blob/peano-lab/docs/PEANO_TRAINING.md#106-model-v3-sealed-curriculum-indexed-objective-and-launch-chain).

In the historical preparation sequence, WMI job `172729` generated both source lanes, exact-corpus
continuation `173040` completed independent attestation, token audit, and A100 runtime smoke, and
current-source seal job `213641` published the immutable corpus. A separate verifier reproduced its
content SHA-256
`7b22bdf083894e3d87b84fc463ff537a75eeecba8e34098429db215592ec6b5b`. The new sealed-
preparation job `214264` passed eligibility, deterministically selected 20,765 train rows, but
rejected their 73,446,475 tokens against the old 70-million ceiling; it produced neither an
accepted token-audit report nor a runtime-smoke report. Retry `217123` passed the 74-million token
gate and published the complete selected train/evaluation audit, then failed at the retained-
wrapper admission boundary before a runtime-smoke report. Fresh repaired preparation job `217768`
then passed the repaired smoke and all three independent report checks under source
`e0f7e7d0`. The completed-predecessor and exact-649-step fixes changed source identity, so fresh
post-fix preparation `217851` repeated and passed the complete gate under `4d44609e`. Production
optimizer `217859` then completed on an A100 and supplied the admitted adapter consumed by trained
evaluation `218171`. The paired reports exist, but the trained report's canonical replay rejection
is now covered by the passed, version-pinned historical attestation; the dedicated base attestation
also passed. The narrow launch-smoke comparison is admitted as 3/4 versus 0/4, without changing the
ordinary verifier or implying broader capability.

## Reproduction and honest resume

A checkpoint name such as `checkpoint-100` is not an identity.  M19 binds a run to:

- the resolved TOML configuration and its digest;
- train and validation bytes plus their replay manifests;
- prompt version and prompt-contract digest;
- training source-tree digest;
- base model ID and requested revision;
- LoRA and optimizer settings; and
- the declared seed.

That identity is written before training.  Automatic resume locates the newest Transformers
checkpoint only inside the output directory and accepts it only when its adjacent run identity has
the expected digest.  It records the checkpoint artifact hash and global step.  This prevents
“resume” from quietly becoming warm-starting different code, data, or hyperparameters.

WMI's managed Torch 2.5.1 cannot safely load the Trainer optimizer pickle under the selected
Transformers release, so its first pilot is deliberately one-shot. It rejects a nonempty output
directory before dataset attestation, forces safetensors for base and model-weight files, and
refuses checkpoint resume entirely. Trainer checkpoints may still contain optimizer/scheduler
`.pt` state, but WMI never loads it. The final PEFT adapter is saved directly as
`adapter_model.safetensors`; loader-visible `.bin`, `.pt`, or pickle files in that final adapter are
rejected before PEFT is imported. A failed attempt is archived or given a new run identity; it is
never silently restarted into the same directory.

After training, `training-manifest.json` records the resolved model and tokenizer snapshots, base
configuration digest, replay attestation, source and input manifests, package versions,
attention/dtype choices, resume decision, example counts, optimization metrics, every strict
gradient boundary, adapter-change fingerprints, exact log history, and live recovery-filesystem
evidence. Adapter and
tokenizer outputs live in separate **closed directories**: the manifest lists and hashes every
regular loader-visible file, and loading rejects symlinks, missing files, mutations, or an extra
unattested file.  Hashing only a familiar weight filename would not be sufficient because model
loaders also interpret configuration and tokenizer files.

Trained evaluation derives its exact `PromptEnvironment` from the dataset attestation embedded in
that training manifest.  It checks the frozen held-out contract, zero-contamination statement,
train/validation hashes, capability preimage, and versioned prompt authority before loading or
executing the adapter; it does not replace those facts with a convenient hard-coded environment.
For the historical run that means the fixed `model-v1` authority. For model-v2 it additionally
means the full checked 56-theorem identity and the separate prompt-visible statement projection;
neither may be reconstructed from an adapter label. The evaluation report then embeds the
training-manifest identity, exact decode policy, evaluator source hash, goal-set hash, seed,
budgets, complete attempted tactic sequences, and per-attempt outcomes.

### From an adapter to a new checked theorem

A benchmark-only evaluator would leave the most interesting classroom question unanswered: after
post-training, can we ask the policy to try a theorem that was not named in the frozen four-goal
report? The underlying evaluator could already accept any closed `EvalGoal`; what was missing was a
careful command-line publication boundary. The new arbitrary-theorem mode is:

```console
python3 scripts/eval_trained_peano_policy.py \
  --adapter results/peano-policy/qwen3-1.7b-lora-wmi-smoke \
  --theorem 'forall n. exists x. n * (n + 1) = 2 * x' \
  --sample --k 16 --max-steps 24 \
  --output results/peano-policy/manual-proofs/even-product.json \
  --proof-output results/peano-policy/manual-proofs/even-product.pa
```

This interface was designed by following the authority backwards. The theorem comes from the user,
but the logic mode and tactic/library capabilities come only from the adapter's attested training
environment. Version 1 therefore remains intuitionistic `model-v1`; a caller cannot make a weak
policy look stronger by enabling the full surface, importing the target, or adding `auto`. Before
loading a billion-parameter model, the command also applies the ordinary one-line, control-character,
length, numeral, parser-depth, and closed-formula checks. A default custom run makes one greedy
attempt. Asking for `k > 1` requires sampling explicitly, because repeated deterministic decoding
would consume tokens without exploring anything new.

The publication path deliberately checks more than the in-memory success flag:

1. each rollout executes one generated tactic at a time through the production surface;
2. a rollout is labelled `proof` only after the independent kernel checks its certificate against
   the owner-retained original formula;
3. among checked rollouts, the exporter deterministically chooses the least proof nodes, then the
   fewest tactic lines, then the lowest sample index;
4. those commands are replayed from a fresh state under the same exact capabilities; and
5. only matching theorem, environment, command count, proof size, and a second kernel-checked QED
   permit creation of the `.pa` file.

The result is ordinary Peano Lab source beginning with `pa prove` and ending with `qed`. Pasting it
into the lab does not trust the previous run; it reconstructs and checks the proof once again. The
JSON sidecar records the adapter, decoder, sources, scheduler identity, every failed and successful
attempt, selected sample, proof nodes, exact replay authority, and SHA-256 of the emitted script.
Existing output paths are never replaced, and repository-local output must stay under `results/`
rather than source or a closed adapter/tokenizer directory. If search finds nothing, the command
exits one and emits no proof file. Dedicated model-free regressions exercise successful replay,
forged-success rejection,
unsafe/open formula preflight, capability widening, resource bounds, source mutation, no-proof
semantics, and output non-overwrite.

WMI adds one more boundary. An ad-hoc interactive allocation would not have the required immutable
source and submission-ledger identity, while a login-node Python lacks the accepted GPU runtime.
The repository therefore transports a theorem as data, never as shell code:

```console
scripts/wmi_prove_theorem.sh \
  --submit --confirm PEANO-LAB-WMI-TRAINING \
  --theorem 'forall n. exists x. n * (n + 1) = 2 * x' \
  --sample --max-new-tokens 96 --max-steps 24 \
  --search-beam-width 8 \
  --search-candidates-per-state 16 \
  --search-max-model-calls 512 \
  --search-max-states 4096
```

This creates a version-2 canonical JSON request with a fresh nonce. Its hash commits to
kernel-guided-search mode and all six host-owned bounds: generated tokens per candidate, depth,
beam width, candidates per state, model calls, and discovered states. The wrapper streams its complete bytes under the deployment
lock; only the 64-hex request ID enters `sbatch --export`. Before the held job is released, the
controller has durably joined that ID and request hash to its Slurm job in a second ledger. The A100
job then repeats request, runtime, adapter, search-report, and kernel checks. Older version-1 request
files retain their original rollout semantics, while the new wrapper rejects the old `--k` rollout
flag instead of giving it a different meaning. Version 2 names the immutable request/search
protocol rather than a prompt version: it accepts only the exact sealed model-v2 or exact sealed
model-v3 authority recovered from the chosen adapter manifest, verifies the complete adapter and
tokenizer snapshots before and after evaluation, and
requires exact per-goal, decoder, and aggregate search accounting. Digest-named evaluation,
optional proof, and terminal summary artifacts live under `results/peano-policy/user-proofs/`.
No-proof is a valid checked search outcome; malformed provenance remains a failed job.

#### Keeping model-v3 loaded for an interactive session

The guarded one-shot WMI command targets the attested model-v3 247-theorem adapter and uses bounded
kernel-guided search. Its defaults are 96 generated tokens per candidate, depth 32, beam width 4,
four candidates per state, 128 model calls, and 2,048 states; it fails closed until that adapter
exists. The Python client remains compatible with an exact attested model-v2 adapter. A persistent
client loads one adapter once and reuses it across theorem queries:

```console
python3 scripts/peano_policy_repl.py \
  --adapter results/peano-policy/qwen3-1.7b-lora-v3-library \
  --max-new-tokens 256
```

The user may enter either a bare closed formula or `pa prove FORMULA`. For each theorem the host
runs the transactional canonical-state beam search, by default to depth 32 with beam width 4, four
candidates per state, 128 model calls, and 2,048 discovered states. A failed candidate leaves its
siblings intact. A successful search is replayed through the headless verifier from scratch, and
only that second kernel-checked result is printed and saved as an ordinary `.pa` script beside a
structured report. Unique result names and no-overwrite publication preserve previous classroom
experiments.

When local hardware cannot hold the adapter, the same persistent loop can occupy one guarded WMI
A100 allocation:

```console
scripts/wmi_peano_policy_repl.sh \
  --connect --confirm PEANO-LAB-WMI-TRAINING
```

The wrapper validates the fixed deployment/runtime before starting a four-hour interactive
allocation, and theorem text enters only after the model is resident. The earlier model-v2-heavy
adapter remains usable in place on Helios through its separate launcher, without a cross-site
artifact transfer:

```console
scripts/helios_peano_policy_repl.sh \
  --connect --confirm PEANO-LAB-TRAINING
```

That historical wrapper requests one GH200 under the fixed account and enters the same Python
client with its model-v2-heavy path; the WMI wrapper is pinned to model-v3. Both reject an
unattested adapter or the wrong surface profile. The interfaces and their model-free tests exist;
the model-v3 adapter now exists and the narrow frozen comparison has separate passed admissions,
but this interface is not evidence of broad model-v3 proof quality.
Neither interface translates English into PA, changes logic mode, or enlarges the adapter's theorem
authority.

The causal control is now a different program, not an evaluator flag. Once the model-v3 adapter
has completed, `eval_pretrained_peano_policy.py` verifies that final manifest and its closed
adapter/tokenizer trees, loads the saved tokenizer and pinned Qwen base revision, and deliberately
does not import or attach PEFT. It then runs the same four goals at seed 20260728 with depth 32,
beam 16, eight candidates per state, 512 model calls, 4,096 states, and 256 generated tokens. The
report says `peano-policy-pretrained-base-v1` and binds the comparison manifest plus both closed
tree hashes. Keeping this identity and WMI job separate prevents base-model behavior from being
misreported as adapter behavior. The trained-adapter independent replay gate remains narrow and
does not accept the control identity; a control replay attestation would be a separate protocol.
The implementation and model-free tests are complete. Control job `218172` produced a raw 0/4 at
`k=1`; its dedicated attestation passed exact identity, provenance, search-accounting, and
zero-claim validation. The paired launch-smoke comparison is therefore admitted under its two
separately scoped attestations.

Reproducible does not necessarily mean bit-identical floating-point training on every platform.
It means that any remaining nondeterminism is bounded and visible, and that nobody can mistake a
different model, environment, dataset, or checkpoint for the same experiment.

## Limitations and the next honest claims

The current work establishes that one small trained adapter can emit several shallow checked
proofs, but not that it is broadly useful for PA or capable of non-trivial induction. Important
limitations remain:

- the model-v3 adapter exists, and the separately admitted four-goal `k=1` launch smoke is 3/4
  versus 0/4; the ordinary trained-report replay still rejects four omitted library-prefix identity
  fields, while the version-pinned historical bridge validates this exact immutable report rather
  than weakening that rule;
- model-v3's 247-theorem identity, strict predecessor-prefix generator, 51-schema root-balanced
  generator, whole-session selector, indexed completion objective, immutable-seal/current-source
  eligibility gate, and independent evaluation replay are implemented; retry `172729`, continuation
  `173040`, and seal job `213641` produced and authenticated the complete immutable corpus; job
  `214264` then failed the old 70-million linear-token gate at 73,446,475 tokens; retry `217123`
  passed all token gates but exposed a retained Accelerate forward wrapper at saved-policy
  admission; after the completed-predecessor repair, fresh same-source preparation `217851` passed
  eligibility, the exact token audit, repaired runtime smoke, and independent three-report
  verification; production optimizer job `217859` then completed, and paired evaluation jobs
  `218171`/`218172` produced the separately attested launch-smoke reports described above;
- the four-goal protocol set is a regression fixture, not a statistically useful final test, and
  hard whole-template OOD sets plus human-authored problems still need to be sealed;
- depth-32 verifier-guided beam search ran in the four-goal smoke, but its gain over a trained
  greedy/rollout condition has not been isolated and no expert-iteration round exists;
- no preference-training or reinforcement-learning result exists;
- no English-to-PA formalizer has been trained or semantically evaluated;
- the full content-bound library identity, prompt projection, and retrieval are implemented, but
  their usefulness remains an empirical question; and
- a revision/configuration-pinned pretrained comparison reporting no PEFT adapter now accompanies
  the four-goal smoke, but weight-shard and raw-generation transcript attestation, a deterministic
  baseline, larger hidden suite, repeated runs, all LoRA-rank studies, and 4B comparisons remain
  outstanding.

The valid statement is therefore not “Peano Lab has a theorem-proving model.” It is narrower: one
one 1.7B model-v3 adapter produced three independently kernel-valid shallow scripts in a frozen
four-goal run where a revision/configuration-pinned pretrained comparison reporting no PEFT adapter
produced none, but it did not solve the induction goal. The 3/4-versus-0/4 result is admitted only
through separately scoped, immutable attestations;
the ordinary trained-report replay still rejects its historical identity defect. Larger conclusions
must be earned by hidden family splits, deterministic and search comparisons, repeated
measurements, and harder induction-rich problems.

That restraint is the main pedagogical result.  A learned explorer can be cheap, fast, and
surprisingly inventive.  Its suggestions remain suggestions.  Peano Lab's kernel decides theorems,
and the experiment's manifests decide what scientific comparison was actually made.