Reachability consequences of signed window profiles

The endpoint formula for a compatible window profile can be used directly as a linear-equivalence witness. These lemmas package that use for winnability and one-chip reachability without imposing restrictions on the profile slopes.

def Utilities.Certificate.WindowProfile.Data.endpointDivisors {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) : CFDiv spec.graph

The signed sum of the start and stop endpoint divisors of a profile.

Equations

• data.endpointDivisors = ∑ edge : Fin p, data.slope edge • (oneChip (spec.pathVertex edge (data.startPosition edge)) - oneChip (spec.pathVertex edge (data.stopPosition edge)))

theorem Utilities.Certificate.WindowProfile.Data.linearEquiv_add_endpointDivisors {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (D : CFDiv spec.graph) : linearEquiv spec.graph D (D + data.endpointDivisors)

Adding the signed endpoint divisor of a compatible window profile is a linear equivalence.

theorem Utilities.Certificate.WindowProfile.Data.winnable_add_endpointDivisors_iff {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (D : CFDiv spec.graph) : winnable spec.graph (D + data.endpointDivisors) ↔ winnable spec.graph D

Winnability is unchanged by adding the signed endpoint divisor of a compatible window profile.

theorem Utilities.Certificate.WindowProfile.Data.reaches_of_effective_endpointDivisors {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) {D : CFDiv spec.graph} {v : spec.Vertex} (hEffective : effective (D - oneChip v + data.endpointDivisors)) : StrongSeparator.Reaches spec.graph D v

If removing one chip and adding the signed endpoint divisor gives an effective divisor, then the original divisor reaches that vertex.