Path-canonical orientations and the corrected independence

The orientation counterexample shows the constrained summand genuinely depends on the orientation of boundary-to-boundary chains; only circuit-supported differences are invisible. The correction: orient every chain canonically, from its lower-labelled boundary end to its higher-labelled one. Two path-canonical orientations of the same system then differ only on circuits, so the circuit-restricted invariance makes the canonical summand well-defined; the corrected value chooses among canonical data, and the corrected independence interface quantifies over it.

def RS.EdgeSubset.PathCanonical {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) : Prop

Path-canonical orientation: every participating boundary-to-boundary chain is directed from its lower-labelled end to its higher-labelled one — the entry edge at the lower end is incoming.

Equations

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

theorem RS.EdgeSubset.pathCanonical_of_allInternal {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) {κ : F.RelTransitionSystem} (o : κ.Orientation) : PathCanonical o

On an all-internal subset every orientation is path-canonical: there are no participating boundary flags.

def RS.EdgeSubset.ChordCross {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (b b' : ↥F.boundaryFlags) : Prop

The chord-interleaving condition between two boundary chains: both chords are recorded at their lower-labelled ends and interleave.

Equations

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

noncomputable def RS.EdgeSubset.chordCrossingCount {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : ℕ

The number of interleaving chain-chord pairs of a transition system.

Equations

• RS.EdgeSubset.chordCrossingCount κ = {bb ∈ F.boundaryFlags.attach ×ˢ F.boundaryFlags.attach | RS.EdgeSubset.ChordCross κ bb.1 bb.2}.card

noncomputable def RS.EdgeSubset.pathSign {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : ℂ

The path-sector sign: the crossing sign of the boundary chain pairing — the Pfaffian chord-diagram sign forced by the two-path repair obstruction.

Equations

• RS.EdgeSubset.pathSign κ = (-1) ^ RS.EdgeSubset.chordCrossingCount κ

theorem RS.EdgeSubset.pathSign_of_allInternal {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) (κ : F.RelTransitionSystem) : pathSign κ = 1

On an all-internal subset the path sign is trivial.

def RS.EdgeSubset.CanonData {α : Type} [LinearOrder α] {W : Fragment α} (F : EdgeSubset W) : Type

Canonical transition data: a relative system with a path-canonical orientation.

Equations

• F.CanonData = ((κ : F.RelTransitionSystem) × { o : κ.Orientation // RS.EdgeSubset.PathCanonical o })

noncomputable def RS.EdgeSubset.throughValueC {α : Type} [LinearOrder α] {W : Fragment α} (F : EdgeSubset W) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) : ℂ

The canonical constrained value: the through summand at the open circuit count, chosen among path-canonical data.

Equations

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

noncomputable def RS.throughMixedPartitionC {α : Type} [LinearOrder α] {k ℓ : ℕ} (h : MixedFunctional k ℓ) (W : Fragment α) (st : GenBoundaryState k ℓ α) : ℂ

The canonical state-constrained partition value of an open fragment.

Equations

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

theorem RS.EdgeSubset.throughSummand_canonical_unique {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ : F.RelTransitionSystem} {o o' : κ.Orientation} (_hc : PathCanonical o) (_hc' : PathCanonical o') (hchain : ∀ f ∈ F.internalFlags, o.isOut f ≠ o'.isOut f → W.pairing f ∈ F.internalFlags) (c : ℕ) : F.throughSummand h st hbnd o c = F.throughSummand h st hbnd o' c

Two path-canonical orientations of one system differ only on circuit components, so their summands agree — the difference set avoids every chain (both orientations direct each chain the same way) and is therefore pairing-closed on internal flags.

def RS.ThroughIndependenceC : Prop

The corrected independence interface: the constrained summand at the open circuit count is independent of the choice of relative transition system and path-canonical orientation.

Equations

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