The Eulerian-independence interface

Regts–Sevenster's Proposition 3: the Definition 5 summand of an Eulerian edge subset does not depend on the choice of transition system and orientation. This Prop names the statement; it is proved as RS.eulerianIndependence in RS/Novel/Skein/AllInternalAgreement.lean. mixedValue_eq_summand eliminates the choice in EdgeSubset.mixedValue against any concrete transition data.

def RS.EulerianIndependence : Prop

The Eulerian-independence statement (Regts–Sevenster, arXiv:1807.04494, Proposition 3): the mixed summand is independent of the transition system and orientation. Proved as RS.eulerianIndependence in RS/Novel/Skein/AllInternalAgreement.lean.

Equations

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

theorem RS.EdgeSubset.mixedValue_eq_summand (hInd : EulerianIndependence) {α : Type} {W : Fragment α} (F : EdgeSubset W) {k ℓ : ℕ} (h : MixedFunctional k ℓ) {κ : F.TransitionSystem} (o : κ.Orientation) : F.mixedValue h = F.mixedSummand h o

Under Eulerian independence, the choice-based value of an edge subset equals the summand at any concrete transition data.

theorem RS.EdgeSubset.mixedValue_transport (hInd : EulerianIndependence) {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) (F : EdgeSubset W₁) {k ℓ : ℕ} (h : MixedFunctional k ℓ) : ((transport e) F).mixedValue h = F.mixedValue h

Transport invariance of the Definition 5 value: under the Eulerian-independence input, the choice-based value of a transported edge subset is the original value.

theorem RS.mixedPartition_transport (hInd : EulerianIndependence) {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {k ℓ : ℕ} (h : MixedFunctional k ℓ) : mixedPartition h W₁ = mixedPartition h W₂

Isomorphism invariance of the mixed partition function: under the Eulerian-independence input, equivalent fragments have equal Definition 5 values.