Transferring a script by comparing path endpoint slopes

A source subdivision replaces every vanishing slot by one unit edge. After summing over contraction classes those edges cancel. On surviving slots, increasing the outgoing endpoint contributions preserves effectivity. This isolates the graph bookkeeping from the integer rounding argument.

theorem Utilities.Certificate.DiscreteSpecialization.source_prin_classSum {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (s : SubdivisionGraph.Spec n p) (hCore : s.core = d.core) (f : firingScript s.graph) (r : Fin n) : ∑ v : Fin n with d.rep v = d.rep r, (prin s.graph) f (s.coreVertex v) = ∑ e : Fin p, ((if d.rep (d.core.tail e) = d.rep r then TwoPoleSubdivision.pathValue s f e 1 - TwoPoleSubdivision.pathValue s f e 0 else 0) + if d.rep (d.core.head e) = d.rep r then -(TwoPoleSubdivision.pathValue s f e (s.length e - 1 + 1) - TwoPoleSubdivision.pathValue s f e (s.length e - 1)) else 0)

The source endpoint sum, regrouped by target contraction classes.

theorem Utilities.Certificate.DiscreteSpecialization.effective_of_endpoint_comparison {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (s : SubdivisionGraph.Spec n p) (hCore : s.core = d.core) (hZero : ∀ (e : Fin p), d.length e = 0 → s.length e = 1) (weight : Fin n → ℤ) (f : firingScript s.graph) (hf : effective (Subdivision.SubdivisionCoreSupport.coreDivisor s weight + (prin s.graph) f)) (g : firingScript d.graph) (slope : Fin p → ℕ → ℤ) (hg : d.IsStepSlope g slope) (hTail : ∀ (e : Fin p), 0 < d.length e → TwoPoleSubdivision.pathValue s f e 1 - TwoPoleSubdivision.pathValue s f e 0 ≤ slope e 0) (hHead : ∀ (e : Fin p), 0 < d.length e → slope e (d.length e - 1) ≤ TwoPoleSubdivision.pathValue s f e (s.length e - 1 + 1) - TwoPoleSubdivision.pathValue s f e (s.length e - 1)) (hInterior : ∀ (e : Fin p) (k : Fin (d.length e - 1)), slope e ↑k ≤ slope e (↑k + 1)) : effective (d.coreClassDivisor weight + (prin d.graph) g)

Only endpoint comparisons and interior convexity are needed to transfer effectivity. Both scripts are actual functions on their respective graphs.

Rounded firing scripts on a contracted subdivision

An effective translate of a core-supported divisor makes the source script convex along every slot. Sample its values every N steps and use one common rounding offset. If the rounded core values agree on contraction classes, they define a script on the target graph. Convex block estimates then give the endpoint comparisons and interior convexity needed to retain effectivity.

theorem Utilities.Certificate.DiscreteSpecialization.winning_path_slopes_mono {n p : ℕ} (s : SubdivisionGraph.Spec n p) (weight : Fin n → ℤ) (f : firingScript s.graph) (hf : effective (Subdivision.SubdivisionCoreSupport.coreDivisor s weight + (prin s.graph) f)) (e : Fin p) (a b : ℕ) : a ≤ b → b < s.length e → ConvexIntegerRounding.slope (TwoPoleSubdivision.pathValue s f e) a ≤ ConvexIntegerRounding.slope (TwoPoleSubdivision.pathValue s f e) b

A winning script for a core-supported divisor has nondecreasing unit slopes along every slot, since there are no prescribed interior chips.

theorem Utilities.Certificate.DiscreteSpecialization.rounded_script_effective {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (s : SubdivisionGraph.Spec n p) (hCore : s.core = d.core) (N : ℕ) (hN : 0 < N) (hZero : ∀ (e : Fin p), d.length e = 0 → s.length e = 1) (hPos : ∀ (e : Fin p), 0 < d.length e → s.length e = N * d.length e) (weight : Fin n → ℤ) (f : firingScript s.graph) (hf : effective (Subdivision.SubdivisionCoreSupport.coreDivisor s weight + (prin s.graph) f)) (k : Fin N) (hConst : ∀ (u v : Fin n), d.rep u = d.rep v → CommonOffsetRounding.round N k (f (s.coreVertex u)) = CommonOffsetRounding.round N k (f (s.coreVertex v))) : ∃ (g : firingScript d.graph), effective (d.coreClassDivisor weight + (prin d.graph) g)

Common-offset rounding transfers an effective translate to the target subdivision once its rounded core values are constant on contracted classes. No nonnegativity assumption on the initial core weights is needed.

Finite specialization by a common rounding offset

Stretch surviving lengths by N and replace vanishing slots by unit edges. When N exceeds the degree bound times the number of vanishing slots, integer rounding turns a winning core-supported script into a winning script on the contracted graph. No metric graph or limiting argument enters.

def Utilities.Certificate.DiscreteSpecialization.stretch {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (N : ℕ) (hN : 0 < N) (hLoopless : ∀ (e : Fin p), d.core.tail e ≠ d.core.head e) : SubdivisionGraph.Spec n p

The positive graph used to prove a specified contraction face.

Equations

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

@[simp]

theorem Utilities.Certificate.DiscreteSpecialization.stretch_core {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (N : ℕ) (hN : 0 < N) (hLoopless : ∀ (e : Fin p), d.core.tail e ≠ d.core.head e) : (stretch d N hN hLoopless).core = d.core

theorem Utilities.Certificate.DiscreteSpecialization.stretch_length_zero {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (N : ℕ) (hN : 0 < N) (hLoopless : ∀ (e : Fin p), d.core.tail e ≠ d.core.head e) (e : Fin p) (he : d.length e = 0) : (stretch d N hN hLoopless).length e = 1

theorem Utilities.Certificate.DiscreteSpecialization.stretch_length_pos {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (N : ℕ) (hN : 0 < N) (hLoopless : ∀ (e : Fin p), d.core.tail e ≠ d.core.head e) (e : Fin p) (he : 0 < d.length e) : (stretch d N hN hLoopless).length e = N * d.length e

theorem Utilities.Certificate.DiscreteSpecialization.constant_on_classes {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (hRep : ∀ (u v : Fin n), d.rep u = d.rep v → ContractionForestCensusGeneral.ReachIn d.core {e : Fin p | d.length e = 0} u v) (potential : Fin n → ℤ) (hZero : ∀ (e : Fin p), d.length e = 0 → potential (d.core.tail e) = potential (d.core.head e)) (u v : Fin n) : d.rep u = d.rep v → potential u = potential v

Equality on zero-slot endpoints propagates through the actual contraction relation. A bare cardinality condition on the representative map would not be enough here.

theorem Utilities.Certificate.DiscreteSpecialization.exists_descending_offset {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (N : ℕ) (hN : 0 < N) (hLoopless : ∀ (e : Fin p), d.core.tail e ≠ d.core.head e) (hRep : ∀ (u v : Fin n), d.rep u = d.rep v → ContractionForestCensusGeneral.ReachIn d.core {e : Fin p | d.length e = 0} u v) (weight majorant : Fin n → ℤ) (hMajorant : ∀ (v : Fin n), 0 ≤ majorant v) (hLe : ∀ (v : Fin n), weight v ≤ majorant v) (hBudget : ↑{e : Fin p | d.length e = 0}.card * ∑ v : Fin n, majorant v < ↑N) (f : firingScript (stretch d N hN hLoopless).graph) (hf : effective (Subdivision.SubdivisionCoreSupport.coreDivisor (stretch d N hN hLoopless) weight + (prin (stretch d N hN hLoopless).graph) f)) : ∃ (k : Fin N), ∀ (u v : Fin n), d.rep u = d.rep v → CommonOffsetRounding.round N k (f ((stretch d N hN hLoopless).coreVertex u)) = CommonOffsetRounding.round N k (f ((stretch d N hN hLoopless).coreVertex v))

A winning script has a common rounding offset that agrees throughout each contracted component. The degree bound may use any effective majorant of its signed starting divisor.

theorem Utilities.Certificate.DiscreteSpecialization.winning_script_coreClassDivisor_of_stretch {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (N : ℕ) (hN : 0 < N) (hLoopless : ∀ (e : Fin p), d.core.tail e ≠ d.core.head e) (hRep : ∀ (u v : Fin n), d.rep u = d.rep v → ContractionForestCensusGeneral.ReachIn d.core {e : Fin p | d.length e = 0} u v) (weight majorant : Fin n → ℤ) (hMajorant : ∀ (v : Fin n), 0 ≤ majorant v) (hLe : ∀ (v : Fin n), weight v ≤ majorant v) (hBudget : ↑{e : Fin p | d.length e = 0}.card * ∑ v : Fin n, majorant v < ↑N) (f : firingScript (stretch d N hN hLoopless).graph) (hf : effective (Subdivision.SubdivisionCoreSupport.coreDivisor (stretch d N hN hLoopless) weight + (prin (stretch d N hN hLoopless).graph) f)) : ∃ (g : firingScript d.graph), effective (d.coreClassDivisor weight + (prin d.graph) g)

Quantitative discrete specialization of a core-supported winning script. The graph is stretched only once; the offset depends on the script.

theorem Utilities.Certificate.DiscreteSpecialization.winnable_coreClassDivisor_of_stretch {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (N : ℕ) (hN : 0 < N) (hLoopless : ∀ (e : Fin p), d.core.tail e ≠ d.core.head e) (hRep : ∀ (u v : Fin n), d.rep u = d.rep v → ContractionForestCensusGeneral.ReachIn d.core {e : Fin p | d.length e = 0} u v) (weight majorant : Fin n → ℤ) (hMajorant : ∀ (v : Fin n), 0 ≤ majorant v) (hLe : ∀ (v : Fin n), weight v ≤ majorant v) (hBudget : ↑{e : Fin p | d.length e = 0}.card * ∑ v : Fin n, majorant v < ↑N) (hWin : winnable (stretch d N hN hLoopless).graph (Subdivision.SubdivisionCoreSupport.coreDivisor (stretch d N hN hLoopless) weight)) : winnable d.graph (d.coreClassDivisor weight)

Winnability descends from one sufficiently stretched positive instance. The signed source weights may have any effective pointwise majorant.

Closing a fixed rank-one divisor over contraction faces

A nonnegative core weight with rank at least one on every positive integer subdivision keeps rank at least one after the zero-length slots contract. For each demanded core chip, finite specialization uses the original weight as its effective majorant. The existing closed-face separator supplies the remaining subdivision-interior rank tests.

def Utilities.Certificate.DiscreteSpecialization.subChipWeight {n : ℕ} (weight : Fin n → ℤ) (anchor v : Fin n) : ℤ

Subtract one chip at a named original core vertex.

Equations

• Utilities.Certificate.DiscreteSpecialization.subChipWeight weight anchor v = weight v - if v = anchor then 1 else 0

theorem Utilities.Certificate.DiscreteSpecialization.coreDivisor_subChipWeight {n p : ℕ} (s : SubdivisionGraph.Spec n p) (weight : Fin n → ℤ) (anchor : Fin n) : Subdivision.SubdivisionCoreSupport.coreDivisor s (subChipWeight weight anchor) = Subdivision.SubdivisionCoreSupport.coreDivisor s weight - oneChip (s.coreVertex anchor)

Subtracting a named core chip commutes with positive subdivision.

theorem Utilities.Certificate.DiscreteSpecialization.coreClassDivisor_subChipWeight {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (weight : Fin n → ℤ) (anchor : Fin n) : d.coreClassDivisor (subChipWeight weight anchor) = d.coreClassDivisor weight - oneChip (d.coreVertex anchor)

A single named chip pushes to a single chip on its contracted class, even when other original vertices belong to that class.

theorem Utilities.Certificate.DiscreteSpecialization.rank_ge_one_coreClassDivisor_of_stretch {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (N : ℕ) (hN : 0 < N) (hConnected : d.core.Connected) (hLoopless : ∀ (e : Fin p), d.core.tail e ≠ d.core.head e) (hRep : ∀ (u v : Fin n), d.rep u = d.rep v → ContractionForestCensusGeneral.ReachIn d.core {e : Fin p | d.length e = 0} u v) (weight : Fin n → ℤ) (hWeight : ∀ (v : Fin n), 0 ≤ weight v) (hBudget : ↑{e : Fin p | d.length e = 0}.card * ∑ v : Fin n, weight v < ↑N) (hRank : rank (stretch d N hN hLoopless).graph (Subdivision.SubdivisionCoreSupport.coreDivisor (stretch d N hN hLoopless) weight) ≥ 1) : rank d.graph (d.coreClassDivisor weight) ≥ 1

A core-supported rank-one divisor on one sufficiently stretched graph already gives rank one after contraction. Its weights need not belong to a single family that works on every positive subdivision.

theorem Utilities.Certificate.DiscreteSpecialization.rank_ge_one_coreClassDivisor_of_positive {n p : ℕ} (d : DegenerateSpec.DegSpec n p) (hConnected : d.core.Connected) (hLoopless : ∀ (e : Fin p), d.core.tail e ≠ d.core.head e) (hRep : ∀ (u v : Fin n), d.rep u = d.rep v → ContractionForestCensusGeneral.ReachIn d.core {e : Fin p | d.length e = 0} u v) (weight : Fin n → ℤ) (hWeight : ∀ (v : Fin n), 0 ≤ weight v) (hPositive : ∀ (s : SubdivisionGraph.Spec n p), s.core = d.core → rank s.graph (Subdivision.SubdivisionCoreSupport.coreDivisor s weight) ≥ 1) : rank d.graph (d.coreClassDivisor weight) ≥ 1

Fixed nonnegative core weights that have rank one on every positive subdivision retain rank one on any actual closed contraction face.