lemma proved term proof

`postedAt_accountAt`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

1005lemma postedAt_accountAt {d : Nat} [AtomicTick (AccountRS d)] (t : Nat) :
1006    AtomicTick.postedAt (M := AccountRS d) t (accountAt (d := d) t) := by

proof body

Term-mode proof.

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. -/

depends on (11)

Lean names referenced from this declaration's body.

AtomicTick in IndisputableMonolith.Chain decl_use
step in IndisputableMonolith.Complexity.CellularAutomata decl_use
tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
accountAt in IndisputableMonolith.LedgerPostingAdjacency decl_use
AccountRS in IndisputableMonolith.LedgerPostingAdjacency decl_use
AtomicTick in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
postedAt in IndisputableMonolith.Recognition.Cycle3 decl_use
AtomicTick in IndisputableMonolith.RRF.Core.Recognition decl_use