`minimal_temporal_resolution`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.TimeEmergence
domain: Foundation
line: 156 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.TimeEmergence on GitHub at line 156.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 153
 154/-- **Theorem**: The minimal temporal resolution is one tick.
 155    No sub-tick dynamics exist. Events are quantized in time. -/
 156theorem minimal_temporal_resolution :
 157    ∀ (s₁ s₂ : LedgerSnapshot),
 158    before s₁ s₂ → 1 ≤ s₂.tick.index - s₁.tick.index := by
 159  intro s₁ s₂ h
 160  unfold before at h
 161  omega
 162
 163/-! ## Summary Certificate -/
 164
 165/-- **F-004/F-006 Certificate**: Time emergence and arrow of time.
 166    1. Time = tick count (discrete, no background)
 167    2. Arrow = defect decrease direction
 168    3. Recognition is irreversible
 169    4. 8-tick epoch is the minimal complete cycle -/
 170theorem time_emergence_certificate :
 171    epoch_length = 8 ∧
 172    epoch_length = 2 ^ 3 ∧
 173    (∀ step : RecognitionStep,
 174      step.output.defect < step.input.defect →
 175      ¬∃ rev : RecognitionStep,
 176        rev.input = step.output ∧ rev.output.defect = step.input.defect) :=
 177  ⟨epoch_length_eq, time_is_discrete, fun step h => recognition_irreversible step h⟩
 178
 179end TimeEmergence
 180end Foundation
 181end IndisputableMonolith

papers checked against this theorem

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