Probe the decision,
not the goal.

Every readout is leave-one-out; chance is a shuffled-label control; the surface-literal baseline is reported first. Same corpus, same whitened head — the only thing that changes is where in the proof we read the model.

Abstract proof concepts are linearly readable off the frozen prover with no training. Domain (topic) reads at 0.95; tactic (proof structure, from the statement) at 0.73 — both far above surface literal and chance. On a goal property the prover's edge over a general encoder is small; the large edge lives in the decision state (§01).

Concepts sit at modestly different depths, with different shapes. Domain is a sharp early-mid peak at L10; tactic-from-statement is a broad, flat plateau across L12–20; the tactic decision state rises with depth to 0.867 at L20. Proof structure is read a little deeper than topic, and more diffusely.

No projection, no dimensionality reduction. Each panel is the real activation matrix at its exact width — one row per proof sample, one column per channel (9728 wide at the MLP gate). Rows are grouped by class. Switch the frame to subtract the always-on component (including the massive-activation sink) and watch the class structure surface; scrub the layer and watch the depth-map finding happen.

How to read it: in per-channel and per-class frames, blue is below and orange above the subtracted mean. In domain, the six math-topic bands separate most crisply around L10 and soften by L35. In tactic · decision, the five-tactic bands are faint at L8 and sharpen climbing to L20 — the model committing to its tactic. The same tactic read from the statement (last track) shows far weaker banding: the goal doesn't carry the decision.

Domain reads well across attention / MLP / gate at the early-mid block — there is no single magic site. This is the coarse nearest-centroid locator over all 10 sites × 36 layers (chance 0.167); its one hotspot is attention-write at L24.

At the located sites the canonical frame fits at 100% energy, quantizes on the lattice q=(3,5,7,11), and passes a byte-equal replay gate with a tamper-evident certificate — a doctored bin is rejected.

• Read-only. Classify + retrieve + refuse. No causal / editing (Option E) and no native-replacement claim.
• The model beating a text encoder at predicting its own next tactic is partly expected — it is what generates it. The interpretability content is that the decision is linear and mid-network, +0.224 above the surface.
• Per-sample, not per-token. The raster axis is samples grouped by class (last token of the statement, or the decision position mid-proof) — not a token-by-token scrub within one prompt.
• No attention internals. These are the 10 block-boundary sites; per-head Q 12×128 / KV 2×128 (GQA) anatomy would need a re-capture. Shown dim in the site rail rather than faked.
• Small curated sets — 480 domain / 495 tactic (statement) / 750 decision points, one prover. Decision layers {8,10,12,14,16,20}; 24–35 left unprobed to avoid the near-tautological logit regime.
• The whitened head is label-supervised in its metric only; the retrieval and continuum results are label-free.