pith. machine review for the scientific record. sign in
theorem proved term proof

past_is_fixed

show as:
view Lean formalization →

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)

 141theorem past_is_fixed (states : ℕ → LedgerSnapshot) (now : ℕ)
 142    (s : LedgerSnapshot) (hs : s ∈ past states now) :
 143    ∃ n, n < now ∧ states n = s := hs

proof body

Term-mode proof.

 144
 145/-! ## Time Does Not Exist Without Recognition -/
 146
 147/-- **Theorem (F-004 core)**: Time is not a background parameter.
 148    Time is DEFINED as the tick count. Without ledger updates, there is no time.
 149    The tick count is a natural number, not a real number.
 150    Continuous time is an approximation valid only for large tick counts. -/

depends on (14)

Lean names referenced from this declaration's body.