Ordered path refinements

IteratedSplitRefinement records arbitrary finite chains of canonical positive bivalent splits. This module supplies the list-shaped constructor needed by emitted metric certificates: replace one positive subdivision slot by an ordered nonempty list of positive segment lengths with the same total.

The construction is deliberately elementary. Keep the first segment in the named slot, put the remaining total in the fresh last slot, and recurse on that fresh slot. No graph search, quotient, or normalization enters. A final LaplacianEquiv is kept as an explicit presentation obligation, since an external certificate generally orders its bivalent vertices and edge occurrences differently from this canonical append-at-the-end convention.

def Utilities.Certificate.IteratedSplitRefinement.pathHeadStep (source : PackedSpec) (slot : Fin source.p) (first : ℕ) (rest : List ℕ) (first_pos : 0 < first) (rest_sum_pos : 0 < rest.sum) (length_sum : source.spec.length slot = first + rest.sum) : CanonicalSplitStep source (splitPacked source slot first rest.sum first_pos rest_sum_pos)

The first canonical step in an ordered path split.

Equations

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

inductive Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplitValid (source : PackedSpec) (slot : Fin source.p) (segments : List ℕ) (target : PackedSpec) : CanonicalSplitChain source target → Prop

Proposition-level evidence that a retained split chain is exactly the left-to-right recursion described by a segment list. Keeping the chain as an index lets OrderedPathSplit eliminate into computational transport data without asking Lean to generate a SizeOf instance for a nested dependent inductive family.

• singleton (source : PackedSpec) (slot : Fin source.p) : OrderedPathSplitValid source slot [source.spec.length slot] source CanonicalSplitChain.refl
• cons (source : PackedSpec) (slot : Fin source.p) (first : ℕ) (rest : List ℕ) (first_pos : 0 < first) (rest_sum_pos : 0 < rest.sum) (length_sum : source.spec.length slot = first + rest.sum) {target : PackedSpec} {tailChain : CanonicalSplitChain (splitPacked source slot first rest.sum first_pos rest_sum_pos) target} (tail : OrderedPathSplitValid (splitPacked source slot first rest.sum first_pos rest_sum_pos) (OneEdgeSplitRefinement.secondSlot source.spec) rest target tailChain) : OrderedPathSplitValid source slot (first :: rest) target ((CanonicalSplitChain.single (pathHeadStep source slot first rest first_pos rest_sum_pos length_sum)).append tailChain)

structure Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit (source : PackedSpec) (slot : Fin source.p) (segments : List ℕ) (target : PackedSpec) : Type

A canonical replacement of one slot by an ordered list of positive segments. The proof field pins the retained chain to the elementary append-at-the-end construction.

• chain : CanonicalSplitChain source target

  The canonical split chain whose validity field certifies the prescribed ordered path segments.

• valid : OrderedPathSplitValid source slot segments target self.chain

def Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.positiveSegments (segments : List ℕ) : List ℕ

Delete zero-length source segments before constructing a positive split chain. These are precisely the segments contracted on a closed DV cone face.

Equations

• Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.positiveSegments segments = List.filter (fun (length : ℕ) => decide (0 < length)) segments

@[simp]

theorem Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.sum_positiveSegments (segments : List ℕ) : (positiveSegments segments).sum = segments.sum

theorem Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.positiveSegments_all_pos (segments : List ℕ) (length : ℕ) : length ∈ positiveSegments segments → 0 < length

theorem Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.positiveSegments_ne_nil {segments : List ℕ} (hSum : 0 < segments.sum) : positiveSegments segments ≠ []

def Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.singleton (source : PackedSpec) (slot : Fin source.p) : OrderedPathSplit source slot [source.spec.length slot] source

The no-op path refinement by the original singleton length.

Equations

• Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.singleton source slot = { chain := Utilities.Certificate.IteratedSplitRefinement.CanonicalSplitChain.refl, valid := ⋯ }

def Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.cons (source : PackedSpec) (slot : Fin source.p) (first : ℕ) (rest : List ℕ) (first_pos : 0 < first) (rest_sum_pos : 0 < rest.sum) (length_sum : source.spec.length slot = first + rest.sum) {target : PackedSpec} (tail : OrderedPathSplit (splitPacked source slot first rest.sum first_pos rest_sum_pos) (OneEdgeSplitRefinement.secondSlot source.spec) rest target) : OrderedPathSplit source slot (first :: rest) target

