Atanasov--Ranganathan configuration 2, generic in the core #
Configuration 2 of Atanasov--Ranganathan, Proposition 5.1, is the local picture at a chip-free core vertex all three of whose slots end on a chip vertex -- a tripod centre. Interpolate the same negative height along the three arms, choosing that height to be the shortest arm length. Every arm consumes at most its endpoint chip, and a shortest arm delivers a chip to the centre.
This file states that picture once, as a ConfigTwo bundle of the lookup data
together with the incidence facts a row must check, and proves the centre's
residual-effectivity and reach lemmas from those facts alone. A row supplies
the tables and discharges the Prop fields; nothing else.
Unlike ConfigThree, the centres are named by an explicit predicate
isCenter rather than "every chip-free vertex". Rows 11 and 12 combine
several local pictures, so a row may declare only some of its chip-free
vertices to be tripod centres and cover the rest by other means; the
conclusions here are stated one centre at a time so that several instances
compose. A row all of whose chip-free vertices are tripod centres gets the
whole closed-orthant construction from closedConstruction.
The generic slot arithmetic (Ends, sum_three, slotTerm, slotValue,
armContribution, endpointPair_arm) is shared with configuration 3 and
currently lives in ConfigurationThree.lean; that is why this file imports
it. Neither structure mentions the other.
The indicator of "the chip at v sits in the contracted class of r".
Instances For
The lookup data of one AR configuration-2 family, together with exactly the incidence facts the calculation uses.
The four chips carry the divisor. Each declared centre v is chip free, its
three slots firstArm v, secondArm v, thirdArm v end on the chips
firstChip v, secondChip v, thirdChip v, and spareChip v names the
fourth chip, which the centre does not touch.
- core : GenusFiveCoreAtlas.Core
The eight-vertex core graph carrying configuration two.
- chipOne : Fin 8
The first of the four designated chip vertices of configuration two.
- chipTwo : Fin 8
The second of the four designated chip vertices of configuration two.
- chipThree : Fin 8
The third of the four designated chip vertices of configuration two.
- chipFour : Fin 8
The fourth of the four designated chip vertices of configuration two.
The Boolean selector of the center vertices, none of which is a designated chip vertex.
The slot joining a center to the first chip assigned to that center.
The slot joining a center to the second chip assigned to that center.
The slot joining a center to the third chip assigned to that center.
The designated chip vertex at the far end of the center's first arm.
The designated chip vertex at the far end of the center's second arm.
The designated chip vertex at the far end of the center's third arm.
The fourth chip vertex, complementary to the three assigned arm endpoints.
- secondChip_isChip (v : Fin 8) : self.isCenter v = true → ConfigurationThree.IsChipOf self.chipOne self.chipTwo self.chipThree self.chipFour (self.secondChip v)
- secondArm_ends (v : Fin 8) : self.isCenter v = true → ConfigurationThree.Ends self.core (self.secondArm v) v (self.secondChip v)
Instances For
The displayed divisor #
One chip on each of the four displayed vertices.
Equations
- cfg.divisor d = AtanasovRanganathan.Configurations.fourChipDivisor (d.coreVertex cfg.chipOne) (d.coreVertex cfg.chipTwo) (d.coreVertex cfg.chipThree) (d.coreVertex cfg.chipFour)
Instances For
A slot from a chip-free class to a chip cannot have collapsed.
Incidence facts transported to a degenerate spec #
The interpolation height #
The shortest of the three arms at a centre.
Equations
Instances For
Which core classes a tripod centre can meet #
Every neighbour of a tripod centre is a chip vertex.
A zero-edge class containing a chip-free tripod centre is a singleton.
A zero-divisor class at a tripod centre is that centre alone.
The interpolated potential #
The closed-face core potential for configuration 2: the tripod height on the centre's class and zero elsewhere.
Equations
- cfg.centerPotential d center = AtanasovRanganathan.ConfigurationCommon.centerPotential d center (cfg.tripodHeight d center)
Instances For
The chip delivered to the centre #
The Laplacian away from the fired class #
Residual effectivity and reach #
Configuration 2 at one centre. Firing the tripod script leaves an effective divisor after removing one chip from the centre's class.
Configuration 2 reaches its centre. This is the statement a row consumes, one centre at a time, so that several local pictures compose.
Configuration 2 on a closed face. A row every one of whose chip-free vertices is a tripod centre gets the whole closed-orthant AR construction.