The row-proof tree layer, deep-embedded #

Step C of the proof-data source needs a way to lower a SPLIT node. NEXT.md proposed lowering it shallowly, as a generated rcases le_or_gt; this file takes the deep-embedded route instead, for the same reason the corresponding closed-row proof module deep-embeds the arithmetic:

the whole tree becomes one piece of data and one decide, instead of one decide per leaf plus a generated tactic script whose size is the number of nodes — for g4row099 that is 64 leaves and 63 splits;
the accumulated context at a leaf is computed by PTree.checks rather than transcribed by the emitter, so the emitter cannot get it wrong;
the rcases le_or_gt of the shallow plan survives verbatim, once, inside PTree.sound below, where it is proved rather than generated.

The tree layer is deliberately minimal: SPLIT, LEAF, USE, AUTO, ABSURD, and the one REDUCE opcode whose Lean theorem exists on the closed orthant, REDUCE CUTVERTEX. Spec §4.2's other opcodes (SPLIT3, MOD, CITE, and the other REDUCE operations) are absent on purpose — spec §13.6's rule is that a node shape is a reject until its Lean theorem exists, and adding a constructor here with no soundness case would break PTree.sound rather than silently weaken it.

`ABSURD` #

(absurd cert) discharges an empty cell: cert is a Farkas derivation of −1 ≥ 0 from the accumulated context, so no point satisfies the context and the row's conclusion holds there vacuously. This is the same Cert and the same Cert.check_sound as everywhere else — the only novelty is that the form entailed is the constant falseForm = −1 rather than something the leaf needs.

It is not a luxury. Splitting a chamber finely produces empty cells as the normal case, so a cover of any size contains them in quantity; a tree layer without ABSURD can only lower covers that were pruned by hand.

AUTO is closed-face sound, not merely an interior-cone shortcut. Its raw permutations are checked against the core, its context forms are pulled back by the slot permutation, and ClosedAuto.bnExists_iff transports through the quotient classes created by zero slots. Named-subtree soundness is therefore kept uniform in the length vector: an auto-wrapped use may invoke the same subtree at the reindexed metric and then transport the result back.

`USE`, and the shape change it forces #

(use k cert_0 … cert_{m-1}) cites the earlier named subtree k. A subtree carries an entry context — a list of forms it may assume on top of the root domain — and the citing node must show that the context accumulated at the citation entails every one of them. That is pure context weakening, and Cert.check_sound is exactly the entailment half of it.

So use cannot be checked against a tree alone: the checker has to know what the earlier subtrees claim. PTree.checksIn therefore threads a list E of entry contexts, PProof bundles an ordered list of subtrees with a main tree, and subsCheck walks the subtrees in order, each seeing only its predecessors. That ordering is what makes the recursion well-founded and is verbatim rpfcheck.c's "use must reference an earlier subtree".

PTree.checks is kept as the E = [] specialisation, so a proof with no subtrees — every row in the catalog that predates this — lowers to exactly the same term it did before.

The payoff is that a chamber cover whose cells reuse the same local witness stores and checks that witness once: on row 099 the 64 materialized leaves become 15 subtrees plus 64 entailment citations.

`REDUCE CUTVERTEX` #

(reduce cutvertex v c_0 … c_{p-1}) names an articulation vertex v and two-colours the slots. the proof-data source verifies that the colouring really does split the core at v into two connected positive-genus factors meeting only there, and then cites the factorwise gluing theorem. On the Lean side that citation is RowProof.bnExists_censusSpec_of_genusFourRankOneCheck, the closed-orthant port of Certificate/CoreVertexCutGenusFour.lean's theorem, whose conclusion is verbatim PTree.sound's at degree = 3.

Three things make the fit exact rather than approximate.

The Lean checker is CoreVertexCut.Data.genusFourRankOneCheck, which re-derives the cut, the two factor genera, and — on a genus-one factor — the two-regularity that PointedGenusOneRigid needs. The colouring is not trusted: CutData carries raw ℕs, toCut decodes them totally, and the checker validates the decoding. A .rpf colouring that does not in fact cut the core is simply rejected by decide.
The gluing theorem is specific to degree = 3, unlike the rest of PTree.sound, which is generic in degree. CutData.checks therefore demands degree = 3 outright rather than papering over the difference.
The node's conclusion is unconditional — it holds on the whole closed orthant — so CutData.checks ignores the accumulated context Γ. That is sound in the safe direction: the node proves more than its chamber needs.

The context discipline #

SPLIT g pushes g in the first branch and −1 − g in the second; over the integers those are exhaustive, and that is the entire coverage argument (spec §4.2). New rows are appended at the end of Γ.ge, so a context row's index never changes as the tree descends: at a leaf of a depth-k branch the root's p coordinate rows still sit at indices 0 … p−1 and the branch conditions at p … p+k−1. That stability is what lets the emitter address context rows by a fixed index in every certificate it synthesises.

The row-proof tree layer, deep-embedded #

ABSURD #

USE, and the shape change it forces #

REDUCE CUTVERTEX #

The context discipline #

The REDUCE CUTVERTEX node #

Subtrees and their entry contexts #

`ABSURD` #

`USE`, and the shape change it forces #

`REDUCE CUTVERTEX` #

The `REDUCE CUTVERTEX` node #