Raw rich-chip divisors on closed faces

The RPF representation stores chips as raw (slot, affine form, coefficient) triples. A rich-leaf soundness proof evaluates the forms and supplies a closed-face vertex decoder (with the C first-match convention). This module is deliberately agnostic about that decoder: it packages the resulting chip divisor and its degree calculation once, so the endpoint-specific decoder is the only remaining W5 geometry.

def Utilities.Subdivision.ClosedRowProof.RichWitness.rawChipMassAt (w : RichWitness) (x : List ℤ) (slot : ℕ) (coordinate : ℤ) : ℤ

Raw signed chip mass at a literal coordinate of one displayed slot. Unlike a quotient-core vertex, this remains meaningful before any zero-length core edges are contracted. The W5 endpoint bridge identifies this mass with the C first-match prefix/suffix accounting on collapsed endpoint runs.

Equations

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

Evaluated physical chip positions

Raw RPF forms denote positions by evaluation at the current parameter point. The decoder below clamps only to make it total; W1 and W3 later prove that every accepted chip already lies in the displayed closed interval, so the clamp is definitionally inactive on actual leaf data.

def Utilities.Subdivision.ClosedRowProof.RichWitness.evaluatedPathVertex {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (edge : Fin p) (coordinate : ℤ) : d.Vertex

Decode an integer coordinate on one slot to its closed-face path vertex. The min is a totality device for this standalone definition, not a semantic relaxation: evaluatedPathVertex_eq_pathVertex removes it under the W1/W3 bounds supplied by an accepted rich leaf.

Equations

• Utilities.Subdivision.ClosedRowProof.RichWitness.evaluatedPathVertex d edge coordinate = d.pathVertex edge ⟨min coordinate.toNat (d.length edge), ⋯⟩

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.evaluatedPathVertex_eq_pathVertex {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (edge : Fin p) (coordinate : ℤ) (hUpper : coordinate ≤ ↑(d.length edge)) : evaluatedPathVertex d edge coordinate = d.pathVertex edge ⟨coordinate.toNat, ⋯⟩

Under the natural closed-interval bounds, evaluating a form uses its literal integer position rather than the total decoder's clamp.

def Utilities.Subdivision.ClosedRowProof.RichWitness.evaluatedChipVertex {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (fallback : Fin n) (x : List ℤ) (slot : ℕ) (form : Form) : d.Vertex

A total raw-chip decoder. The fallback is used only for malformed slot indices; w3Checks proves those cannot occur in an accepted witness.

Equations

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

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.evaluatedChipVertex_of_slot_lt {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (fallback : Fin n) (x : List ℤ) (slot : ℕ) (form : Form) (hslot : slot < p) : evaluatedChipVertex d fallback x slot form = evaluatedPathVertex d ⟨slot, hslot⟩ (eval form x)

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.evaluatedChipVertex_eq_namedPathVertex {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (fallback : Fin n) (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) {chip : ℕ × Form × ℤ} (hchip : chip ∈ w.chips) : ∃ (i : Fin ((w.blockList (↑a) chip.1).length - 1)), evaluatedChipVertex d fallback x chip.1 chip.2.1 = d.pathVertex ⟨chip.1, ⋯⟩ ⟨(w.pointValue x (↑a) chip.1 (↑i + 1)).toNat, ⋯⟩

On an accepted rich leaf, a raw chip's physical decoded vertex is exactly the path vertex of its W3-named endpoint. W1 supplies the interval bounds that make the total decoder's clamp inactive.

Core divisor on a contracted face

The rich RPF divisor is written on the uncontracted core. On a closed face its coefficients must be summed over each quotient class, exactly as for the existing explicit-potential certificate. Keeping this operation next to the raw chip divisor makes the final degree calculation independent of the W5 endpoint accounting.

def Utilities.Subdivision.ClosedRowProof.RichWitness.richCoreDivisor {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) : CFDiv d.graph

Push the raw core coefficient list to the quotient core of a degenerate subdivision; interior vertices receive no core coefficient.

Equations

• Utilities.Subdivision.ClosedRowProof.RichWitness.richCoreDivisor d w (Sum.inl c) = ∑ v : Fin n with d.rep v = ↑c, w.divisorCore.getD (↑v) 0
• Utilities.Subdivision.ClosedRowProof.RichWitness.richCoreDivisor d w (Sum.inr val) = 0

@[simp]

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.richCoreDivisor_coreVertex {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (r : Fin n) : richCoreDivisor d w (d.coreVertex r) = ∑ v : Fin n with d.rep v = d.rep r, w.divisorCore.getD (↑v) 0

@[simp]

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.richCoreDivisor_interiorVertex {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (e : Fin p) (o : Fin (d.length e - 1)) : richCoreDivisor d w (d.interiorVertex e o) = 0

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.deg_richCoreDivisor {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) : CFDiv.degree (richCoreDivisor d w) = ∑ v : Fin n, w.divisorCore.getD (↑v) 0

Quotienting the core cannot change its total degree.

C first-match chip accounting

rawChipDivisor deliberately decodes a chip by its evaluated physical position. The checker, on the other hand, uses syntactic named endpoints to assign a chip to the first matching interior point. The following small list layer exposes that assignment as an ordinary sum of indicator terms. It is independent of the closed-face geometry and is consequently reusable both for W4 runs and for W5 endpoint prefixes/suffixes.

def Utilities.Subdivision.ClosedRowProof.RichWitness.chipMatches (w : RichWitness) (a e i : ℕ) (c : ℕ × Form × ℤ) : Bool

The Boolean predicate by which the C checker assigns a raw chip to a named point. The range (i - 1) clause makes this the first syntactic match; index zero is excluded separately by chipAt.

Equations

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

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.chipAt_eq_indicator_sum (w : RichWitness) (a e i : ℕ) (hi : i ≠ 0) : w.chipAt a e i = (List.map (fun (c : ℕ × Form × ℤ) => if w.chipMatches a e i c = true then c.2.2 else 0) w.chips).sum

At every nonzero named index, chipAt is exactly the sum of coefficients of raw chips whose first syntactic match is that index.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.chipPrefix_eq_indicator_sum (w : RichWitness) (a e s : ℕ) : w.chipPrefix a e s = List.foldl (fun (z : ℤ) (i : ℕ) => z + if i = 0 then 0 else (List.map (fun (c : ℕ × Form × ℤ) => if w.chipMatches a e i c = true then c.2.2 else 0) w.chips).sum) 0 (List.range (s + 1))

The inclusive named-point sum used in chipPrefix has an explicit raw chip indicator expansion. Index zero contributes nothing, so this remains valid even for the tail candidate s = 0.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.headChipSum_eq_indicator_sum (w : RichWitness) (a e s : ℕ) : List.foldl (fun (z : ℤ) (t : ℕ) => if t = 0 then z else z + w.chipAt a e ((w.blockList a e).length - t)) 0 (List.range (s + 1)) = List.foldl (fun (z : ℤ) (t : ℕ) => if t = 0 then z else z + if (w.blockList a e).length - t = 0 then 0 else (List.map (fun (c : ℕ × Form × ℤ) => if w.chipMatches a e ((w.blockList a e).length - t) c = true then c.2.2 else 0) w.chips).sum) 0 (List.range (s + 1))

The head-side named-point sum used by headCandidate, before subtracting the block-slope bound, likewise expands into first-match chip indicators.

def Utilities.Subdivision.ClosedRowProof.RichWitness.rawChipDivisor {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (decode : ℕ → Form → d.Vertex) : CFDiv d.graph

The divisor represented by raw RPF chips once their slot/form positions have been decoded on a particular closed face.

Equations

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

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.rawChipDivisor_apply {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (decode : ℕ → Form → d.Vertex) (vertex : d.Vertex) : rawChipDivisor d w decode vertex = (List.map (fun (chip : ℕ × Form × ℤ) => if decode chip.1 chip.2.1 = vertex then chip.2.2 else 0) w.chips).sum

Pointwise coefficient formula for decoded raw chips. The endpoint-specific decoder instantiation will identify the right side with W5's first-matched prefix/suffix sums.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.evaluatedRawChipDivisor_apply_interiorVertex {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (fallback : Fin n) (x : List ℤ) (e : Fin p) (o : Fin (d.length e - 1)) : rawChipDivisor d w (evaluatedChipVertex d fallback x) (d.interiorVertex e o) = (List.map (fun (chip : ℕ × Form × ℤ) => if evaluatedChipVertex d fallback x chip.1 chip.2.1 = d.interiorVertex e o then chip.2.2 else 0) w.chips).sum

Exact raw-list coefficient formula at an interior vertex of a closed face. Instantiating decode with evaluatedChipVertex is the row-local bridge needed by W4: it says that the only remaining geometric question is which named endpoints evaluate to this particular interior offset. No injectivity of pathVertex is assumed (and none is available on a closed face).

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.deg_rawChipDivisor {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (decode : ℕ → Form → d.Vertex) : CFDiv.degree (rawChipDivisor d w decode) = (List.map (fun (chip : ℕ × Form × ℤ) => chip.2.2) w.chips).sum

Decoding positions cannot change degree: every raw coefficient contributes exactly once. In particular this is compatible with chips collapsing onto a core class.