Reflection on one subdivision segment

The firing potential on a path starts at zero, has slope -1 until the first of a position and its mirror image, is constant between them, and has slope +1 after the second. It therefore returns to zero at the other endpoint, so extending it by zero away from the chosen subdivision slot creates no unwanted firing across the rest of the core.

def Utilities.SegmentReflection.symmetricPosition {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge : Fin p) (position : spec.PathPosition edge) : spec.PathPosition edge

The path position symmetric to position under reversal of the slot.

Equations

• Utilities.SegmentReflection.symmetricPosition spec edge position = ⟨spec.length edge - ↑position, ⋯⟩

@[simp]

theorem Utilities.SegmentReflection.symmetricPosition_val {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge : Fin p) (position : spec.PathPosition edge) : ↑(symmetricPosition spec edge position) = spec.length edge - ↑position

def Utilities.SegmentReflection.value (length position i : ℕ) : ℤ

The integral plateau potential at numerical path offset i.

Equations

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

def Utilities.SegmentReflection.slope (length position i : ℕ) : ℤ

The oriented slope after numerical path position i.

Equations

• Utilities.SegmentReflection.slope length position i = if i < min position (length - position) then -1 else if max position (length - position) ≤ i then 1 else 0

theorem Utilities.SegmentReflection.min_add_max_reflection {length position : ℕ} (hPosition : position ≤ length) : min position (length - position) + max position (length - position) = length

@[simp]

theorem Utilities.SegmentReflection.value_zero (length position : ℕ) : value length position 0 = 0

theorem Utilities.SegmentReflection.value_length {length position : ℕ} (hPosition : position ≤ length) : value length position length = 0

theorem Utilities.SegmentReflection.value_succ_sub_value {length position i : ℕ} (hPosition : position ≤ length) : value length position (i + 1) - value length position i = slope length position i

Consecutive values realize the advertised three-piece slope.

theorem Utilities.SegmentReflection.slope_divergence {length position j : ℕ} (hLength : 0 < length) (hPosition : position ≤ length) (hj : j ≤ length) : ((if j < length then slope length position j else 0) - if 0 < j then slope length position (j - 1) else 0) = (((-if j = 0 then 1 else 0) - if j = length then 1 else 0) + if j = position then 1 else 0) + if j = length - position then 1 else 0

The divergence of the slope is -1 at either endpoint and +1 at the chosen position and its mirror. Coincident terms add, including the midpoint and endpoint cases.

The slot-supported firing script

def Utilities.SegmentReflection.script {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge : Fin p) (position : spec.PathPosition edge) : firingScript spec.graph

Extend the plateau potential by zero over every core vertex and every other subdivision slot.

Equations

• Utilities.SegmentReflection.script spec edge position (Sum.inl _vertex) = 0
• Utilities.SegmentReflection.script spec edge position (Sum.inr interior) = if interior.fst = edge then Utilities.SegmentReflection.value (spec.length edge) (↑position) (↑interior.snd + 1) else 0

@[simp]

theorem Utilities.SegmentReflection.script_core {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge : Fin p) (position : spec.PathPosition edge) (vertex : Fin n) : script spec edge position (spec.coreVertex vertex) = 0

@[simp]

theorem Utilities.SegmentReflection.script_interior_same {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge : Fin p) (position : spec.PathPosition edge) (offset : Fin (spec.length edge - 1)) : script spec edge position (spec.interiorVertex edge offset) = value (spec.length edge) (↑position) (↑offset + 1)

@[simp]

theorem Utilities.SegmentReflection.script_interior_other {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge other : Fin p) (position : spec.PathPosition edge) (hOther : other ≠ edge) (offset : Fin (spec.length other - 1)) : script spec edge position (spec.interiorVertex other offset) = 0

theorem Utilities.SegmentReflection.script_stepLeft {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge other : Fin p) (position : spec.PathPosition edge) (offset : Fin (spec.length other)) : script spec edge position (spec.stepLeft other offset) = if other = edge then value (spec.length edge) ↑position ↑offset else 0

Script value at the left endpoint of any emitted unit step.

theorem Utilities.SegmentReflection.script_stepRight {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge other : Fin p) (position : spec.PathPosition edge) (offset : Fin (spec.length other)) : script spec edge position (spec.stepRight other offset) = if other = edge then value (spec.length edge) (↑position) (↑offset + 1) else 0

Script value at the right endpoint of any emitted unit step.

theorem Utilities.SegmentReflection.script_stepDifference {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge other : Fin p) (position : spec.PathPosition edge) (offset : Fin (spec.length other)) : script spec edge position (spec.stepRight other offset) - script spec edge position (spec.stepLeft other offset) = if other = edge then slope (spec.length edge) ↑position ↑offset else 0

