All-internal agreement: Eulerian independence outright

A standard TransitionSystem on an edge subset forces every participating flag to be internally attached (attach_internal), so the subset is all-internal even inside an open fragment. This file generalizes the closed-fragment agreement chain of ClosedAgreement.lean from Fragment (Fin 0) to arbitrary fragments under allInternal: through-edges vanish, the core colouring is the full odd colouring, and the open circuit count is the standard circuit count.

The genuinely new ingredient is the boundary state. On an open fragment the even boundary match is not vacuous: it pins the even colouring at the (non-participating) boundary flags. Instead, each even colouring ψ induces the all-even state evenState ψ recording its boundary values; the even boundary match for evenState ψ₀ holds exactly on the fibre {ψ | evenState ψ = evenState ψ₀}, and the mixed summand decomposes fibrewise into through summands over the finitely many realized states. Applying the unconditional all-internal independence (throughSummand_independence_of_allInternal) fibre by fibre proves the Eulerian-independence interface outright. No state is ever chosen — every state used is manufactured from an existing even colouring — so no (k, ℓ) = (0, 0) edge case arises.

Vacuous through-data on all-internal subsets

theorem RS.EdgeSubset.attach_inl_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) {f : W.Flag} (hf : f ∈ F.flags) : ∃ (v : W.Vertex), W.attach f = Sum.inl v

On an all-internal subset, every participating flag attaches to an internal vertex.

theorem RS.EdgeSubset.throughFlags_eq_empty_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) : F.throughFlags = ∅

On an all-internal subset, there are no through-flags.

theorem RS.EdgeSubset.coreFlags_eq_flags_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) : F.coreFlags = F.flags

On an all-internal subset, the core flags are the full flags.

theorem RS.EdgeSubset.throughProduct_one_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} [LinearOrder α] (hall : F.allInternal) {k ℓ : ℕ} (st : GenBoundaryState k ℓ α) : F.throughProduct st = 1

On an all-internal subset, the through product is 1.

theorem RS.EdgeSubset.boundaryFlag_notMem_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) (i : α) : W.boundaryFlag i ∉ F.flags

On an all-internal subset, no boundary flag participates.

The boundary state of an even colouring

noncomputable def RS.EdgeSubset.evenState {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) {k : ℕ} (ℓ : ℕ) (ψ : F.EvenColouring k) : GenBoundaryState k ℓ α

The all-even boundary state recording an even colouring's values at the boundary flags.

Equations

• RS.EdgeSubset.evenState hall ℓ ψ i = Sum.inl (↑ψ ⟨W.boundaryFlag i, ⋯⟩)

theorem RS.EdgeSubset.evenState_matches {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) {k : ℕ} (ℓ : ℕ) (ψ : F.EvenColouring k) : genBoundarySubsetMatches W F.flags (evenState hall ℓ ψ)

The state of an even colouring satisfies the boundary subset matching condition.

theorem RS.EdgeSubset.coreOddBoundaryMatch_evenState {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) {k ℓ : ℕ} (ψ₀ : F.EvenColouring k) (φ : F.CoreOddColouring ℓ) : F.coreOddBoundaryMatch (evenState hall ℓ ψ₀) φ

The core odd boundary match holds vacuously at an even state.

theorem RS.EdgeSubset.genEvenBoundaryMatch_evenState_iff {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) {k ℓ : ℕ} (ψ₀ ψ : F.EvenColouring k) : genEvenBoundaryMatch F (evenState hall ℓ ψ₀) ⋯ ψ ↔ evenState hall ℓ ψ = evenState hall ℓ ψ₀

The even boundary match at the state of ψ₀ holds exactly on the fibre of ψ₀.

The colouring equivalence

noncomputable def RS.EdgeSubset.coreOddEquivAll {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) (ℓ : ℕ) : F.CoreOddColouring ℓ ≃ F.OddColouring ℓ

On an all-internal subset, the core odd colouring type is equivalent to the full odd colouring type, via coreFlags = flags.

Equations

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

Vertex-local data agreement

theorem RS.EdgeSubset.coreOddListAt_eq_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) {ℓ : ℕ} {κ : F.TransitionSystem} (o : κ.Orientation) (φ_core : F.CoreOddColouring ℓ) (v : W.Vertex) : F.coreOddListAt o.toRel φ_core v = F.oddListAt o ((coreOddEquivAll hall ℓ) φ_core) v

coreOddListAt at φ_core agrees with oddListAt at coreOddEquivAll φ_core.

theorem RS.EdgeSubset.coreOddSignAt_eq_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) {ℓ : ℕ} {κ : F.TransitionSystem} (o : κ.Orientation) (φ_core : F.CoreOddColouring ℓ) (v : W.Vertex) : F.coreOddSignAt o.toRel φ_core v = F.oddSignAt o ((coreOddEquivAll hall ℓ) φ_core) v

coreOddSignAt at φ_core agrees with oddSignAt at coreOddEquivAll φ_core.

Circuit count agreement

theorem RS.EdgeSubset.openCircuitCount_toRel {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) : κ.toRelTransitionSystem.openCircuitCount = κ.circuitCount

The open circuit count of a standard transition system's relative system equals the standard circuit count.

The through summand at an even state

theorem RS.EdgeSubset.throughSummand_evenState {α : Type} {W : Fragment α} {F : EdgeSubset W} [LinearOrder α] (hall : F.allInternal) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (ψ₀ : F.EvenColouring k) {κ : F.TransitionSystem} (o : κ.Orientation) : F.throughSummand h (evenState hall ℓ ψ₀) ⋯ o.toRel κ.toRelTransitionSystem.openCircuitCount = (-1) ^ κ.circuitCount * ∑ ψ : F.EvenColouring k, if evenState hall ℓ ψ = evenState hall ℓ ψ₀ then ∑ φ : F.OddColouring ℓ, ∏ v : W.Vertex, ↑(F.oddSignAt o φ v) * h.evalOdd (F.evenColoursAt ψ v) (F.oddListAt o φ v) else 0

Fibre bridge: the through summand at the state of ψ₀ equals the circuit-signed colouring sum over the fibre of ψ₀.

The fibre decomposition of the mixed summand

theorem RS.EdgeSubset.mixedSummand_eq_fibre_sum {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) {k ℓ : ℕ} (h : MixedFunctional k ℓ) {κ : F.TransitionSystem} (o : κ.Orientation) : F.mixedSummand h o = ∑ st ∈ Finset.image (evenState hall ℓ) Finset.univ, (-1) ^ κ.circuitCount * ∑ ψ : F.EvenColouring k, if evenState hall ℓ ψ = st then ∑ φ : F.OddColouring ℓ, ∏ v : W.Vertex, ↑(F.oddSignAt o φ v) * h.evalOdd (F.evenColoursAt ψ v) (F.oddListAt o φ v) else 0

Fibre decomposition: the mixed summand is the sum over the realized boundary states of the fibre sums.

The Eulerian-independence interface, proved

theorem RS.eulerianIndependence : EulerianIndependence

Eulerian independence (Regts–Sevenster arXiv:1807.04494, Proposition 3, as a theorem): the Definition 5 mixed summand of an edge subset does not depend on the choice of transition system and orientation.