Split-metadata compatibility (light half)

The Compatible predicate records the parts of split-metadata validity needed for gluing: marker multiplicities, looplessness, and preservation of edge multiplicities. It is genus-generic and follows directly from ValidAt. The marker-fibre counting lemma below supports comparison of two compatible presentations.

structure Utilities.Certificate.PseudocoreSplitGlue.Compatible {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (data : core.SplitMetadata) : Prop

The three pieces of split-metadata validity that the glue actually uses. Cut connectedness of the split core is deliberately not included.

• markers (vertex : Fin n) : data.markerMultiplicity vertex = core.loops vertex
• loopless (edge : Fin core.splitEdgeCount) : data.splitCore.tail edge ≠ data.splitCore.head edge
• multiplicity (first second : Fin (n + core.loopCount)) : GenusFourPseudocore.Pseudocore.explicitCoreMultiplicity data.splitCore first second = data.expectedMultiplicity first second

theorem Utilities.Certificate.PseudocoreSplitGlue.compatible_of_validAt {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} {data : core.SplitMetadata} {g : ℕ} (hValid : data.ValidAt g) : Compatible data

Recovering the omitted connectedness field

theorem Utilities.Certificate.PseudocoreSplitGlue.splitCore_connected_of_compatible {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (data : core.SplitMetadata) (hCoreConnected : core.Connected) (hCompatible : Compatible data) : data.splitCore.Connected

Although Compatible deliberately omits a connectedness field, a compatible split of a connected pseudocore is automatically connected.

For a cut separating two base vertices, use pseudocore connectedness and the checked base--base multiplicity. If a displayed marker lies on the opposite side from its base, its checked double edge crosses the cut. These two cases exhaust arbitrary cuts of the displayed split.

theorem Utilities.Certificate.PseudocoreSplitGlue.validAt_of_coreValid_compatible {n g : ℕ} {core : GenusFourPseudocore.Pseudocore n} (data : core.SplitMetadata) (hValid : core.ValidAt g) (hCompatible : Compatible data) : data.ValidAt g

Core validity plus the lightweight glue predicate reconstructs the full checked split validity.

theorem Utilities.Certificate.PseudocoreSplitGlue.card_markerFiber {n m : ℕ} {source : GenusFourPseudocore.Pseudocore n} {target : GenusFourPseudocore.Pseudocore m} (sourceSplit : source.SplitMetadata) (targetSplit : target.SplitMetadata) (vertexEquiv : Fin n ≃ Fin m) (hSource : ∀ (vertex : Fin n), sourceSplit.markerMultiplicity vertex = source.loops vertex) (hTarget : ∀ (vertex : Fin m), targetSplit.markerMultiplicity vertex = target.loops vertex) (hLoops : ∀ (i : Fin n), source.loops i = target.loops (vertexEquiv i)) (w : Fin m) : Fintype.card { x : Fin source.loopCount // vertexEquiv (sourceSplit.markerBase x) = w } = Fintype.card { y : Fin target.loopCount // targetSplit.markerBase y = w }

Fibres of markerBase over corresponding base vertices have the same size, because both count semantic loops at that vertex.