`legalAtomicTick_oneBitDiff`

proved

show as: view math explainer →

module: IndisputableMonolith.LedgerPostingAdjacency
domain: LedgerPostingAdjacency
line: 994 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.LedgerPostingAdjacency on GitHub at line 994.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 991    simpa [hcost'] using this
 992  exact postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 (d := d) (L := L) (L' := L') hmono hneq hleJ1
 993
 994theorem legalAtomicTick_oneBitDiff {d : Nat} {L L' : LedgerState d}
 995    (h : LegalAtomicTick (d := d) L L') :
 996    OneBitDiff (parity d L) (parity d L') :=
 997  postingStep_oneBitDiff (legalAtomicTick_implies_PostingStep (d := d) h)
 998
 999/-! ## Workstream B tightening: RS AtomicTick ⇒ PostingStep (legality predicate) -/
1000
1001/-- Choose the unique posted account at tick `t` from an RS `AtomicTick` instance. -/
1002noncomputable def accountAt {d : Nat} [AtomicTick (AccountRS d)] (t : Nat) : Fin d :=
1003  Classical.choose (ExistsUnique.exists (AtomicTick.unique_post (M := AccountRS d) t))
1004
1005lemma postedAt_accountAt {d : Nat} [AtomicTick (AccountRS d)] (t : Nat) :
1006    AtomicTick.postedAt (M := AccountRS d) t (accountAt (d := d) t) := by
1007  have hex : ∃ u : Fin d, AtomicTick.postedAt (M := AccountRS d) t u :=
1008    ExistsUnique.exists (AtomicTick.unique_post (M := AccountRS d) t)
1009  simpa [accountAt] using (Classical.choose_spec hex)
1010
1011/-- An RS-atomic tick step, parameterized by an explicit debit/credit side schedule. -/
1012noncomputable def stepAt {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1013    LedgerState d :=
1014  post L (accountAt (d := d) t) (sideAt t)
1015
1016lemma stepAt_isPostingStep {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1017    PostingStep (d := d) L (stepAt (d := d) sideAt t L) := by
1018  refine ⟨accountAt (d := d) t, sideAt t, rfl⟩
1019
1020theorem stepAt_oneBitDiff {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1021    OneBitDiff (parity d L) (parity d (stepAt (d := d) sideAt t L)) :=
1022  postingStep_oneBitDiff (stepAt_isPostingStep (d := d) sideAt t L)
1023
1024/-! ## A per-tick posting schedule induces an adjacent walk in parity space -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.