The divisor denoted by a rich row-proof leaf

This module isolates the representation-independent divisor and degree calculation from the closed-face soundness assembly.

def Utilities.Subdivision.ClosedRowProof.RichWitness.richDivisor {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (fallback : Fin n) (x : List ℤ) : CFDiv d.graph

The divisor denoted by a rich witness on a particular closed face: raw core coefficients are pushed to quotient classes and raw chip forms are evaluated at their physical subdivision positions.

Equations

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

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.deg_richDivisor {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (fallback : Fin n) (x : List ℤ) : CFDiv.degree (richDivisor d w fallback x) = ∑ v : Fin n, w.divisorCore.getD (↑v) 0 + (List.map (fun (chip : ℕ × Form × ℤ) => chip.2.2) w.chips).sum

Evaluation and contraction preserve the witness's declared total degree.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.sum_getD_eq_list_sum (xs : List ℤ) (n : ℕ) (hLength : xs.length = n) : ∑ v : Fin n, xs.getD (↑v) 0 = xs.sum

A finite getD sum agrees with the list sum when the list has the declared core length.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.deg_richDivisor_eq_declared {n p : ℕ} {degree : ℤ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (fallback : Fin n) (x : List ℤ) (hLength : w.divisorCore.length = n) (hDegree : List.foldl (fun (x1 x2 : ℤ) => x1 + x2) 0 w.divisorCore + List.foldl (fun (z : ℤ) (c : ℕ × Form × ℤ) => z + c.2.2) 0 w.chips = degree) : CFDiv.degree (richDivisor d w fallback x) = degree

W7 turns the representation-independent degree calculation into the degree declared by the rich leaf.