The h-generic value identity and Definition 5 normal-form theorem

For a closed fragment, an arbitrary mixed functional's Definition 5 summand equals the (κ, o)-free normal form — the engine of Eulerian independence.

The h-generic value identity

theorem RS.hMaster_colouringOfFlip {k ℓ : ℕ} (h : MixedFunctional k ℓ) (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) : hMaster h W (colouringOfFlip W F o ψ φ) = (-1) ^ κ.circuitCount * ∏ v : W.Vertex, ↑(F.oddSignAt o φ v) * h.evalOdd (F.evenColoursAt ψ v) (F.oddListAt o φ v)

The h-generic value identity: the h-generic master summand of the flipped data colouring equals the circuit sign times the vertex product of oddSign times evalOdd.

The normal-form theorem

theorem RS.mixedSummand_eq_nf {k ℓ : ℕ} (h : MixedFunctional k ℓ) (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : F.mixedSummand h o = defFiveNF h W F

The normal-form theorem: the mixed summand of any transition data equals the (κ, o)-free normal form defFiveNF.

Closed-fragment Eulerian independence

theorem RS.eulerian_independence_closed {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (h : MixedFunctional k ℓ) {κ κ' : F.TransitionSystem} (o : κ.Orientation) (o' : κ'.Orientation) : F.mixedSummand h o = F.mixedSummand h o'

Closed-fragment Eulerian independence: the Definition 5 summand of a closed fragment's edge subset does not depend on the transition system and orientation.

The choice-free value lemma

theorem RS.mixedValue_eq_summand_closed {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (h : MixedFunctional k ℓ) {κ : F.TransitionSystem} (o : κ.Orientation) : F.mixedValue h = F.mixedSummand h o

The choice-free value lemma: under any concrete transition data, the choice-based mixedValue equals the mixedSummand.