The script difference along a unit step is the reflection slope on the chosen slot and zero on every other slot.

theorem Utilities.SegmentReflection.prin_script_eq_slot_sum {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge : Fin p) (position : spec.PathPosition edge) (vertex : spec.Vertex) : (prin spec.graph) (script spec edge position) vertex = ∑ offset : Fin (spec.length edge), ((if spec.stepLeft edge offset = vertex then slope (spec.length edge) ↑position ↑offset else 0) + if spec.stepRight edge offset = vertex then -slope (spec.length edge) ↑position ↑offset else 0)

The principal divisor of the slot-supported script is the divergence of its slope along that one slot; every other emitted step contributes zero.

theorem Utilities.SegmentReflection.prin_script_pathVertex {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge : Fin p) (position probe : spec.PathPosition edge) : (prin spec.graph) (script spec edge position) (spec.pathVertex edge probe) = (((-if ↑probe = 0 then 1 else 0) - if ↑probe = spec.length edge then 1 else 0) + if ↑probe = ↑position then 1 else 0) + if ↑probe = spec.length edge - ↑position then 1 else 0

The principal coefficient at a vertex of the chosen path is the discrete divergence of the two adjacent slopes.

theorem Utilities.SegmentReflection.prin_script_pathVertex_eq_reflectionDivisor {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge : Fin p) (position probe : spec.PathPosition edge) : (prin spec.graph) (script spec edge position) (spec.pathVertex edge probe) = (-oneChip (spec.coreVertex (spec.core.tail edge)) - oneChip (spec.coreVertex (spec.core.head edge)) + oneChip (spec.pathVertex edge position) + oneChip (spec.pathVertex edge (symmetricPosition spec edge position))) (spec.pathVertex edge probe)

On the chosen path, the numerical divergence formula is exactly the coefficient of the desired four-chip divisor.

theorem Utilities.SegmentReflection.prin_script_eq_reflectionDivisor {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge : Fin p) (position : spec.PathPosition edge) : (prin spec.graph) (script spec edge position) = -oneChip (spec.coreVertex (spec.core.tail edge)) - oneChip (spec.coreVertex (spec.core.head edge)) + oneChip (spec.pathVertex edge position) + oneChip (spec.pathVertex edge (symmetricPosition spec edge position))

Exact principal-divisor identity for reflection on one arbitrary subdivision slot.

Public reflection and reachability interfaces

theorem Utilities.SegmentReflection.reflectsTo {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (edge : Fin p) (position : spec.PathPosition edge) : AtanasovRanganathan.Configurations.SegmentConfiguration.ReflectsTo spec edge position

Every named position on every subdivision slot satisfies the abstract segment-reflection obligation.

theorem Utilities.SegmentReflection.reaches_pathPosition {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (D : CFDiv spec.graph) (edge : Fin p) (position : spec.PathPosition edge) (hEffective : effective D) (hTail : 1 ≤ D (spec.coreVertex (spec.core.tail edge))) (hHead : 1 ≤ D (spec.coreVertex (spec.core.head edge))) : Certificate.StrongSeparator.Reaches spec.graph D (spec.pathVertex edge position)

Endpoint chips on a slot reach every named path position.

theorem Utilities.SegmentReflection.reaches_minLengthPosition {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (D : CFDiv spec.graph) (edge leftLength rightLength : Fin p) (hBound : min (spec.length leftLength) (spec.length rightLength) ≤ spec.length edge) (hEffective : effective D) (hTail : 1 ≤ D (spec.coreVertex (spec.core.tail edge))) (hHead : 1 ≤ D (spec.coreVertex (spec.core.head edge))) : Certificate.StrongSeparator.Reaches spec.graph D (spec.pathVertex edge (spec.minLengthPosition edge leftLength rightLength hBound))

min(a,b) specialization with the reflection obligation discharged.

theorem Utilities.SegmentReflection.reaches_differencePosition {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (D : CFDiv spec.graph) (edge minuend subtrahend : Fin p) (hBound : spec.length minuend - spec.length subtrahend ≤ spec.length edge) (hEffective : effective D) (hTail : 1 ≤ D (spec.coreVertex (spec.core.tail edge))) (hHead : 1 ≤ D (spec.coreVertex (spec.core.head edge))) : Certificate.StrongSeparator.Reaches spec.graph D (spec.pathVertex edge (spec.differencePosition edge minuend subtrahend hBound))

Truncated-difference specialization with the reflection obligation discharged.