A loop-split interface for the genus-four loop lemma

Atanasov--Ranganathan contract two topological loops, use genus two on the contracted graph, and then lift the resulting degree-three divisor back across the loops. In the certificate model a topological loop is represented by a bivalent core marker joined to its base by two subdivided edge slots.

This file formalizes the rank-theoretic end of that argument. The embedded core is already known to be a strong separator, so it is enough to reach the original core vertices and the loop markers. Reaching a marker can in turn be split into two small pieces: a representative carrying two chips at the loop base and the standard degree-two reflection move on the loop.

The remaining geometric input for the full loop lemma is deliberately visible in the hypotheses of bnExists_three_of_two_loop_split_witness: one must construct the two-chip representatives after contracting the loops and prove the reflection move uniformly for two subdivided paths of arbitrary positive lengths. Neither assertion is silently delegated to generated data here.

def Utilities.Certificate.GenusFourLoopLemma.HasTwoChipsRepresentative {G : CFGraph} (D : CFDiv G) (base : G.V) : Prop

The divisor class of D has an effective representative carrying two chips at base. This is the exact pointed input needed to enter an attached topological loop.

Equations

• Utilities.Certificate.GenusFourLoopLemma.HasTwoChipsRepresentative D base = ∃ (E : CFDiv G), effective E ∧ linearEquiv G D E ∧ 2 ≤ E base

theorem Utilities.Certificate.GenusFourLoopLemma.exists_common_two_chip_class_genus_two {G : CFGraph} (hConnected : graphConnected G) (hGenus : G.genus = 2) (first second : G.V) : ∃ (D : CFDiv G), effective D ∧ CFDiv.degree D = 3 ∧ rank G D ≥ 1 ∧ HasTwoChipsRepresentative D first ∧ HasTwoChipsRepresentative D second

The genus-two algebraic heart of the Atanasov--Ranganathan loop lemma. For any two prospective loop bases, one degree-three class has effective representatives carrying two chips at either base.

def Utilities.Certificate.GenusFourLoopLemma.TwoChipReflection {G : CFGraph} (base target : G.V) : Prop

A two-chip reflection move from base through target. On a cycle, the second output chip is the reflection of target in base. Writing the move as an exact principal divisor keeps this interface independent of any particular cycle coordinates.

Equations

• Utilities.Certificate.GenusFourLoopLemma.TwoChipReflection base target = ∃ (reflected : G.V) (script : firingScript G), (prin G) script = -2 • oneChip base + oneChip target + oneChip reflected

def Utilities.Certificate.GenusFourLoopLemma.markerBorrowScript {G : CFGraph} (target : G.V) : firingScript G

Borrow once at a loop marker. When the marker is joined to its base by two unit edges and has no other neighbors, this is the complete two-chip reflection script.

Equations

• Utilities.Certificate.GenusFourLoopLemma.markerBorrowScript target vertex = if vertex = target then -1 else 0

theorem Utilities.Certificate.GenusFourLoopLemma.twoChipReflection_of_doubleEdgeMarker {G : CFGraph} {base target : G.V} (hDistinct : base ≠ target) (hDouble : numEdges G base target = 2) (hNoOther : ∀ (vertex : G.V), vertex ≠ base → numEdges G target vertex = 0) : TwoChipReflection base target

The split model's unsubdivided double edge realizes a two-chip reflection: borrowing at its bivalent marker moves two chips from the base to the marker. This is the length-one endpoint of the arbitrary-length cycle bridge still needed for the full loop lemma.

Reflection through two arbitrarily subdivided paths

def Utilities.Certificate.GenusFourLoopLemma.loopRampPotential {n : ℕ} (marker : Fin n) (depth : ℕ) : Fin n → ℤ

The core potential used to move two chips from a loop base towards its marker. Its depth is the length of the shorter path.

Equations

• Utilities.Certificate.GenusFourLoopLemma.loopRampPotential marker depth vertex = if vertex = marker then -↑depth else 0

