The endpoint layer for a marked script

ConfigurationCommon reads the Laplacian at a contracted core class as a sum, over the slots of the uncontracted core, of one endpointPair. This file is the same reading for DegSpec.splitScript, the script that may bend downward at one marked offset per slot (SplitRampScript.lean).

Two facts make the marked layer cheap.

• An unmarked slot is not new. Setting mark e = 0 and markValue e = potential (rep (tail e)) makes the marked endpoint pair equal to ConfigurationCommon.endpointPair (endpointPair_of_unmarked). A row therefore marks only the one or two slots carrying an interior chip and keeps the existing single-ramp ledger -- and the existing configuration files' arithmetic -- everywhere else.
• A marked slot splits into two ordinary arms. Its tail endpoint sees the canonical ramp of rise markRiseIn over mark e steps, and its head endpoint the canonical ramp of rise markRiseOut over length e - mark e steps (endpointPair_marked_tail, endpointPair_marked_head). So the one-edge ledger of ConfigurationFive -- stated on bare naturals, independent of any core -- applies to each half unchanged.

Both AR rows that need this (05, the sixth family, and 08, the seventh) place their interior chips so that one of the two rises is always zero, which is also the hypothesis under which the chip pays for the kink; see Utilities/Subdivision/SplitRampArithmetic.lean.

def AtanasovRanganathan.ConfigurationMarkedCommon.endpointPair (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (potential : Fin 8 → ℤ) (mark : Fin 12 → ℕ) (markValue : Fin 12 → ℤ) (e : Fin 12) (r : Fin 8) : ℤ

The two endpoint terms one original core slot contributes to one contracted core class, for a marked script. As in ConfigurationCommon.endpointPair, keeping them paired is what makes a collapsed slot cancel.

Equations

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

theorem AtanasovRanganathan.ConfigurationMarkedCommon.prin_eq_sum_endpointPair (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) (r : Fin 8) : (prin d.graph) (d.splitScript potential mark markValue) (d.coreVertex r) = ∑ e : Fin 12, endpointPair d potential mark markValue e r

The core-class Laplacian of a marked script is the sum of its endpoint pairs. This is prin_splitScript_coreVertex_eq_endpointSum with the summand named.

Unmarked slots

theorem AtanasovRanganathan.ConfigurationMarkedCommon.markRiseOut_eq_coreRise (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} (hInv : d.RepInvariant potential) {markValue : Fin 12 → ℤ} {e : Fin 12} (hValue : markValue e = potential (d.rep (d.core.tail e))) : d.markRiseOut potential markValue e = d.coreRise potential e

On an unmarked slot the outgoing rise is the ordinary core rise.

theorem AtanasovRanganathan.ConfigurationMarkedCommon.endpointPair_of_unmarked (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} (hInv : d.RepInvariant potential) {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} {e : Fin 12} (hMark : mark e = 0) (hValue : markValue e = potential (d.rep (d.core.tail e))) (r : Fin 8) : endpointPair d potential mark markValue e r = ConfigurationCommon.endpointPair d potential e r

An unmarked slot is not new. Its marked endpoint pair is literally the single-ramp one.

Marked slots

A marked slot is read as two ordinary arms. The hypotheses below are the ones a configuration supplies anyway: the mark lies strictly inside its slot exactly when neither half has collapsed.

theorem AtanasovRanganathan.ConfigurationMarkedCommon.splitStep_tail_of_pos (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) {e : Fin 12} (hPos : 0 < mark e) : Utilities.Certificate.SubdivisionArithmetic.splitStep (d.length e) (mark e) (d.markRiseIn potential markValue e) (d.markRiseOut potential markValue e) 0 = Utilities.Certificate.SubdivisionArithmetic.step (mark e) (d.markRiseIn potential markValue e) 0

At the tail of a marked slot the script is the canonical ramp of rise markRiseIn over mark e steps.

theorem AtanasovRanganathan.ConfigurationMarkedCommon.splitStep_head_of_lt (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) {e : Fin 12} (hPos : 0 < d.length e) (hLt : mark e < d.length e) : Utilities.Certificate.SubdivisionArithmetic.splitStep (d.length e) (mark e) (d.markRiseIn potential markValue e) (d.markRiseOut potential markValue e) (d.length e - 1) = Utilities.Certificate.SubdivisionArithmetic.step (d.length e - mark e) (d.markRiseOut potential markValue e) (d.length e - 1 - mark e)

At the head of a marked slot the script is the canonical ramp of rise markRiseOut over length e - mark e steps.

theorem AtanasovRanganathan.ConfigurationMarkedCommon.splitStep_tail_eq_zero_of_flat (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) {e : Fin 12} (hFlat : d.markRiseIn potential markValue e = 0) : Utilities.Certificate.SubdivisionArithmetic.splitStep (d.length e) (mark e) (d.markRiseIn potential markValue e) (d.markRiseOut potential markValue e) 0 = if 0 < mark e then 0 else Utilities.Certificate.SubdivisionArithmetic.step (d.length e) (d.markRiseOut potential markValue e) 0

A marked slot whose incoming ramp is flat contributes nothing at its tail. This is the shape both AR rows use at the far end of a marked leg.

theorem AtanasovRanganathan.ConfigurationMarkedCommon.splitStep_head_eq_zero_of_flat (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) {e : Fin 12} (hPos : 0 < d.length e) (hLt : mark e < d.length e) (hFlat : d.markRiseOut potential markValue e = 0) : Utilities.Certificate.SubdivisionArithmetic.splitStep (d.length e) (mark e) (d.markRiseIn potential markValue e) (d.markRiseOut potential markValue e) (d.length e - 1) = 0

A marked slot whose outgoing ramp is flat contributes nothing at its head.

Where a marked slot contributes nothing

A marked slot whose chip lies strictly inside it touches only one contracted class: the one carrying the height. The chip's own cost is paid at the marked interior vertex, by prin_splitScript_interiorVertex_ge_neg_one, not at any core class. These three lemmas are what makes a row's class bookkeeping short.

The hypothesis mark e < d.length e (resp. 0 < mark e) is not cosmetic: when the mark reaches an end of its slot the chip is that core vertex, the split ramp degenerates to a single ramp, and the slot behaves like an ordinary arm with its chip at a core class. A row must case-split there; see the module docstring of ConfigurationSeven.

theorem AtanasovRanganathan.ConfigurationMarkedCommon.splitStep_eq_zero_of_flat (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) {e : Fin 12} (hIn : d.markRiseIn potential markValue e = 0) (hOut : d.markRiseOut potential markValue e = 0) {k : ℕ} (hk : k < d.length e) : Utilities.Certificate.SubdivisionArithmetic.splitStep (d.length e) (mark e) (d.markRiseIn potential markValue e) (d.markRiseOut potential markValue e) k = 0

Both ramps flat: the slot moves nothing anywhere.

theorem AtanasovRanganathan.ConfigurationMarkedCommon.endpointPair_eq_zero_of_flat (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) {e : Fin 12} (hIn : d.markRiseIn potential markValue e = 0) (hOut : d.markRiseOut potential markValue e = 0) (r : Fin 8) : endpointPair d potential mark markValue e r = 0

theorem AtanasovRanganathan.ConfigurationMarkedCommon.endpointPair_eq_zero_of_ne_tail (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) {e : Fin 12} (hOut : d.markRiseOut potential markValue e = 0) (hPos : 0 < d.length e) (hLt : mark e < d.length e) {r : Fin 8} (hNe : d.rep (d.core.tail e) ≠ d.rep r) : endpointPair d potential mark markValue e r = 0

A marked slot read from its tail: nothing reaches any class other than the tail's.

theorem AtanasovRanganathan.ConfigurationMarkedCommon.endpointPair_eq_zero_of_ne_head (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) {e : Fin 12} (hIn : d.markRiseIn potential markValue e = 0) (hPos : 0 < mark e) {r : Fin 8} (hNe : d.rep (d.core.head e) = d.rep r → False) : endpointPair d potential mark markValue e r = 0

A marked slot read from its head: nothing reaches any class other than the head's.