Marked leaf checkers: domination, multiplicity residuals, legged and pointed leaves

The generic row-proof checker in this directory validates a leaf against the five closed-face rows W1–W5 plus the degree row W7. A leaf that also carries a mark — a distinguished core vertex at which the divisor must dominate, or at which a residual must be read with multiplicity greater than one — needs two more executable rows, and a leaf carrying two marks (a "legged" leaf, in the vocabulary of the once- and twice-marked programmes) needs one more table per mark.

Those rows were written privately, one copy per marked programme, on top of a private duplicate of this checker. They are generic: nothing below mentions a genus, a row, or a marked-graph existence statement. They belong here, beside the checker they extend, so that the checker's namespace stays self-contained in its own directory.

What is here, and what deliberately is not

• the four leaf checkers, assembled from the two doubled-anchor rows in Utilities/Subdivision/DoubledAnchorChecks.lean: Witness.leggedLeafChecks, Witness.pointedLeafChecks, RichWitness.pointedLeafChecks, RichWitness.richLeggedLeafChecks;
• RichWitness.richDivisor_rank_ge_one, the strong-separator half of richLeaf_sound stated for the divisor rather than for BNExists, because a legged leaf needs the divisor itself.

Not here, by design: the soundness theorems that consume these rows — effective_degenerateDivisor_sub_smul_one_chip, class_mult_balance_nonnegative, winnable_sub_smul_one_chip_degenerateCoreVertex and the marked-completion bridges. They are heavier, they are consumed only by the marked programmes, and promoting them would buy nothing here. They stay in MarkedGraphs/Certificate/DegenerateDoubledAnchor.lean, which imports this file.

Why the checkers and not just the definitions

Witness and RichWitness are the structures declared in this directory. Dot notation resolves w.leggedLeafChecks in the namespace of w's type, so a checker written elsewhere is invisible to w.leggedLeafChecks however the file is imported. Keeping these four here is what lets the marked programmes consume the row-proof checker without maintaining a second copy of it.

Compact marked leaves

def Utilities.Subdivision.ClosedRowProof.Witness.leggedLeafChecks {n p : ℕ} (w : Witness) (m : ℕ) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (degree : ℤ) (mark attachment : Fin n) (chips mult : ℤ) : Bool

The legged leaf checker. Witness.leafChecks plus the goal's two extra rows: W7's domination at the first mark (chips chips) and the (comp x …) plan's W5 at multiplicity mult at the second.

Both extra rows are point-independent tests on the certificate's own core divisor, so an emitter discharges them by decide.

Equations

• One or more equations did not get rendered due to their size.

def Utilities.Subdivision.ClosedRowProof.Witness.pointedLeafChecks {n p : ℕ} (w : Witness) (M : ℕ) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (degree : ℤ) (mark : Fin n) (mult : ℤ) : Bool

Compact pointed checker: the ordinary rank-one leaf plus the same plan at the marked core vertex checked with multiplicity mult.

Equations

• w.pointedLeafChecks M core Γ degree mark mult = (w.leafChecks M core Γ degree && (Utilities.Subdivision.ClosedRowProof.leafCertificate M core w).multResidualCheck mult mark)

Rich marked leaves

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.richDivisor_rank_ge_one {n p : ℕ} (core : Certificate.ExplicitPotential.Core n p) (w : RichWitness) (Γ : Context) (hn : 0 < n) (x : List ℤ) (hx : Γ.Holds x) (hConnected : core.connectedCheck = true) (hW1 : w.w1Checks core Γ = true) (hW2 : w.w2Checks core Γ = true) (hW3 : w.w3Checks core = true) (hW4 : w.w4Checks core Γ = true) (hW5 : w.w5Checks core = true) (ℓ : Fin p → ℕ) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(ℓ e)) (hForest : Certificate.ContractionForestCensusGeneral.IsForest core (zeroSet ℓ)) (hNotLoopy : ¬Certificate.ContractionForestCensusGeneral.IsLoopy core (zeroSet ℓ)) (fallback : Fin n) : rank (censusSpec core hn ℓ hForest hNotLoopy).graph (richDivisor (censusSpec core hn ℓ hForest hNotLoopy) w fallback x) ≥ 1

The rich divisor has rank at least one, by the strong separator over the n rank anchors. This is richLeaf_sound's second half, kept as its own statement because a marked leaf needs the divisor and not just BNExists.

def Utilities.Subdivision.ClosedRowProof.RichWitness.pointedLeafChecks {n p : ℕ} (w : RichWitness) (M : ℕ) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (degree : ℤ) (mark : Fin n) (mult : ℤ) : Bool

Rich pointed checker. The ordinary W1--W5 leaf supplies rank one; one additional W5 table reads the marked plan with multiplicity mult.

Equations

• w.pointedLeafChecks M core Γ degree mark mult = (w.richLeafChecks M core Γ degree && w.w5MultChecks core mult ↑mark)

def Utilities.Subdivision.ClosedRowProof.RichWitness.richLeggedLeafChecks {n p : ℕ} (w : RichWitness) (M : ℕ) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (degree : ℤ) (mark attachment : Fin n) (chips mult : ℤ) : Bool

The legged rich leaf checker. richLeafChecks plus one W5 table per mark, at the mark's own multiplicity.

There is deliberately no W7 domination row: the first mark's obligation is supplied as winnability by its own W5 table. Compare Witness.leggedLeafChecks, which does carry a domination row because the compact leaf's divisor is available pointwise.

Equations

• w.richLeggedLeafChecks M core Γ degree mark attachment chips mult = (w.richLeafChecks M core Γ degree && w.w5MultChecks core chips ↑mark && w.w5MultChecks core mult ↑attachment)