Encyclopedia Foundation Foundation Initial Condition Past Theorem

ARTICLE 4 claims 4 theorems

Foundation Initial Condition Past Theorem

A machine-checked theorem proves a universe of perfect balance is the unique lowest-cost state, but it does not prove that state lies in the past.

Verify this page

The Forced Minimum

The declaration past_theorem proves a precise fact about any collection of ledger entries, where a ledger is a discrete record of events. Imagine each entry carries a positive real number, a ratio. The theorem concerns the total defect, a measure of how far the entries stray from the value one, with defect zero meaning perfect balance. The result is threefold: a configuration with zero total defect exists, it is the unique such configuration, and it is the global minimum of the defect function. In plain terms, there is exactly one way to arrange the entries so that nothing is out of balance, and that arrangement has the lowest possible total defect.

This is a genuine theorem, machine-checked in the framework's library of formal theorems. It follows from the cost axioms that define the defect, and it is not a definitional choice. The theorem also connects to entropy: the framework defines entropy as proportional to total defect, so the unique minimum-defect configuration is also the unique minimum-entropy state. Any configuration with at least one entry not equal to one has positive entropy. The mathematics here is clean and complete.

What the theorem does not do is attribute this minimum state to the past. The name past_theorem is a target, not an achievement. The proof establishes minimality as a property of the potential, but being initial is a property of the direction of travel along that potential. Those are separate claims, and the framework's own dynamics currently point the wrong way. Each variational tick, a step of the recognition cycle, is defined to pick the feasible minimizer, so the defect descends in the tick index by construction. The unity configuration is the attractor every trajectory runs toward, not the state it runs from. Calling the minimum the past would reverse the tree's own dynamics.

In Recognition Science, the traditional Past Hypothesis of cosmology, the idea that the universe began in a low-entropy state, does not become a proved theorem here. It becomes a proved uniqueness-and-minimality result plus an open question about which end of time sits at the minimum. The gate for restoring the temporal reading is stated explicitly: either a derivation that physical time runs along increasing defect, which would invert the tick order, or a dynamics that provably departs from unity rather than descending to it. Until one of those holds, the minimum is a fact about the potential, not about the origin.

The consequence is a sharper question. Thermal equilibrium is not merely improbable in this framework; it is uniquely non-minimal, and there is exactly one zero-cost configuration. The puzzle of why the universe started with low entropy becomes the puzzle of why time runs away from the minimum, not toward it. That is a different and still substantial question, one the framework has not yet answered.

THEOREM past_theorem · IndisputableMonolith/Foundation/InitialCondition.lean
past_theorem · IndisputableMonolith/Foundation/InitialCondition.lean:156 
/-- **Unique global minimality, with no temporal attribution.** What is proved, and it is a real
    theorem: the zero-defect configuration exists, is the unique such configuration, and is the
    global minimum of `total_defect`. That is forced by the cost axioms and is the honest F-005
    content.

    The word "initial" is not proved anywhere and currently has the wrong sign. Each variational
    tick is DEFINED to pick the feasible minimizer
    (`VariationalDynamics.IsVariationalSuccessor`), so defect descends in the tick index by
    construction and `unity_config` is the attractor every trajectory runs toward, not the state it
    runs from. Calling the minimum "the past" therefore reverses the tree's own dynamics.

    So this does not yet answer Penrose, Albert, or Boltzmann. It answers a different and still
    substantial question: thermal equilibrium is not merely improbable but uniquely non-minimal,
    and there is exactly one zero-cost configuration.

    Gate for restoring the temporal reading, either branch sufficing: a derivation that physical
    time runs along INCREASING `total_defect`, which inverts the tick order of the variational
    update and needs its own independent justification; or a dynamics that provably departs from
    unity rather than descending to it. `Foundation.ReadingArrowSweep` gives the criterion this is
    measured against, and `Holography.ObserverHorizonOrientation` shows the direction cannot be
    borrowed from a boundary. -/
theorem past_theorem {N : ℕ} (hN : 0 < N) :
    (∃! c : Configuration N, total_defect c = 0) ∧
    total_defect (unity_config N hN) = 0 ∧
    (∀ c : Configuration N, total_defect (unity_config N hN) ≤ total_defect c) := by
  refine ⟨⟨unity_config N hN, unity_defect_zero hN, ?_⟩, unity_defect_zero hN,
    unity_is_global_minimum hN⟩
  intro c hc
  have h_entries : ∀ i, c.entries i = 1 :=
    (zero_defect_iff_unity hN c).mp hc
  have h_u_entries : ∀ i, (unity_config N hN).entries i = 1 := fun _ => rfl
  have h_eq : c.entries = (unity_config N hN).entries :=
    funext fun i => by rw [h_entries i, h_u_entries i]
  exact Configuration.mk.injEq .. |>.mpr h_eq
