Iterated canonical bivalent splits

This module packages a finite sequence of the canonical positive one-edge splits from OneEdgeSplitRefinement. The numbers of core vertices and edge slots change at every step, so PackedSpec hides those indices while each CanonicalSplitStep retains the split occurrence, its two positive lengths, and the required length sum.

Composing the checked one-edge LaplacianEquivs gives a reusable transport from the original subdivision presentation to any presentation obtained by a finite chain of positive bivalent refinements. In particular, Brill--Noether existence is invariant along the whole chain.

structure Utilities.Certificate.IteratedSplitRefinement.PackedSpec : Type

A subdivision specification together with its dependent core sizes.

• n : ℕ

  The number of core vertices in the packed subdivision specification.

• p : ℕ

  The number of ordered core slots in the packed subdivision specification.

• spec : SubdivisionGraph.Spec self.n self.p

  The positive-length subdivision specification with the stored vertex and slot counts.

@[reducible, inline]

abbrev Utilities.Certificate.IteratedSplitRefinement.PackedSpec.graph (packed : PackedSpec) : CFGraph

The finite graph presented by a packed subdivision specification.

Equations

• packed.graph = packed.spec.graph

@[reducible, inline]

abbrev Utilities.Certificate.IteratedSplitRefinement.PackedSpec.Vertex (packed : PackedSpec) : Type

Its subdivision vertices.

Equations

• packed.Vertex = packed.spec.Vertex

def Utilities.Certificate.IteratedSplitRefinement.splitPacked (source : PackedSpec) (split : Fin source.p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) : PackedSpec

The target presentation produced by one canonical bivalent split.

Equations

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

structure Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitStep (source target : PackedSpec) : Type

A proof-carrying canonical bivalent split between packed presentations.

target_eq makes the target exactly the canonical split. Relabeling a separately generated presentation remains a subsequent LaplacianEquiv obligation.

• splitSlot : Fin source.p

  The source slot divided by this canonical split step.

• firstLength : ℕ

  The positive length of the first segment created by the split.

• secondLength : ℕ

  The positive length of the second segment, completing the original slot length.

• firstLength_pos : 0 < self.firstLength
• secondLength_pos : 0 < self.secondLength
• length_sum : source.spec.length self.splitSlot = self.firstLength + self.secondLength
• target_eq : target = splitPacked source self.splitSlot self.firstLength self.secondLength ⋯ ⋯

def Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitStep.laplacianEquiv {source target : PackedSpec} (step : CanonicalSplitStep source target) : LaplacianEquiv source.graph target.graph

The checked one-edge equivalence attached to a canonical split step.

Equations

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

inductive Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitChain (source : PackedSpec) : PackedSpec → Type

A data-carrying reflexive-transitive closure of canonical split steps.

Unlike Relation.ReflTransGen, this lives in Type: the endpoint graph equivalence retains the concrete split data instead of eliminating a proposition into computational data.

• refl {source : PackedSpec} : CanonicalSplitChain source source
• tail {source middle target : PackedSpec} : CanonicalSplitChain source middle → CanonicalSplitStep middle target → CanonicalSplitChain source target

def Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitChain.single {source target : PackedSpec} (step : CanonicalSplitStep source target) : CanonicalSplitChain source target

Regard one canonical split as a one-step chain.

Equations

• Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitChain.single step = Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitChain.refl.tail step

def Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitChain.append {source target : PackedSpec} (first : CanonicalSplitChain source target) {final : PackedSpec} : CanonicalSplitChain target final → CanonicalSplitChain source final

Concatenate two canonical split chains.

Equations

• first.append Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitChain.refl = first
• first.append (chain.tail step) = (first.append chain).tail step

def Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitChain.laplacianEquivAux (source : PackedSpec) {target : PackedSpec} : CanonicalSplitChain source target → LaplacianEquiv source.graph target.graph

Compose the one-edge equivalences along a split chain.

Equations

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

def Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitChain.laplacianEquiv {source target : PackedSpec} (chain : CanonicalSplitChain source target) : LaplacianEquiv source.graph target.graph

Compose the one-edge equivalences along a split chain.

Equations

• chain.laplacianEquiv = Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitChain.laplacianEquivAux source chain

def Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitChain.vertexEquiv {source target : PackedSpec} (chain : CanonicalSplitChain source target) : source.Vertex ≃ target.Vertex

The vertex transport determined by a split chain.

Equations

• chain.vertexEquiv = chain.laplacianEquiv.toEquiv

theorem Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitChain.bnExists_iff {source target : PackedSpec} (chain : CanonicalSplitChain source target) (r d : ℤ) : BNExists source.graph r d ↔ BNExists target.graph r d

Iterated positive bivalent splitting preserves Brill--Noether existence, in both directions and for every rank and degree.