Chip evaluations for the theta ramp #
The endpoint and first-interior evaluations support the firing identity
eq:multDiffMarkedPts and the evenly-marked conclusion cor:evenlyMarkedKGT
in the paper source.
The theta ramp uses the path positions 0, 1, and length. Position 1
needs a length split: on a strand of length one it is the head core vertex,
whereas on a longer strand it is the first interior vertex.
theorem
Bananas.one_chip_pathVertex_zero_apply_interior
{g : ℕ}
(B : Banana g)
(α edge : Fin (g + 1))
(offset : Fin (B.length edge - 1))
:
oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α ⟨0, ⋯⟩)
(Utilities.Certificate.SubdivisionGraph.Spec.interiorVertex B edge offset) = 0
theorem
Bananas.one_chip_pathVertex_length_apply_interior
{g : ℕ}
(B : Banana g)
(α edge : Fin (g + 1))
(offset : Fin (B.length edge - 1))
:
oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α ⟨B.length α, ⋯⟩)
(Utilities.Certificate.SubdivisionGraph.Spec.interiorVertex B edge offset) = 0
@[simp]
theorem
Bananas.one_chip_pathVertex_one_apply_interior_of_length_eq_one
{g : ℕ}
(B : Banana g)
(α : Fin (g + 1))
(hLength : B.length α = 1)
(edge : Fin (g + 1))
(offset : Fin (B.length edge - 1))
:
oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α ⟨1, ⋯⟩)
(Utilities.Certificate.SubdivisionGraph.Spec.interiorVertex B edge offset) = 0