Documentation

LeanPool.RegtsSevenster.RS.Novel.Skein.PairingValue

The pairing-resolved signed value #

The signed canonical summand of a single transition system, chosen among its path-canonical orientations. Within one system the choice is immaterial (throughSummand_pathCanonical); across systems with the same boundary pairing it is invariant given the pairing-preserving ledger — the well-definedness of the value as a function of the pairing, riding on the proved block connectivity.

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

The signed canonical summand of one system: the path sign times the through summand at the open circuit count, at a chosen path-canonical orientation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem RS.EdgeSubset.signedValueAt_eq {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ : F.RelTransitionSystem} (o : κ.Orientation) (hc : PathCanonical o) :
    F.signedValueAt hM st hbnd κ = pathSign κ * F.throughSummand hM st hbnd o κ.openCircuitCount

    The signed value evaluates at any concrete path-canonical orientation.

    source
    theorem RS.EdgeSubset.canonical_transfer_of_samePairing {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (HLedger : MatchPreservingLedger) {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ κ' : F.RelTransitionSystem} (hsp : SamePairing κ κ') (o : κ.Orientation) (hc : PathCanonical o) :
    ∃ (o' : κ'.Orientation), PathCanonical o'

    Canonical-orientation existence transfers along the same pairing, given the ledger: fold the ledger down the block chain and cross the final MatchEq.

    source
    theorem RS.EdgeSubset.signedValueAt_samePairing {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (HLedger : MatchPreservingLedger) {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ κ' : F.RelTransitionSystem} (hsp : SamePairing κ κ') :
    F.signedValueAt hM st hbnd κ = F.signedValueAt hM st hbnd κ'

    Same-pairing invariance of the signed value (conditional on the pairing-preserving ledger): the signed canonical summand is a function of the boundary pairing alone.