Localizing a guarding picture to one chip-free component

AtanasovRanganathan.Guarding.GuardingSet asks, for every chip-free core vertex v and every degenerate spec d over the core, for

Reaches d.graph (d.coreClassDivisor chips) (d.coreVertex v).

Every picture in the library discharges that by exhibiting a firing script on the whole of d.graph and checking its residual there. That is why the library's pictures are indexed by the ambient core and not by the shape of the component being guarded: a component of four vertices sitting in a ten-vertex core has to have its Dhar arithmetic rewritten from scratch.

This file supplies the alternative. reaches_coreVertex_of_induced_script is the same conclusion, but its arithmetic hypothesis lives on the induced subgraph cut out by a vertex set A -- typically the component together with the chip vertices it hangs from. The only extra obligation is that the script vanish at the vertices of A which have an edge leaving A.

interior_of_steps is the combinatorial criterion which discharges the interiority obligation on a subdivision: a vertex is interior to A as soon as every unit step touching it has its other end in A.

What this buys

A component's picture becomes a statement about the component, provable once and reusable in every ambient core the shape occurs in. Concretely, the genus-six "two-banana chain" (auxiliary calculations Sec. 5a) occupies six of core 46's ten vertices; localizing to it replaces a genus-six Dhar calculation by a genus-two one with two frozen endpoints.

Layering

Utilities only: DegSpec already lives here, so LowGenus picture files may use this directly.

theorem Utilities.Gluing.DegSpec.interior_of_steps {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (A : Finset d.Vertex) (x : d.Vertex) (hLeft : ∀ (s : d.Step), d.stepLeft s.fst s.snd = x → d.stepRight s.fst s.snd ∈ A) (hRight : ∀ (s : d.Step), d.stepRight s.fst s.snd = x → d.stepLeft s.fst s.snd ∈ A) : Interior d.graph A x

Interiority on a subdivision is a statement about unit steps. If every unit step with an end at x has its other end inside A, then no edge at x leaves A.

theorem Utilities.Gluing.DegSpec.reaches_coreVertex_of_induced_script {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (weight : Fin n → ℤ) (hWeight : ∀ (v : Fin n), 0 ≤ weight v) {A : Finset d.Vertex} (hA : A.Nonempty) {v : Fin n} (hv : d.coreVertex v ∈ A) {t : firingScript (inducedSubgraph d.graph A hA)} (ht : SupportInterior t) (hEff : effective ((fun (x : (inducedSubgraph d.graph A hA).V) => d.coreClassDivisor weight ↑x) - oneChip ⟨d.coreVertex v, hv⟩ + (prin (inducedSubgraph d.graph A hA)) t)) : Certificate.StrongSeparator.Reaches d.graph (d.coreClassDivisor weight) (d.coreVertex v)

The shape of a guarding discharge, localized.

This is GuardingSet.guard's conclusion, obtained from a local Dhar move computed inside the induced subgraph on A. hOff is free for a chip assignment, since coreClassDivisor of nonnegative weights is effective.