THEOREM initial_state_minimum_entropy · IndisputableMonolith/Foundation/InitialCondition.lean
initial_state_minimum_entropy · IndisputableMonolith/Foundation/InitialCondition.lean:138 
/-- **Theorem**: The initial state has minimum entropy. -/
theorem initial_state_minimum_entropy {N : ℕ} (hN : 0 < N) :
    entropy (unity_config N hN) = 0 := unity_defect_zero hN
THEOREM nonunity_positive_entropy · IndisputableMonolith/Foundation/InitialCondition.lean
nonunity_positive_entropy · IndisputableMonolith/Foundation/InitialCondition.lean:142 
/-- **Theorem**: Any non-unity state has positive entropy. -/
theorem nonunity_positive_entropy {N : ℕ} (_hN : 0 < N) (c : Configuration N)
    (h : ∃ i, c.entries i ≠ 1) : 0 < entropy c := by
  obtain ⟨j, hj⟩ := h
  have hj_pos : 0 < LawOfExistence.defect (c.entries j) :=
    LawOfExistence.defect_pos_of_ne_one (c.entries_pos j) hj
  calc 0 < LawOfExistence.defect (c.entries j) := hj_pos
    _ ≤ ∑ i : Fin N, LawOfExistence.defect (c.entries i) := by
        apply Finset.single_le_sum (f := fun i => LawOfExistence.defect (c.entries i))
          (fun i _ => LawOfExistence.defect_nonneg (c.entries_pos i))
          (Finset.mem_univ j)
THEOREM past_theorem · IndisputableMonolith/Foundation/InitialCondition.lean
past_theorem · IndisputableMonolith/Foundation/InitialCondition.lean:156 
/-- **Unique global minimality, with no temporal attribution.** What is proved, and it is a real
    theorem: the zero-defect configuration exists, is the unique such configuration, and is the
    global minimum of `total_defect`. That is forced by the cost axioms and is the honest F-005
    content.

    The word "initial" is not proved anywhere and currently has the wrong sign. Each variational
    tick is DEFINED to pick the feasible minimizer
    (`VariationalDynamics.IsVariationalSuccessor`), so defect descends in the tick index by
    construction and `unity_config` is the attractor every trajectory runs toward, not the state it
    runs from. Calling the minimum "the past" therefore reverses the tree's own dynamics.

    So this does not yet answer Penrose, Albert, or Boltzmann. It answers a different and still
    substantial question: thermal equilibrium is not merely improbable but uniquely non-minimal,
    and there is exactly one zero-cost configuration.

    Gate for restoring the temporal reading, either branch sufficing: a derivation that physical
    time runs along INCREASING `total_defect`, which inverts the tick order of the variational
    update and needs its own independent justification; or a dynamics that provably departs from
    unity rather than descending to it. `Foundation.ReadingArrowSweep` gives the criterion this is
    measured against, and `Holography.ObserverHorizonOrientation` shows the direction cannot be
    borrowed from a boundary. -/
theorem past_theorem {N : ℕ} (hN : 0 < N) :
    (∃! c : Configuration N, total_defect c = 0) ∧
    total_defect (unity_config N hN) = 0 ∧
    (∀ c : Configuration N, total_defect (unity_config N hN) ≤ total_defect c) := by
  refine ⟨⟨unity_config N hN, unity_defect_zero hN, ?_⟩, unity_defect_zero hN,
    unity_is_global_minimum hN⟩
  intro c hc
  have h_entries : ∀ i, c.entries i = 1 :=
    (zero_defect_iff_unity hN c).mp hc
  have h_u_entries : ∀ i, (unity_config N hN).entries i = 1 := fun _ => rfl
  have h_eq : c.entries = (unity_config N hN).entries :=
    funext fun i => by rw [h_entries i, h_u_entries i]
  exact Configuration.mk.injEq .. |>.mpr h_eq

What this page does not claim

The theorem does not claim the minimum-entropy state is the initial state of the universe. The theorem does not prove the Past Hypothesis of Albert or the Weyl Curvature Hypothesis of Penrose. The theorem does not claim the direction of time is derived within the framework.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND