The base layer shared by every Atanasov--Ranganathan configuration

Every AR configuration on a genus-five core interpolates a potential that is a negative constant on one contracted core class and zero elsewhere, and then reads off what each original core slot contributes at each contracted class. Three groups of facts are common to all of them and depend on no row and on no particular configuration:

• the six one-slot ramp lemmas, which say what the first and last slope of a truncated ramp is (firstStep_neg_eq_neg_one, lastStep_pos_eq_one, firstStep_full_eq_one, lastStep_neg_full_eq_neg_one, firstStep_pos_nonneg, lastStep_neg_nonpos);
• the one-class potential centerPotential together with its rep-invariance and its value on a singleton class;
• the endpoint bookkeeping endpointContribution and endpointPair, including the fact that a slot with zero rise contributes nothing.

These used to live in GenusFiveRow11, where they were first written, which forced ConfigurationThree and ConfigurationTwo to import a row. They are collected here so that the configuration files depend on no row at all, and GenusFiveRow11 can itself be a ConfigTwo instantiation.

Core size

Everything here is generic in the core size (n, p): n vertices and p slots. The genus-five programme instantiates it at (8, 12) and the genus-six critical pencil at (10, 15); because n and p are implicit and inferred from the DegSpec, no genus-five call site had to change when this file stopped being genus-five specific.

The one-slot ramp lemmas

theorem AtanasovRanganathan.ConfigurationCommon.firstStep_neg_eq_neg_one {L k : ℕ} (hk : 0 < k) (hkL : k ≤ L) : Utilities.Certificate.SubdivisionArithmetic.step L (-↑k) 0 = -1

The first slope of a truncated negative ramp consumes one chip.

theorem AtanasovRanganathan.ConfigurationCommon.lastStep_pos_eq_one {L k : ℕ} (hk : 0 < k) (hkL : k ≤ L) : Utilities.Certificate.SubdivisionArithmetic.step L (↑k) (L - 1) = 1

The last slope of a positive ramp consumes one chip at its head.

theorem AtanasovRanganathan.ConfigurationCommon.firstStep_full_eq_one {L : ℕ} (hL : 0 < L) : Utilities.Certificate.SubdivisionArithmetic.step L (↑L) 0 = 1

A ramp whose height equals the whole arm delivers one chip at its tail.

theorem AtanasovRanganathan.ConfigurationCommon.lastStep_neg_full_eq_neg_one {L : ℕ} (hL : 0 < L) : Utilities.Certificate.SubdivisionArithmetic.step L (-↑L) (L - 1) = -1

A reversed full-arm ramp delivers one chip at its head.

theorem AtanasovRanganathan.ConfigurationCommon.firstStep_pos_nonneg {L k : ℕ} (hL : 0 < L) : 0 ≤ Utilities.Certificate.SubdivisionArithmetic.step L (↑k) 0

theorem AtanasovRanganathan.ConfigurationCommon.lastStep_neg_nonpos {L k : ℕ} (hk : 0 < k) (hkL : k ≤ L) : Utilities.Certificate.SubdivisionArithmetic.step L (-↑k) (L - 1) ≤ 0

The one-class potential

def AtanasovRanganathan.ConfigurationCommon.centerPotential {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (height : ℕ) (v : Fin n) : ℤ

Negative height on one contracted class and zero on all other classes.

Equations

• AtanasovRanganathan.ConfigurationCommon.centerPotential d center height v = if d.rep v = d.rep center then -↑height else 0

theorem AtanasovRanganathan.ConfigurationCommon.centerPotential_repInvariant {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (height : ℕ) : d.RepInvariant (centerPotential d center height)

theorem AtanasovRanganathan.ConfigurationCommon.centerPotential_eq_of_singleton {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (height : ℕ) (hSingleton : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) (v : Fin n) : centerPotential d center height v = if v = center then -↑height else 0

Endpoint bookkeeping

def AtanasovRanganathan.ConfigurationCommon.endpointContribution {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (potential : Fin n → ℤ) (v : Fin n) : ℤ

The per-source-core endpoint contribution used by the class-sum formula.

Equations

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

def AtanasovRanganathan.ConfigurationCommon.endpointPair {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (potential : Fin n → ℤ) (e : Fin p) (r : Fin n) : ℤ

The two endpoint terms contributed by one original core slot to one contracted core class. Keeping them paired is essential on a closed face: when a zero slot is contracted, its two artificial endpoint terms cancel.

Equations

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

theorem AtanasovRanganathan.ConfigurationCommon.zero_rise_endpoint_pair {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (e : Fin p) (r : Fin n) : ((if d.rep (d.core.tail e) = d.rep r then Utilities.Certificate.SubdivisionArithmetic.step (d.length e) 0 0 else 0) + if d.rep (d.core.head e) = d.rep r then -Utilities.Certificate.SubdivisionArithmetic.step (d.length e) 0 (d.length e - 1) else 0) = 0

theorem AtanasovRanganathan.ConfigurationCommon.endpointPair_eq_zero_of_rise_eq_zero {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (potential : Fin n → ℤ) (e : Fin p) (r : Fin n) (hRise : d.coreRise potential e = 0) : endpointPair d potential e r = 0

Redistributing chips inside contracted classes

A chip may be delivered to a vertex of the target's class other than the target itself, and a collapsed arm may put its chip in the centre's class. Both are handled by moving weight within a class, which leaves every class sum -- hence the divisor -- unchanged.

def AtanasovRanganathan.ConfigurationCommon.indicatorWeight {n : ℕ} (vertex source : Fin n) : ℤ

The integer indicator assigning one chip at the source vertex and zero elsewhere.

Equations

• AtanasovRanganathan.ConfigurationCommon.indicatorWeight vertex source = if vertex = source then 1 else 0

def AtanasovRanganathan.ConfigurationCommon.transferWeight {n : ℕ} (source target vertex : Fin n) : ℤ

The degree-zero weight that removes one chip at the source and adds one at the target.

Equations

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

theorem AtanasovRanganathan.ConfigurationCommon.sum_transferWeight_eq_zero {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) {source target : Fin n} (hRep : d.rep source = d.rep target) (r : Fin n) : ∑ v : Fin n with d.rep v = d.rep r, transferWeight source target v = 0

theorem AtanasovRanganathan.ConfigurationCommon.sum_indicatorWeight_class {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (source r : Fin n) : ∑ v : Fin n with d.rep v = d.rep r, indicatorWeight v source = if d.rep source = d.rep r then 1 else 0

Endpoint accounting on the contracted face

def AtanasovRanganathan.ConfigurationCommon.positiveEndpointContribution {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (potential : Fin n → ℤ) (v : Fin n) : ℤ

Endpoint contribution with the artificial endpoints of a zero slot suppressed. Those two terms cancel after passing to a contracted class.

Equations

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

theorem AtanasovRanganathan.ConfigurationCommon.positiveEndpointContribution_classSum_eq {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (potential : Fin n → ℤ) (hInv : d.RepInvariant potential) (r : Fin n) : ∑ v : Fin n with d.rep v = d.rep r, positiveEndpointContribution d potential v = (prin d.graph) (d.interpolatedScript potential) (d.coreVertex r)