Foundation Time Emergence Arrow Well Defined

The arrow's definition

In ordinary physics, time is a background stage on which events unfold. The Recognition Science framework replaces that stage with a ledger: a discrete record of events, each carrying a tick number and a real-valued defect. There is no separate flowing time; the tick counter is time. The declaration arrow_well_defined states a conditional fact about this ledger: if a sequence of ledger snapshots is monotone, meaning each step advances the tick counter and never increases the defect, then the earlier snapshot is before the later one and the defect has not grown. The theorem proves that this ordering is consistent, not that any actual process must obey it.

The framework's library, a machine-checked collection of formal theorems, defines the arrow of time as the conjunction of two conditions: a later tick index and a defect that is less than or equal to the earlier one. The theorem arrow_well_defined shows that a monotone sequence satisfies this definition at every step. It also proves that the minimal temporal resolution is one tick: if one snapshot is before another, their tick indices differ by at least one. The past is the set of snapshots with smaller tick indices, the future the set with larger ones, and the present is the current snapshot. The past is fixed by definition: a snapshot in the past remains in the past.

What the declaration does not claim is as important as what it proves. The defect value here is an abstract nonnegative real number with no link to the framework's cost function. The monotonicity condition, DefectMonotone, is a structure: it carries the defect-decreasing property as a field. Every inhabitant of that structure arrives already oriented. The theorem unpacks that field; it does not derive the direction from the cost axioms. The framework's own documentation is explicit: the orientation of the arrow is funded by the floor at zero, while the dynamical claim that states actually move along it remains a premise. A separate theorem deriving monotonicity from the cost axioms would be needed to promote the dynamical half. Until then, the arrow of time in this framework is supplied, not derived.

This distinction matters for anyone reading the framework's claims. The theorem recognition_irreversible shows that a step with a strictly decreasing defect cannot be reversed by another step that restores the original defect. That is a statement about the types involved, not a physical law. The framework proves that the eight-tick cycle is the minimal complete update, and that this equals 2 to the third power. But the direction of time, the fact that states move from past to future, is a premise of the model, not a consequence of the cost function. The framework's library proves consistency conditions, not physical inevitability.

/-- **Conditional (F-006)**: given `DefectMonotone`, the temporal ordering and the defect ordering
    agree on a unit step. The direction is supplied by the `defect_decreasing` field of the
    hypothesis, so this establishes consistency of the two orderings, not the existence of the
    arrow. See the module retag note. -/
theorem arrow_well_defined (states : ℕ → LedgerSnapshot)
    (h : DefectMonotone states) (n : ℕ)
    (h_step : (states (n + 1)).tick.index = (states n).tick.index + 1) :
    arrow_of_time (states n) (states (n + 1)) := by
  constructor
  · show (states n).tick.index < (states (n + 1)).tick.index
    omega
  · exact h.defect_decreasing n h_step

/-- **Theorem**: The minimal temporal resolution is one tick.
    No sub-tick dynamics exist. Events are quantized in time. -/
theorem minimal_temporal_resolution :
    ∀ (s₁ s₂ : LedgerSnapshot),
    before s₁ s₂ → 1 ≤ s₂.tick.index - s₁.tick.index := by
  intro s₁ s₂ h
  unfold before at h
  omega

/-- **Theorem about the type `RecognitionStep`**: no step returns to a strictly higher defect.
    This follows from the `defect_reduce` field, which every step carries by construction, so it
    says that the type admits no such inhabitant. Read as physics it is conditional on the claim
    that recognition updates are `RecognitionStep`s. See the module retag note. -/
theorem recognition_irreversible (step : RecognitionStep)
    (h_strict : step.output.defect < step.input.defect) :
    ¬∃ (reverse : RecognitionStep),
      reverse.input = step.output ∧
      reverse.output.defect = step.input.defect := by
  intro ⟨rev, h_in, h_out⟩
  have h1 := rev.defect_reduce
  rw [h_in] at h1
  linarith

/-- **Theorem (F-004 core)**: Time is not a background parameter.
    Time is DEFINED as the tick count. Without ledger updates, there is no time.
    The tick count is a natural number, not a real number.
    Continuous time is an approximation valid only for large tick counts. -/
theorem time_is_discrete : epoch_length = 2 ^ (3 : ℕ) := by
  simp [epoch_length, DimensionForcing.eight_tick]

/-- **Definitional unfolding, not a theorem.** The proof is the hypothesis itself: membership in
    `past` *is* the existence of an earlier index with that state, so this restates the definition
    and establishes no immutability. The real content is `LedgerTime.past_immutable`, where
    committing a new entry provably leaves the earlier segment untouched, together with
    `LedgerTime.past_addressable` for address stability. Retained as a convenience projection. -/
theorem past_is_fixed (states : ℕ → LedgerSnapshot) (now : ℕ)
    (s : LedgerSnapshot) (hs : s ∈ past states now) :
    ∃ n, n < now ∧ states n = s := hs

What this page does not claim

This answer does not claim that the arrow of time is derived from the cost function. This answer does not claim that defect is linked to the framework's Jcost function. This answer does not claim that the direction of time is physically inevitable rather than a premise.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/TimeEmergence.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: