Theta Prefix #
theorem
Bananas.raw_strand_prefix_linearEquiv
{g : ℕ}
(B : Banana g)
(α : Fin (g + 1))
(n : ℕ)
(hn : n ≤ B.length α)
:
linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)
(↑n • (oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α ⟨1, ⋯⟩) - oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α 0)))
(oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α ⟨n, ⋯⟩) - oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α 0))
Paper source: the prefix firing calculation used in eq:multDiffMarkedPts.
This adapter is currently proved for slots stored in the left-to-right
orientation. The reversed-orientation adapter is a separate endpoint
reflection calculation, not a definitional simplification.
theorem
Bananas.strand_prefix_linearEquiv_of_tail_zero
{g : ℕ}
(B : Banana g)
(α : Fin (g + 1))
(p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α)
(hTail : B.core.tail α = 0)
:
linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)
(↑↑p • (oneChip (strandVertex B α ⟨1, ⋯⟩) - oneChip (leftEndpoint B)))
(oneChip (strandVertex B α p) - oneChip (leftEndpoint B))
theorem
Bananas.strand_prefix_linearEquiv_of_tail_nonzero
{g : ℕ}
(B : Banana g)
(α : Fin (g + 1))
(p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α)
(hTail : B.core.tail α ≠ 0)
:
linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)
(↑↑p • (oneChip (strandVertex B α ⟨1, ⋯⟩) - oneChip (leftEndpoint B)))
(oneChip (strandVertex B α p) - oneChip (leftEndpoint B))
Full normalized form of the one-strand prefix identity used by
eq:multDiffMarkedPts; the two cases account for the subdivision model's
arbitrary storage orientation.
theorem
Bananas.strand_prefix_linearEquiv
{g : ℕ}
(B : Banana g)
(α : Fin (g + 1))
(p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α)
:
linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)
(↑↑p • (oneChip (strandVertex B α ⟨1, ⋯⟩) - oneChip (leftEndpoint B)))
(oneChip (strandVertex B α p) - oneChip (leftEndpoint B))