Prepend one segment by splitting off first, then follow a recursively constructed refinement of the fresh remainder slot.

Equations

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

theorem Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.sum_eq {source target : PackedSpec} {slot : Fin source.p} {segments : List ℕ} (split : OrderedPathSplit source slot segments target) : segments.sum = source.spec.length slot

The listed segment lengths add to the original slot length.

theorem Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.all_pos {source target : PackedSpec} {slot : Fin source.p} {segments : List ℕ} (split : OrderedPathSplit source slot segments target) (length : ℕ) : length ∈ segments → 0 < length

Every segment in an ordered path split is positive.

@[irreducible]

noncomputable def Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.ofList (source : PackedSpec) (slot : Fin source.p) (segments : List ℕ) : segments ≠ [] → (∀ length ∈ segments, 0 < length) → segments.sum = source.spec.length slot → (target : PackedSpec) × OrderedPathSplit source slot segments target

Construct the canonical ordered refinement from a positive nonempty list whose sum is the named slot length.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.ofList x✝¹ x✝ [] nonempty x_6 x_7 = ⋯.elim

noncomputable def Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.ofListWithZeros (source : PackedSpec) (slot : Fin source.p) (segments : List ℕ) (sum_eq : segments.sum = source.spec.length slot) : (target : PackedSpec) × OrderedPathSplit source slot (positiveSegments segments) target

Construct the positive canonical path refinement represented by a list which may contain zero entries. Zero entries disappear before splitting; the final RefinementPresentation.relabeling is the explicit obligation that identifies this positive canonical model with the contracted closed-face presentation used by a certificate.

Equations

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

theorem Utilities.Certificate.IteratedSplitRefinement.OrderedPathSplit.bnExists_iff {source target : PackedSpec} {slot : Fin source.p} {segments : List ℕ} (split : OrderedPathSplit source slot segments target) (r d : ℤ) : BNExists source.graph r d ↔ BNExists target.graph r d

Ordered path refinement preserves every Brill--Noether existence statement.

structure Utilities.Certificate.IteratedSplitRefinement.RefinementPresentation (source : PackedSpec) (presented : CFGraph) : Type u_1

A canonical positive refinement followed by an arbitrary checked relabeling to the presentation used by an emitted certificate.

• refined : PackedSpec

  The subdivision specification reached after the canonical refinements.

• chain : CanonicalSplitChain source self.refined

  The checked sequence of canonical splits from the source to the refined specification.

• relabeling : LaplacianEquiv self.refined.graph presented

  The edge-multiplicity-preserving relabeling from the refined graph to the presented graph.

def Utilities.Certificate.IteratedSplitRefinement.RefinementPresentation.ofChain {source : PackedSpec} {presented : CFGraph} {refined : PackedSpec} (chain : CanonicalSplitChain source refined) (relabeling : LaplacianEquiv refined.graph presented) : RefinementPresentation source presented

Package a split chain and its final checked relabeling.

Equations

• Utilities.Certificate.IteratedSplitRefinement.RefinementPresentation.ofChain chain relabeling = { refined := refined, chain := chain, relabeling := relabeling }

def Utilities.Certificate.IteratedSplitRefinement.RefinementPresentation.ofOrderedPathSplit {source : PackedSpec} {presented : CFGraph} {slot : Fin source.p} {segments : List ℕ} {refined : PackedSpec} (split : OrderedPathSplit source slot segments refined) (relabeling : LaplacianEquiv refined.graph presented) : RefinementPresentation source presented

Package one ordered path split and its final checked relabeling.

Equations

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

def Utilities.Certificate.IteratedSplitRefinement.RefinementPresentation.laplacianEquiv {source : PackedSpec} {presented : CFGraph} (presentation : RefinementPresentation source presented) : LaplacianEquiv source.graph presented

The composite Laplacian equivalence from the stable subdivision to the certificate presentation.

Equations

• presentation.laplacianEquiv = presentation.chain.laplacianEquiv.trans presentation.relabeling

theorem Utilities.Certificate.IteratedSplitRefinement.RefinementPresentation.bnExists_iff {source : PackedSpec} {presented : CFGraph} (presentation : RefinementPresentation source presented) (r d : ℤ) : BNExists source.graph r d ↔ BNExists presented r d

A checked positive refinement presentation preserves every Brill--Noether existence statement, in both directions.