Rich Leaf Assembly

theorem finRange_map_sum {p : ℕ} (f : Fin p → ℤ) : (List.map f (List.finRange p)).sum = ∑ e : Fin p, f e

theorem foldl_finRange_add {p : ℕ} (f : Fin p → ℤ) : List.foldl (fun (z : ℤ) (e : Fin p) => z + f e) 0 (List.finRange p) = ∑ e : Fin p, f e

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.selectedBlock_intervalLength {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hx : Γ.Holds x) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(d.length e)) (a : Fin n) (e : Fin p) (k : ℕ) (hk : k < d.length e) : have b := richBlockEnds d w core Γ x hW1 hx hCoord a e; ↑(b.endAt (b.blockAt k) - b.startAt (b.blockAt k)) = w.blockLengthValue x (↑a) (↑e) (b.blockAt k)

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.rich_blockSlope_bounds {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hW2 : w.w2Checks core Γ = true) (hx : Γ.Holds x) (ℓ : Fin p → ℕ) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(ℓ e)) (hn : 0 < n) (hForest : Certificate.ContractionForestCensusGeneral.IsForest core (zeroSet ℓ)) (hNotLoopy : ¬Certificate.ContractionForestCensusGeneral.IsLoopy core (zeroSet ℓ)) (a : Fin n) (e : Fin p) (k : ℕ) (hk : k < d.length e) (hd : d = censusSpec core hn ℓ hForest hNotLoopy) : have data := w.richCensusPiecewiseData core Γ x hW1 hW2 hx ℓ hCoord hn hForest hNotLoopy a; (w.block (↑a) (↑e) (data.blockAt e k)).lo ≤ Certificate.DegenerateSpec.DegSpec.blockSlope data.blockAt data.blockEnd data.blockRise e k ∧ Certificate.DegenerateSpec.DegSpec.blockSlope data.blockAt data.blockEnd data.blockRise e k ≤ (w.block (↑a) (↑e) (data.blockAt e k)).hi

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.rawChipMassAt_selectorChange {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hW3 : w.w3Checks core = true) (hx : Γ.Holds x) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(d.length e)) (a : Fin n) (e : Fin p) (o : Fin (d.length e - 1)) (hChange : (richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt ↑o < (richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt (↑o + 1)) : w.rawChipMassAt x (↑e) (↑↑o + 1) = w4ChipSum (fun (t : ℕ) => w.chipAt (↑a) (↑e) t) ((richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt ↑o + 1) ((richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt (↑o + 1))

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.rawChipMassAt_eq_zero_of_sameSelector {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hW3 : w.w3Checks core = true) (hx : Γ.Holds x) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(d.length e)) (a : Fin n) (e : Fin p) (o : Fin (d.length e - 1)) (hSame : (richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt ↑o = (richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt (↑o + 1)) : w.rawChipMassAt x (↑e) (↑↑o + 1) = 0

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.blockList_length_eq_one_of_coord_eq_zero {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hW3 : w.w3Checks core = true) (hx : Γ.Holds x) (a : Fin n) (e : Fin p) (hcoord : eval (coordForm ↑e) x = 0) : (w.blockList ↑a ↑e).length = 1

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.tail_blockAt_eq_collapse {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hx : Γ.Holds x) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(d.length e)) (a : Fin n) (e : Fin p) (hpos : 0 < d.length e) (s : ℕ) (hs : s ≤ (w.blockList ↑a ↑e).length - 1) (hzero : w.pointValue x (↑a) (↑e) s = 0) (hmax : ∀ (i : ℕ), s < i → i ≤ (w.blockList ↑a ↑e).length - 1 → w.pointValue x (↑a) (↑e) i ≠ 0) : (richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt 0 = s

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.head_blockAt_eq_collapse {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hx : Γ.Holds x) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(d.length e)) (a : Fin n) (e : Fin p) (hpos : 0 < d.length e) (s : ℕ) (hs : s ≤ (w.blockList ↑a ↑e).length - 1) (hhead : w.pointValue x (↑a) (↑e) ((w.blockList ↑a ↑e).length - s) = eval (coordForm ↑e) x) (hlow : ∀ (i : ℕ), 1 ≤ i → i < (w.blockList ↑a ↑e).length - s → w.pointValue x (↑a) (↑e) i ≠ eval (coordForm ↑e) x) : (richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt (d.length e - 1) = (w.blockList ↑a ↑e).length - 1 - s

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.classSum_w5ActualResidual_eq {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (mult : ℤ) (a : Fin n) (tail head : Fin p → ℤ) (r : Fin n) : ∑ v : Fin n with d.rep v = d.rep r, w.w5ActualResidual core mult a tail head v = (∑ v : Fin n with d.rep v = d.rep r, w.divisorCore.getD (↑v) 0 - if d.rep a = d.rep r then mult else 0) + ∑ e : Fin p, ((if d.rep (core.tail e) = d.rep r then tail e else 0) + if d.rep (core.head e) = d.rep r then head e else 0)

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.richDivisor_winnable_sub_smul {n p : ℕ} (core : Certificate.ExplicitPotential.Core n p) (w : RichWitness) (Γ : Context) (hn : 0 < n) (x : List ℤ) (hx : Γ.Holds x) (hW1 : w.w1Checks core Γ = true) (hW2 : w.w2Checks core Γ = true) (hW3 : w.w3Checks core = true) (hW4 : w.w4Checks 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) (mult : ℤ) (anchor : Fin n) (hW5m : ∀ (v : Fin n), 0 ≤ w.w5MultResidual core mult ↑anchor ↑v) : winnable (censusSpec core hn ℓ hForest hNotLoopy).graph (richDivisor (censusSpec core hn ℓ hForest hNotLoopy) w fallback x - mult • oneChip ((censusSpec core hn ℓ hForest hNotLoopy).coreVertex anchor))

The rich leaf's script reaches its plan's vertex, at any multiplicity.

The body of this lemma used to sit inline inside richLeaf_sound, specialised to one chip. It is stated for mult chips because a legged rich leaf needs exactly the same argument at the doubled anchor: mult = 1 is a rank anchor, mult = m is the (comp x …) plan certifying D − m·1_x winnable. Nothing in the argument cared how many chips were withdrawn — only that W5 stays nonnegative after withdrawing them, which is the hW5m hypothesis.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.richLeaf_sound {m n p : ℕ} (core : Certificate.ExplicitPotential.Core n p) (w : RichWitness) (Γ : Context) (degree : ℤ) (hp : p ≤ m) (hn : 0 < n) (hchk : w.richLeafChecks m core Γ degree = true) (point : Fin m → ℤ) (hΓ : Γ.Holds (List.ofFn point)) (ℓ : Fin p → ℕ) (hlen : ∀ (e : Fin p), ↑(ℓ e) = point (Fin.castLE hp e)) (hForest : Certificate.ContractionForestCensusGeneral.IsForest core (zeroSet ℓ)) (hNotLoopy : ¬Certificate.ContractionForestCensusGeneral.IsLoopy core (zeroSet ℓ)) : BNExists (censusSpec core hn ℓ hForest hNotLoopy).graph 1 degree