Documentation

LeanPool.BrillNoetherGraphs.LowGenus.GenusFiveConfigurations

Genus-five Atanasov--Ranganathan configuration infrastructure #

The eleven local pictures in Proposition 5.1 are not themselves the final divisors. For a fixed subdivision, a construction chooses an effective degree-four divisor and, at every vertex outside its support, identifies one of the eleven pictures and supplies the corresponding integral Dhar move.

This file packages exactly that checked output. It deliberately does not formalize the informal burning-subgraph notation G_v: the load-bearing data is the firing script and effective residual, which is both unambiguous and what the rank proof actually consumes.

Four-chip bookkeeping #

def AtanasovRanganathan.Configurations.fourChipDivisor {G : CFGraph} (first second third fourth : G.V) :

The degree-four divisor used by the genus-five pictures. Repeated chip positions are allowed, as required by AR's seventh family.

Equations

AtanasovRanganathan.Configurations.fourChipDivisor first second third fourth = oneChip first + oneChip second + oneChip third + oneChip fourth

Instances For

theorem AtanasovRanganathan.Configurations.fourChipDivisor_effective {G : CFGraph} (first second third fourth : G.V) :

effective (fourChipDivisor first second third fourth)

@[simp]

theorem AtanasovRanganathan.Configurations.deg_fourChipDivisor {G : CFGraph} (first second third fourth : G.V) :

CFDiv.degree (fourChipDivisor first second third fourth) = 4

theorem AtanasovRanganathan.Configurations.fourChipDivisor_has_chip_first {G : CFGraph} (first second third fourth : G.V) :

1 ≤ fourChipDivisor first second third fourth first

theorem AtanasovRanganathan.Configurations.fourChipDivisor_has_chip_second {G : CFGraph} (first second third fourth : G.V) :

1 ≤ fourChipDivisor first second third fourth second

theorem AtanasovRanganathan.Configurations.fourChipDivisor_has_chip_third {G : CFGraph} (first second third fourth : G.V) :

1 ≤ fourChipDivisor first second third fourth third

theorem AtanasovRanganathan.Configurations.fourChipDivisor_has_chip_fourth {G : CFGraph} (first second third fourth : G.V) :

1 ≤ fourChipDivisor first second third fourth fourth

The eleven local pictures #

inductive AtanasovRanganathan.Configurations.GenusFiveConfigurationKind :

Names for the eleven local configurations in Proposition 5.1, in TikZ reading order. Keeping the tag in construction data makes later audits say which AR picture is being invoked at each off-support vertex.

Instances For

@[instance_reducible]

instance AtanasovRanganathan.Configurations.instDecidableEqGenusFiveConfigurationKind :

DecidableEq GenusFiveConfigurationKind

Equations

AtanasovRanganathan.Configurations.instDecidableEqGenusFiveConfigurationKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AtanasovRanganathan.Configurations.instReprGenusFiveConfigurationKind :

Repr GenusFiveConfigurationKind

Equations

AtanasovRanganathan.Configurations.instReprGenusFiveConfigurationKind = { reprPrec := AtanasovRanganathan.Configurations.instReprGenusFiveConfigurationKind.repr }

def AtanasovRanganathan.Configurations.instReprGenusFiveConfigurationKind.repr :

GenusFiveConfigurationKind → ℕ → Std.Format

Equations

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

Instances For

def AtanasovRanganathan.Configurations.GenusFiveConfigurationKind.isTopRow :

GenusFiveConfigurationKind → Bool

The first six pictures form the top row of AR's figure.

Equations

Instances For

Checked output of one global construction #

structure AtanasovRanganathan.Configurations.DegreeFourDharPencil (G : CFGraph) :

Type u_1

A degree-four pencil proved by AR-style local Dhar calculations.

The configuration tag is documentary; soundness comes from the accompanying DharMove, whose firing script and effective residual are kernel checked.

divisor : CFDiv G
The effective degree-four divisor for which the pencil supplies moves to vertices outside its support.
divisor_effective : effective self.divisor
divisor_degree : CFDiv.degree self.divisor = 4
moveOffSupport (vertex : G.V) : self.divisor vertex = 0 → GenusFiveConfigurationKind × DharMove G self.divisor vertex
For each vertex outside the divisor support, a configuration label and a verified Dhar move reaching that vertex.

Instances For

noncomputable def AtanasovRanganathan.Configurations.DegreeFourDharPencil.ofEffectiveRankOne {G : CFGraph} (D : CFDiv G) (hEffective : effective D) (hDegree : CFDiv.degree D = 4) (hRank : rank G D ≥ 1) :

DegreeFourDharPencil G

Package any effective degree-four rank-one divisor as an AR pencil.

The row constructions are easiest to read when they prove rank semantically (for example by a separator argument). The diagnostic DharMove fields do not add a mathematical hypothesis: rank one says that D - [v] is winnable at every vertex, and the definitions of winnability and principality expose an effective representative and an integral firing script.

