Pseudocore presentation in bridgeless genus two

This is the constructive bivalent-path reduction behind the topological classification of a bridgeless genus-two graph. It specializes the generic pseudocore normalization to show that the retained base core has at most two vertices; bivalent semantic-loop markers are retained by the pseudocore construction rather than accidentally suppressed.

inductive Bananas.BridgelessGenusTwoCoreNormalForm (G : CFGraph) : Prop

The two topological models produced by the genus-two pseudocore normalization. The wedge branch deliberately records the intrinsic pointed-rigid genus-one factors; replacing them by explicitly indexed cycles is a separate genus-one presentation step.

• theta {G : CFGraph} (B : Banana 2) (equivalence : Utilities.Certificate.LaplacianEquiv G (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : BridgelessGenusTwoCoreNormalForm G
• rigidWedge {G : CFGraph} (base factor : CFGraph) (attachment : base.V) (root : factor.V) (baseConnected : _root_.graphConnected base) (baseGenus : base.genus = 1) (baseCut : Utilities.TwoEdgeCutCondition base) (factorCut : Utilities.TwoEdgeCutCondition factor) (wedgeCut : Utilities.TwoEdgeCutCondition (Utilities.vertexWedge base factor attachment root)) (baseRigid : Utilities.PointedGenusOneRigid base attachment) (factorRigid : Utilities.PointedGenusOneRigid factor root) (equivalence : Utilities.Certificate.LaplacianEquiv G (Utilities.vertexWedge base factor attachment root)) : BridgelessGenusTwoCoreNormalForm G

inductive Bananas.MarkedBridgelessGenusTwoCoreNormalForm (G : CFGraph) (u v : G.V) : Prop

The same structural alternatives with the two marked vertices carried explicitly to the model graph.

• theta {G : CFGraph} {u v : G.V} (B : Banana 2) (u' v' : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) (equivalence : Utilities.CFGraphIso G (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (uEquation : equivalence.vertexEquiv u = u') (vEquation : equivalence.vertexEquiv v = v') : MarkedBridgelessGenusTwoCoreNormalForm G u v
• rigidWedge {G : CFGraph} {u v : G.V} (base factor : CFGraph) (attachment : base.V) (root : factor.V) (u' v' : (Utilities.vertexWedge base factor attachment root).V) (baseConnected : _root_.graphConnected base) (baseGenus : base.genus = 1) (baseCut : Utilities.TwoEdgeCutCondition base) (factorCut : Utilities.TwoEdgeCutCondition factor) (wedgeCut : Utilities.TwoEdgeCutCondition (Utilities.vertexWedge base factor attachment root)) (baseRigid : Utilities.PointedGenusOneRigid base attachment) (factorRigid : Utilities.PointedGenusOneRigid factor root) (equivalence : Utilities.CFGraphIso G (Utilities.vertexWedge base factor attachment root)) (uEquation : equivalence.vertexEquiv u = u') (vEquation : equivalence.vertexEquiv v = v') : MarkedBridgelessGenusTwoCoreNormalForm G u v

theorem Bananas.pseudocore_baseVertexCount_eq_one_or_two {n : ℕ} (core : Utilities.Certificate.GenusFourPseudocore.Pseudocore n) (hValid : core.ValidAt 2) (hBound : n ≤ 2) : n = 1 ∨ n = 2

A valid genus-two pseudocore with at most two base vertices has either one or two base vertices. The impossible zero-vertex case already contradicts the Euler edge equation.

theorem Bananas.pseudocore_loopCount_eq_zero_or_two_of_two_base_vertices (core : Utilities.Certificate.GenusFourPseudocore.Pseudocore 2) (hValid : core.ValidAt 2) : core.loopCount = 0 ∨ core.loopCount = 2

In the two-base-vertex genus-two pseudocore case, semantic loops occur at both base vertices or at neither. These are respectively the two-cycle wedge and theta branches after splitting loop markers.

theorem Bananas.pseudocore_loopCount_eq_two_of_one_base_vertex (core : Utilities.Certificate.GenusFourPseudocore.Pseudocore 1) (hValid : core.ValidAt 2) : core.loopCount = 2

The one-base-vertex genus-two pseudocore consists of two semantic loops.

theorem Bananas.pseudocore_valence_eq_three_of_two_base_vertices (core : Utilities.Certificate.GenusFourPseudocore.Pseudocore 2) (hValid : core.ValidAt 2) (vertex : Fin 2) : core.valence vertex = 3

A valid genus-two pseudocore on two base vertices is exactly cubic.

theorem Bananas.thetaPresentation_of_loopFree_twoBasePseudocore (core : Utilities.Certificate.GenusFourPseudocore.Pseudocore 2) (hValid : core.ValidAt 2) (hLoops : core.loopCount = 0) (spec : Utilities.Certificate.SubdivisionGraph.Spec (2 + core.loopCount) core.splitEdgeCount) {G : CFGraph} (hPresentation : Nonempty (Utilities.Certificate.LaplacianEquiv G spec.graph)) : ∃ (B : Banana 2), Nonempty (Utilities.Certificate.LaplacianEquiv G (Utilities.Certificate.SubdivisionGraph.Spec.graph B))

A loop-free two-base-vertex genus-two pseudocore presentation is already a theta (Banana 2) presentation. No separate graph construction is needed: a positive subdivision with two core vertices and three slots is definitionally the banana model.

theorem Bananas.bridgelessGenusTwo_pseudocorePresentation (G : CFGraph) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hGenus : G.genus = 2) : ∃ (k : ℕ) (core : Utilities.Certificate.GenusFourPseudocore.Pseudocore k) (split : core.SplitMetadata), k ≤ 2 ∧ core.ValidAt 2 ∧ Utilities.Certificate.PseudocoreSplitGlue.Compatible split ∧ ∃ (spec : Utilities.Certificate.SubdivisionGraph.Spec (k + core.loopCount) core.splitEdgeCount), spec.core = split.splitCore ∧ Nonempty (Utilities.Certificate.LaplacianEquiv G spec.graph)

Every nontrivial bridgeless genus-two graph is Laplacian-equivalent to a positive subdivision of the loopless split of a valid genus-two pseudocore with at most two base vertices.

theorem Bananas.bridgelessGenusTwo_coreNormalForm (G : CFGraph) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hGenus : G.genus = 2) : BridgelessGenusTwoCoreNormalForm G

Construct the theta-or-rigid-wedge structural form of every nontrivial bridgeless genus-two graph.

theorem Bananas.marked_bridgelessGenusTwo_coreNormalForm (G : CFGraph) (u v : G.V) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hGenus : G.genus = 2) : MarkedBridgelessGenusTwoCoreNormalForm G u v

Transport the two marks through the structural core normal form.