The ledgers in value form

The pairing-preserving ledgers restated for the pairing-resolved signed value: existence of a matching canonical orientation plus equality of signed summands is exactly preservation of signedValueAt together with transfer of canonical-orientation existence. The single-step disjunct is a theorem (stepLedger_single), so the move ledger in value form reduces to the paired step in value form.

def RS.PairedValueLedger : Prop

The paired step, value form: across a π-returning repair block, canonical-orientation existence transfers and the pairing-resolved signed value is preserved.

Equations

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

theorem RS.EdgeSubset.pairedLedger_iff_value : PairedLedger ↔ PairedValueLedger

The paired step and its value form are equivalent.

theorem RS.EdgeSubset.signedValueAt_samePairing_of_value {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (HPaired : PairedValueLedger) {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 from the value step: the full well-definedness with the paired input in value form.