Equations

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

Instances For

theorem AtanasovRanganathan.Configurations.DegreeFourDharPencil.nonempty_ofBNExists {G : CFGraph} (existence : Utilities.BNExists G 1 4) :

Nonempty (DegreeFourDharPencil G)

Package an abstract Brill--Noether existence witness as an AR pencil.

BNExists does not require its displayed divisor to be effective. Rank at least one nevertheless makes that divisor winnable, hence linearly equivalent to an effective divisor of the same degree and rank. This adapter is useful for finite cone covers: each cone may use a different explicit certificate, while the row interface still asks for the diagnostic DharMove package.

theorem AtanasovRanganathan.Configurations.DegreeFourDharPencil.rank_ge_one {G : CFGraph} (pencil : DegreeFourDharPencil G) :

rank G pencil.divisor ≥ 1

theorem AtanasovRanganathan.Configurations.DegreeFourDharPencil.bnExists {G : CFGraph} (pencil : DegreeFourDharPencil G) :

Utilities.BNExists G 1 4

def AtanasovRanganathan.Configurations.PositiveSubdivisionDharConstruction {n p : ℕ} (core : Utilities.Certificate.ExplicitPotential.Core n p) (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) :

Uniform checked construction over every positive integral subdivision of a fixed ordered core.

Equations

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

Instances For

theorem AtanasovRanganathan.Configurations.PositiveSubdivisionDharConstruction.toPositiveSubdivisionPencil {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} {core_nonempty : 0 < n} {core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge} (construction : PositiveSubdivisionDharConstruction core core_nonempty core_loopless) :

PositiveSubdivisionPencil core core_nonempty core_loopless 4

Forgetting the diagnostic configuration tags and explicit scripts gives the finite-boundary pencil statement used by the global AR reduction.

Closed-orthant constructions #

def AtanasovRanganathan.Configurations.zeroSlots {p : ℕ} (length : Fin p → ℕ) :

The zero-length slots of a closed length vector.

Equations

AtanasovRanganathan.Configurations.zeroSlots length = {e : Fin p | length e = 0}

Instances For

@[simp]

theorem AtanasovRanganathan.Configurations.mem_zeroSlots {p : ℕ} (length : Fin p → ℕ) (e : Fin p) :

e ∈ zeroSlots length ↔ length e = 0

def AtanasovRanganathan.Configurations.faceSpec {n p : ℕ} (core : Utilities.Certificate.ExplicitPotential.Core n p) (core_nonempty : 0 < n) (length : Fin p → ℕ) (forest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest core (zeroSlots length)) (not_loopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy core (zeroSlots length)) :

Utilities.Certificate.DegenerateSpec.DegSpec n p

The canonical degenerate subdivision of a fixed core at a forest face.

The representative map is the union-find quotient generated by the zero-length slots. This is the public, unmarked counterpart of the private row-authoring censusSpec; unlike a bare DegSpec, it cannot contain an artificial identification unrelated to a vanishing slot.

Equations

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

Instances For

theorem AtanasovRanganathan.Configurations.faceSpec_eq_censusSpec {n p : ℕ} (core : Utilities.Certificate.ExplicitPotential.Core n p) (core_nonempty : 0 < n) (length : Fin p → ℕ) (forest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest core (zeroSlots length)) (not_loopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy core (zeroSlots length)) :

faceSpec core core_nonempty length forest not_loopy = Utilities.Certificate.ClosedFaceCensus.censusSpec core core_nonempty length forest not_loopy

The AR-facing closed subdivision is the generic public census subdivision. Keeping this equality named lets structural and generated closed-row proofs share one certificate layer without conversion boilerplate.

def AtanasovRanganathan.Configurations.ClosedSubdivisionDharConstruction {n p : ℕ} (core : Utilities.Certificate.ExplicitPotential.Core n p) (core_nonempty : 0 < n) :

A single AR construction valid on the whole genus-preserving closed orthant of a fixed core. This is now the primary hard-row obligation.

The only face hypotheses are the two intrinsic graph checks: the zero set is a forest and its contraction creates no surviving loop. Consequently one proof covers the positive subdivision and every honest nonloopy forest face, with no arbitrary representative map in the authoring interface.

Equations

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

Instances For

theorem AtanasovRanganathan.Configurations.ClosedSubdivisionDharConstruction.toPositiveSubdivisionPencil {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} {core_nonempty : 0 < n} (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (construction : ClosedSubdivisionDharConstruction core core_nonempty) :

PositiveSubdivisionPencil core core_nonempty core_loopless 4

The interior of a closed construction is the original positive-length AR pencil. This is the labor-saving direction: every row is authored closed, while its existing public PositiveSubdivisionPencil theorem is recovered without row-specific endpoint or contraction arguments.