Sub-interval reflection scripts

The same-strand argument needs segment-reflection primitives (segScript and its Laplacian) on an arbitrary sub-interval [lo, hi] of a single slot. They are stated in the Bananas namespace because this is their natural geometric setting.

This is the SegmentReflection plateau transplanted onto an arbitrary sub-interval [lo, hi] of one slot and extended by zero. Its Laplacian consumes the chips at path positions lo and hi and produces chips at target and its mirror lo + hi - target.

def Bananas.segValue {p : ℕ} (star : Fin p) (lo hi target : ℕ) : Fin p → ℕ → ℤ

Path values of the sub-interval reflection.

Equations

• Bananas.segValue star lo hi target edge k = if edge = star then if k ≤ hi then Utilities.SegmentReflection.value (hi - lo) (target - lo) (k - lo) else 0 else 0

def Bananas.segScript {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (star : Fin p) (lo hi target : ℕ) : firingScript spec.graph

The sub-interval reflection script.

Equations

• Bananas.segScript spec star lo hi target = spec.slotValueScript (fun (x : Fin n) => 0) (Bananas.segValue star lo hi target)

def Bananas.segSlope {p : ℕ} (star : Fin p) (lo hi target : ℕ) : Fin p → ℕ → ℤ

Unit-step slopes of the sub-interval reflection.

Equations

• Bananas.segSlope star lo hi target edge k = if edge = star then if lo ≤ k ∧ k < hi then Utilities.SegmentReflection.slope (hi - lo) (target - lo) (k - lo) else 0 else 0

theorem Bananas.segValue_star {p : ℕ} (star : Fin p) (lo hi target k : ℕ) : segValue star lo hi target star k = if k ≤ hi then Utilities.SegmentReflection.value (hi - lo) (target - lo) (k - lo) else 0

theorem Bananas.segValue_other {p : ℕ} {star edge : Fin p} (he : edge ≠ star) (lo hi target k : ℕ) : segValue star lo hi target edge k = 0

theorem Bananas.segSlope_star {p : ℕ} (star : Fin p) (lo hi target k : ℕ) : segSlope star lo hi target star k = if lo ≤ k ∧ k < hi then Utilities.SegmentReflection.slope (hi - lo) (target - lo) (k - lo) else 0

theorem Bananas.segSlope_other {p : ℕ} {star edge : Fin p} (he : edge ≠ star) (lo hi target k : ℕ) : segSlope star lo hi target edge k = 0

theorem Bananas.segCompatible {n p : ℕ} {spec : Utilities.Certificate.SubdivisionGraph.Spec n p} {star : Fin p} {lo hi target : ℕ} (hlo : lo < target) (hhi : target < hi) (hlen : hi ≤ spec.length star) : spec.SlotValueCompatible (fun (x : Fin n) => 0) (segValue star lo hi target)

theorem Bananas.isStepSlope_seg {n p : ℕ} {spec : Utilities.Certificate.SubdivisionGraph.Spec n p} {star : Fin p} {lo hi target : ℕ} (hlo : lo < target) (hhi : target < hi) (hlen : hi ≤ spec.length star) : spec.IsStepSlope (segScript spec star lo hi target) (segSlope star lo hi target)

theorem Bananas.segSlope_zero {p : ℕ} {star : Fin p} {lo hi target : ℕ} (hlo : lo < target) (hhi : target < hi) : segSlope star lo hi target star 0 = if lo = 0 then -1 else 0

theorem Bananas.segSlope_last {n p : ℕ} {spec : Utilities.Certificate.SubdivisionGraph.Spec n p} {star : Fin p} {lo hi target : ℕ} (hlo : lo < target) (hhi : target < hi) (hlen : hi ≤ spec.length star) : segSlope star lo hi target star (spec.length star - 1) = if hi = spec.length star then 1 else 0

theorem Bananas.segSlope_diff {p : ℕ} {star : Fin p} {lo hi target : ℕ} (hlo : lo < target) (hhi : target < hi) (k : ℕ) (hk : 0 < k) : segSlope star lo hi target star k - segSlope star lo hi target star (k - 1) = (((-if k = lo then 1 else 0) - if k = hi then 1 else 0) + if k = target then 1 else 0) + if k = lo + hi - target then 1 else 0

theorem Bananas.prin_seg_core {n p : ℕ} {spec : Utilities.Certificate.SubdivisionGraph.Spec n p} {star : Fin p} {lo hi target : ℕ} (hlo : lo < target) (hhi : target < hi) (hlen : hi ≤ spec.length star) (v : Fin n) : (prin spec.graph) (segScript spec star lo hi target) (spec.coreVertex v) = (if spec.core.tail star = v then if lo = 0 then -1 else 0 else 0) + if spec.core.head star = v then -if hi = spec.length star then 1 else 0 else 0

theorem Bananas.prin_seg_int {n p : ℕ} {spec : Utilities.Certificate.SubdivisionGraph.Spec n p} {star : Fin p} {lo hi target : ℕ} (hlo : lo < target) (hhi : target < hi) (hlen : hi ≤ spec.length star) (edge : Fin p) (offset : Fin (spec.length edge - 1)) : (prin spec.graph) (segScript spec star lo hi target) (spec.interiorVertex edge offset) = if edge = star then (((-if ↑offset + 1 = lo then 1 else 0) - if ↑offset + 1 = hi then 1 else 0) + if ↑offset + 1 = target then 1 else 0) + if ↑offset + 1 = lo + hi - target then 1 else 0 else 0

Generic vertex and chip lemmas

Elementary facts about subdivision vertices and oneChip evaluations, transplanted verbatim from the Generic/Chips sections of Utilities/GenusFourCore100.lean and Utilities/GenusFourCore097.lean so that the banana development does not depend on those genus-four case files.

theorem Bananas.interiorVertex_eq_iff {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (e e' : Fin p) (off : Fin (spec.length e - 1)) (off' : Fin (spec.length e' - 1)) : spec.interiorVertex e off = spec.interiorVertex e' off' ↔ e = e' ∧ ↑off = ↑off'

Distinct interior vertices are distinguished by their slot and offset.

theorem Bananas.coreVertex_ne_interiorVertex {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (v : Fin n) (e : Fin p) (off : Fin (spec.length e - 1)) : spec.coreVertex v ≠ spec.interiorVertex e off

theorem Bananas.divisor_ext {n p : ℕ} {spec : Utilities.Certificate.SubdivisionGraph.Spec n p} {D E : CFDiv spec.graph} (hcore : ∀ (v : Fin n), D (spec.coreVertex v) = E (spec.coreVertex v)) (hint : ∀ (edge : Fin p) (offset : Fin (spec.length edge - 1)), D (spec.interiorVertex edge offset) = E (spec.interiorVertex edge offset)) : D = E

Two divisors on a subdivision agree once they agree at the core vertices and at every interior vertex.

theorem Bananas.pathVertex_interior {n p : ℕ} {spec : Utilities.Certificate.SubdivisionGraph.Spec n p} (edge : Fin p) (k : ℕ) (hk0 : 0 < k) (hk : k < spec.length edge) : spec.pathVertex edge ⟨k, ⋯⟩ = spec.interiorVertex edge ⟨k - 1, ⋯⟩

A strictly interior path position is an interior vertex.

theorem Bananas.one_chip_pV_core {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (e : Fin p) (k : ℕ) (hk : k ≤ spec.length e) (v : Fin n) : oneChip (spec.pathVertex e ⟨k, ⋯⟩) (spec.coreVertex v) = (if k = 0 then if spec.core.tail e = v then 1 else 0 else 0) + if k = spec.length e then if spec.core.head e = v then 1 else 0 else 0

theorem Bananas.one_chip_pV_int {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (e : Fin p) (k : ℕ) (hk : k ≤ spec.length e) (e' : Fin p) (off : Fin (spec.length e' - 1)) : oneChip (spec.pathVertex e ⟨k, ⋯⟩) (spec.interiorVertex e' off) = if e = e' then if k = ↑off + 1 then 1 else 0 else 0

theorem Bananas.one_chip_pos_core {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (e : Fin p) (pos : spec.PathPosition e) (v : Fin n) : oneChip (spec.pathVertex e pos) (spec.coreVertex v) = (if ↑pos = 0 then if spec.core.tail e = v then 1 else 0 else 0) + if ↑pos = spec.length e then if spec.core.head e = v then 1 else 0 else 0

theorem Bananas.one_chip_pos_int {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (e : Fin p) (pos : spec.PathPosition e) (e' : Fin p) (off : Fin (spec.length e' - 1)) : oneChip (spec.pathVertex e pos) (spec.interiorVertex e' off) = if e = e' then if ↑pos = ↑off + 1 then 1 else 0 else 0