No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
924theorem postingStep_iff_legalAtomicTick {d : Nat} {L L' : LedgerState d} :
925 PostingStep (d := d) L L' ↔ LegalAtomicTick (d := d) L L' :=
proof body
Term-mode proof.
926 ⟨postingStep_implies_legalAtomicTick (d := d), legalAtomicTick_implies_PostingStep (d := d)⟩
927
928/-! ### Optional B3-style tightening: minimal cost (among monotone, nontrivial steps) ⇒ posting -/
929
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (14)
Lean names referenced from this declaration's body.
-
nontrivial
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
LedgerState
in IndisputableMonolith.Foundation.VariationalDynamics
decl_use
-
LedgerState
in IndisputableMonolith.Information.InformationIsLedger
decl_use
-
LedgerState
in IndisputableMonolith.Information.Thermodynamics
decl_use
-
LedgerState
in IndisputableMonolith.LedgerPostingAdjacency
decl_use
-
LegalAtomicTick
in IndisputableMonolith.LedgerPostingAdjacency
decl_use
-
legalAtomicTick_implies_PostingStep
in IndisputableMonolith.LedgerPostingAdjacency
decl_use
-
PostingStep
in IndisputableMonolith.LedgerPostingAdjacency
decl_use
-
postingStep_implies_legalAtomicTick
in IndisputableMonolith.LedgerPostingAdjacency
decl_use
-
LedgerState
in IndisputableMonolith.QFT.GaugeInvariance
decl_use
-
L
in IndisputableMonolith.Recognition
decl_use
-
L
in IndisputableMonolith.Recognition.Cycle3
decl_use