theorem Utilities.Certificate.GenusFourLoopLemma.twoChipReflection_of_two_oriented_paths {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (base marker : Fin n) (first second : Fin p) (hFirstSecond : first ≠ second) (hFirstTail : spec.core.tail first = base) (hFirstHead : spec.core.head first = marker) (hSecondTail : spec.core.tail second = base) (hSecondHead : spec.core.head second = marker) (hOnly : ∀ (edge : Fin p), spec.core.tail edge = marker ∨ spec.core.head edge = marker → edge = first ∨ edge = second) (hLengthOrder : spec.length first ≤ spec.length second) : TwoChipReflection (spec.coreVertex base) (spec.coreVertex marker)

Two parallel oriented core slots, with no other slot incident to their common head, realize the standard two-chip reflection. The reflected chip lands at the marker when the paths have equal length; otherwise it lands on the longer path at the same distance from the base as the marker is along the shorter path.

This is the arbitrary-length metric statement left implicit in the published Atanasov--Ranganathan loop argument.

theorem Utilities.Certificate.GenusFourLoopLemma.twoChipReflection_of_two_paths {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (base marker : Fin n) (first second : Fin p) (hFirstSecond : first ≠ second) (hFirstTail : spec.core.tail first = base) (hFirstHead : spec.core.head first = marker) (hSecondTail : spec.core.tail second = base) (hSecondHead : spec.core.head second = marker) (hOnly : ∀ (edge : Fin p), spec.core.tail edge = marker ∨ spec.core.head edge = marker → edge = first ∨ edge = second) : TwoChipReflection (spec.coreVertex base) (spec.coreVertex marker)

Order-free form of twoChipReflection_of_two_oriented_paths.

theorem Utilities.Certificate.GenusFourLoopLemma.effective_sub_two_chips {G : CFGraph} {E : CFDiv G} {base : G.V} (hEffective : effective E) (hTwo : 2 ≤ E base) : effective (E - 2 • oneChip base)

Removing two chips at one vertex from an effective divisor that carries at least two there remains effective.

theorem Utilities.Certificate.GenusFourLoopLemma.reaches_of_twoChipsRepresentative_of_twoChipReflection {G : CFGraph} {D : CFDiv G} {base target : G.V} (hRepresentative : HasTwoChipsRepresentative D base) (hReflection : TwoChipReflection base target) : StrongSeparator.Reaches G D target

A two-chip representative and a loop reflection make the divisor reach the chosen loop vertex.

theorem Utilities.Certificate.GenusFourLoopLemma.bnExists_of_reaches_coreVertices {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (hConnected : graphConnected spec.graph) (D : CFDiv spec.graph) (degree : ℤ) (hDegree : CFDiv.degree D = degree) (hReaches : ∀ (vertex : Fin n), StrongSeparator.Reaches spec.graph D (spec.coreVertex vertex)) : BNExists spec.graph 1 degree

A direct strong-separator wrapper: reaching every embedded core vertex of a connected positive subdivision proves rank one. This statement is useful independently of loops and avoids forcing callers through the affine-potential certificate format.

def Utilities.Certificate.GenusFourLoopLemma.splitSubdivisionSpec {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (data : core.SplitMetadata) (hValid : data.Valid) (length : Fin core.splitEdgeCount → ℕ) (hLength : ∀ (edge : Fin core.splitEdgeCount), 0 < length edge) : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount

The concrete positive subdivision carried by valid loop-split metadata.

Equations

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

theorem Utilities.Certificate.GenusFourLoopLemma.bnExists_three_of_two_loop_split_witness {n : ℕ} (core : GenusFourPseudocore.Pseudocore n) (data : core.SplitMetadata) (hValid : data.Valid) (_hTwoLoops : 2 ≤ core.loopCount) (length : Fin core.splitEdgeCount → ℕ) (hLength : ∀ (edge : Fin core.splitEdgeCount), 0 < length edge) (D : CFDiv (splitSubdivisionSpec data hValid length hLength).graph) (hDegree : CFDiv.degree D = 3) (hBaseReaches : ∀ (base : Fin n), StrongSeparator.Reaches (splitSubdivisionSpec data hValid length hLength).graph D ((splitSubdivisionSpec data hValid length hLength).coreVertex (core.baseVertex base))) (hLoopWitness : ∀ (marker : Fin core.loopCount), HasTwoChipsRepresentative D ((splitSubdivisionSpec data hValid length hLength).coreVertex (core.baseVertex (data.markerBase marker))) ∧ TwoChipReflection ((splitSubdivisionSpec data hValid length hLength).coreVertex (core.baseVertex (data.markerBase marker))) ((splitSubdivisionSpec data hValid length hLength).coreVertex (core.markerVertex marker))) : BNExists (splitSubdivisionSpec data hValid length hLength).graph 1 3

A compact, honest split-model form of the genus-four two-loop lemma.

The marker count identifies the two-loop configurations covered by the theorem. Original vertices are discharged by hBaseReaches. For each semantic loop, hLoopWitness supplies the two independent ingredients formalized above, after which the embedded-core strong-separator theorem handles every subdivision-interior vertex automatically.