Reusable Atanasov--Ranganathan configuration moves #
The seven pictures in Atanasov--Ranganathan, Lemma 4.1, are local Dhar
calculations. This file records the common proof interface independently of
those pictures: a configuration supplies an integral firing script whose
removed-chip residual is effective, hence a StrongSeparator.Reaches fact.
Two geometric patterns are isolated here.
- A segment configuration starts with one chip at each endpoint and uses an
exact two-endpoint reflection to reach a named point of the segment. The
min(a,b)anda-bpositions occurring in configurations six and seven are exposed throughMovingPosition. - The doubled-path configuration is fully discharged using the interpolated
truncated-ramp potential already proved in
GenusFourLoopLemma.
The paper's diagrams do not specify an ordered core-slot encoding, edge orientations, or which dashed half-edge continues outside each solid configuration. Consequently this module does not assert that a numbered picture, or Core 095, has been encoded. It gives the reusable checked moves to which such incidence data must eventually be connected.
A uniform interface for one Dhar calculation #
One local Dhar calculation: after removing the target chip, the displayed integral firing script leaves an effective residual.
- script : firingScript G
The integral firing script whose principal divisor makes the residual effective after subtracting a chip at the target.
Instances For
A checked local Dhar move proves the corresponding reachability fact.
Conversely, an explicit effective representative and its firing script can be packaged as a local move without mentioning linear equivalence again.
Equations
- AtanasovRanganathan.Configurations.DharMove.ofScript script hEffective = { script := script, residual_effective := hEffective }
Instances For
A reachability proof already contains a firing script: unfold its effective
representative and extract the principal divisor witnessing linear
equivalence. This converse is noncomputable only because Reaches is stated
existentially; the resulting DharMove is checked by the same residual
effectivity field as a hand-authored move.
Equations
- AtanasovRanganathan.Configurations.DharMove.ofReaches hReach = { script := Classical.choose ⋯, residual_effective := ⋯ }
Instances For
Rank at least one supplies a checked Dhar move at every target. This is
the useful converse to DharMove.reaches when a row is proved by a global
rank argument (for example a strong-separator or transmission theorem) rather
than by retaining its local scripts as primary data.
Equations
Instances For
Configuration version of the off-support lemma: it is enough to attach a local Dhar move to every vertex outside the support of an effective divisor.
Degree bookkeeping for a configuration proof of any rank-one pencil.
Degree-three specialization retained for the genus-four configurations.
Three-chip divisors with a named moving chip #
The degree-three divisor used throughout the genus-four pictures. The three vertices need not be distinct.
Equations
Instances For
Every displayed chip position is automatically reached; Dhar moves are needed only away from these three positions.
A three-chip divisor whose first chip is at the min(a,b) position used
in the sixth and seventh configurations of the paper.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A three-chip divisor whose first chip is at a truncated difference of edge lengths, as in the three macroscopic cases of the first genus-four family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Configuration 1: two endpoint chips on a segment #
An exact reflection starting with one chip at each of two endpoints. The second output chip is allowed to coincide with the requested target.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The first pictured configuration, abstracted to its exact principal identity: endpoint chips plus a segment reflection reach the requested point.
Exact geometric obligation for a subdivided segment: its two endpoint chips reflect to a named path position and one further effective chip.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Once the segment potential identity is known, the endpoint-chip configuration reaches the named subdivision position.
min(a,b) specialization of the segment configuration.
Difference-position specialization used by the first genus-four family.
Doubled-path configuration: a closed potential proof #
Two chips at the common base of two subdivided paths reach their bivalent
marker. Unlike SegmentConfiguration.ReflectsTo, the geometric potential
identity here is already fully proved by the truncated-ramp interpolation
API.
Rank-one wrapper for a subdivision in which the doubled-path marker is the only core reachability test not discharged elsewhere.