Where a raw rich chip actually lands on a closed face

RichChipDecoder turns the raw (slot, form, coefficient) triples into a divisor by evaluating each form and reading off pathVertex. RichChipBridge identifies the physical mass at a coordinate with the checker's syntactic first-match accounting. What is still missing between them is purely the closed-face trichotomy: which coordinate of which slot is which vertex.

That is this module. It has no arithmetic content; it is the pathVertex case split (0 / length / interior) pushed through rawChipDivisor_apply.

The one place it is not a triviality is the head mass on a collapsed slot. When length e = 0 the two endpoints of the slot are the same vertex, so adding a tail term and a head term would count a chip there twice. headMassAdj suppresses the head term exactly there; RichChipBridge's rawChipMassAt_eq_zero_of_coord_eq_zero says the suppressed value was 0 anyway, so nothing is lost.

Vertex identities on a degenerate subdivision

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.interiorVertex_ne_coreVertex {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (e : Fin p) (o : Fin (d.length e - 1)) (r : Fin n) : d.interiorVertex e o ≠ d.coreVertex r

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.interiorVertex_inj {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) {s e : Fin p} {u : Fin (d.length s - 1)} {o : Fin (d.length e - 1)} (h : d.interiorVertex s u = d.interiorVertex e o) : s = e ∧ ↑u = ↑o

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.pathVertex_congr {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) {s e : Fin p} (hse : s = e) {k : d.PathPosition s} {k' : d.PathPosition e} (hk : ↑k = ↑k') : d.pathVertex s k = d.pathVertex e k'

Path vertices are determined by slot and position. This tiny lemma is the only place the dependency of PathPosition on the slot has to be substituted away.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.pathVertex_eq_interiorVertex {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (e : Fin p) (k : d.PathPosition e) (o : Fin (d.length e - 1)) (hval : ↑k = ↑o + 1) : d.pathVertex e k = d.interiorVertex e o

On its own slot, the path vertex one past an interior offset is that interior vertex.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.slot_eq_of_pathVertex_eq_interiorVertex {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) {s e : Fin p} {k : d.PathPosition s} {o : Fin (d.length e - 1)} (h : d.pathVertex s k = d.interiorVertex e o) : s = e ∧ ↑k = ↑o + 1

Conversely, a path vertex which is an interior vertex names its own slot and offset.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.pathVertex_eq_coreVertex_iff {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (s : Fin p) (k : d.PathPosition s) (r : Fin n) : d.pathVertex s k = d.coreVertex r ↔ ↑k = 0 ∧ d.rep (d.core.tail s) = d.rep r ∨ ↑k ≠ 0 ∧ ↑k = d.length s ∧ d.rep (d.core.head s) = d.rep r

The core-class half of the same trichotomy.

The evaluated decoder, resolved

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.chip_eval_mem_Icc {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) {chip : ℕ × Form × ℤ} (hchip : chip ∈ w.chips) (hslot : chip.1 < p) : 0 ≤ eval chip.2.1 x ∧ eval chip.2.1 x ≤ ↑(d.length ⟨chip.1, hslot⟩)

Every raw chip of an accepted rich leaf evaluates into the closed interval of its own slot. This is the hypothesis both placement lemmas need in order to remove the total decoder's clamp.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.evaluatedChipVertex_eq_pathVertex {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (fallback : Fin n) (x : List ℤ) {chip : ℕ × Form × ℤ} (hslot : chip.1 < p) (hUpper : eval chip.2.1 x ≤ ↑(d.length ⟨chip.1, hslot⟩)) : evaluatedChipVertex d fallback x chip.1 chip.2.1 = d.pathVertex ⟨chip.1, hslot⟩ ⟨(eval chip.2.1 x).toNat, ⋯⟩

The decoded vertex of an in-range chip is the literal path vertex of its evaluated coordinate.

Placement at an interior vertex

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.rawChipDivisor_interiorVertex_eq_rawChipMassAt {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 fallback : Fin n) (e : Fin p) (o : Fin (d.length e - 1)) : rawChipDivisor d w (evaluatedChipVertex d fallback x) (d.interiorVertex e o) = w.rawChipMassAt x (↑e) (↑↑o + 1)

The interior chip coefficient. On a closed face the decoded raw chip divisor at an interior vertex is exactly the physical chip mass of that slot at that coordinate.

Placement at a core class

def Utilities.Subdivision.ClosedRowProof.RichWitness.headMassAdj {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (x : List ℤ) (e : Fin p) : ℤ

The head-side physical chip mass, suppressed on a collapsed slot.

On a slot of length 0 the two displayed endpoints are the same vertex, so a tail term and a head term would double count. By RichChipBridge.rawChipMassAt_eq_zero_of_coord_eq_zero an accepted rich leaf has no chip on such a slot at all, so the suppressed value is 0; the if is what makes that visible without a hypothesis.

Equations

• Utilities.Subdivision.ClosedRowProof.RichWitness.headMassAdj d w x e = if d.length e = 0 then 0 else w.rawChipMassAt x ↑e ↑(d.length e)

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.rawChipDivisor_coreVertex_eq {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 fallback r : Fin n) : rawChipDivisor d w (evaluatedChipVertex d fallback x) (d.coreVertex r) = ∑ e : Fin p, ((if d.rep (d.core.tail e) = d.rep r then w.rawChipMassAt x (↑e) 0 else 0) + if d.rep (d.core.head e) = d.rep r then headMassAdj d w x e else 0)

The core-class chip coefficient. On a closed face the decoded raw chip divisor at a contracted core class is the sum, over slots, of the two endpoint masses of the slots whose endpoints lie in the class.