Encyclopedia Foundation Foundation Initial Condition Initial State Minimum Entropy
ARTICLE 3 claims 3 theorems
Foundation Initial Condition Initial State Minimum Entropy
A machine-checked proof shows the lowest-entropy configuration of a ledger is the one where every entry is at its neutral value, but it does not show that this state was the universe's past.
The minimum entropy state
The declaration initial_state_minimum_entropy establishes a precise mathematical fact about a model of a ledger, a discrete record of events. In this framework, a configuration is a collection of positive real numbers, one for each of N ledger entries. Each entry has a cost, called its defect, which measures how far it is from the neutral value 1. The total defect of a configuration is the sum of these individual costs. The theorem proves that the configuration where every entry equals 1 has a total defect of zero, and that this is the unique global minimum of total defect. Because entropy is defined as proportional to total defect, this configuration is the unique state of minimum entropy.
The proof is not just a statement of minimality; it also establishes uniqueness. The theorem zero_defect_iff_unity shows that a configuration has zero total defect if and only if every entry is exactly 1. This means there is exactly one state with zero entropy, and every other configuration has strictly positive entropy. The framework's library of formal theorems proves this from its cost axioms, which are the same axioms that force the form of the cost function itself. The result is that the minimum entropy state is not a choice or an accident; it is forced by the structure of the cost.
In Recognition Science, this result is often discussed in the context of the Past Hypothesis, the idea that the universe began in a state of low entropy. The theorem proves that the zero-defect configuration is the unique minimum, but it does not prove that this configuration was the initial state of the universe. The word "initial" is not earned by the mathematics. The framework's own dynamics, which defines each tick as picking the feasible minimizer, makes total defect non-increasing over time. This means the minimum entropy state is the attractor that every trajectory runs toward, not the state it runs from. The theorem is about the potential, not about the direction of travel along it.
What the declaration does establish is substantial: thermal equilibrium, in this model, is not merely improbable but uniquely non-minimal, and there is exactly one zero-cost configuration. The question of whether this minimum was the origin of time remains open. The framework explicitly gates this temporal reading behind a separate derivation that physical time runs along increasing total defect, or a dynamics that provably departs from unity. Until then, the theorem answers a question about the structure of the cost function, not about the history of the universe.
THEOREM unity_is_global_minimum · unity_unique_minimizer · past_theorem · IndisputableMonolith/Foundation/InitialCondition.lean
/-- **Theorem**: The unity configuration achieves the global minimum of total defect. -/
theorem unity_is_global_minimum {N : ℕ} (hN : 0 < N) (c : Configuration N) :
total_defect (unity_config N hN) ≤ total_defect c := by
rw [unity_defect_zero hN]
exact total_defect_nonneg c
/-- **Theorem**: The unity configuration is the UNIQUE global minimizer. -/
theorem unity_unique_minimizer {N : ℕ} (hN : 0 < N) (c : Configuration N) :
total_defect c = total_defect (unity_config N hN) →
∀ i, c.entries i = 1 := by
rw [unity_defect_zero hN]
exact (zero_defect_iff_unity hN c).mp
/-- **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 zero_defect_iff_unity · IndisputableMonolith/Foundation/InitialCondition.lean
/-- **Theorem (F-005 core)**: The unity configuration is the unique
zero-total-defect configuration.
Every entry must be 1 for total defect to vanish. -/
theorem zero_defect_iff_unity {N : ℕ} (_hN : 0 < N) (c : Configuration N) :
total_defect c = 0 ↔ ∀ i, c.entries i = 1 := by
constructor
· intro h_zero
have h_terms : ∀ i, LawOfExistence.defect (c.entries i) = 0 := by
by_contra h_not
push_neg at h_not
obtain ⟨j, hj⟩ := h_not
have hj_pos : 0 < LawOfExistence.defect (c.entries j) := by
have h_nn := LawOfExistence.defect_nonneg (c.entries_pos j)
exact lt_of_le_of_ne h_nn (Ne.symm hj)
have h_sum_pos : 0 < total_defect c := by
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)
linarith
intro i
exact (LawOfExistence.defect_zero_iff_one (c.entries_pos i)).mp (h_terms i)
· intro h_all_one
simp only [total_defect]
apply Finset.sum_eq_zero
intro i _
rw [h_all_one i]
exact LawOfExistence.defect_one
THEOREM past_theorem · IndisputableMonolith/Foundation/InitialCondition.lean
/-- **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 that the minimum entropy state was the initial state of the universe. The theorem does not claim that the Past Hypothesis is proved. The theorem does not claim that the unity configuration is the origin of time.
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:
- What independent justification could show that physical time runs along increasing total defect?
- What dynamics would provably depart from unity rather than descend to it?
- How does the empty ledger record, as opposed to the unity configuration, satisfy the requirements for being an origin of time?
- What does the ReadingArrowSweep criterion measure this temporal reading against?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM unity_is_global_minimum · unity_unique_minimizer · past_theorem · IndisputableMonolith/Foundation/InitialCondition.lean
/-- **Theorem**: The unity configuration achieves the global minimum of total defect. -/ theorem unity_is_global_minimum {N : ℕ} (hN : 0 < N) (c : Configuration N) : total_defect (unity_config N hN) ≤ total_defect c := by rw [unity_defect_zero hN] exact total_defect_nonneg c/-- **Theorem**: The unity configuration is the UNIQUE global minimizer. -/ theorem unity_unique_minimizer {N : ℕ} (hN : 0 < N) (c : Configuration N) : total_defect c = total_defect (unity_config N hN) → ∀ i, c.entries i = 1 := by rw [unity_defect_zero hN] exact (zero_defect_iff_unity hN c).mp/-- **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_eqThe theorem proves that the configuration where every entry equals 1 has a total defect of zero, and that this is the unique global minimum of total defect. unity_is_global_minimum · unity_unique_minimizer · past_theorem · IndisputableMonolith/Foundation/InitialCondition.leanTHEOREM zero_defect_iff_unity · IndisputableMonolith/Foundation/InitialCondition.lean
/-- **Theorem (F-005 core)**: The unity configuration is the unique zero-total-defect configuration. Every entry must be 1 for total defect to vanish. -/ theorem zero_defect_iff_unity {N : ℕ} (_hN : 0 < N) (c : Configuration N) : total_defect c = 0 ↔ ∀ i, c.entries i = 1 := by constructor · intro h_zero have h_terms : ∀ i, LawOfExistence.defect (c.entries i) = 0 := by by_contra h_not push_neg at h_not obtain ⟨j, hj⟩ := h_not have hj_pos : 0 < LawOfExistence.defect (c.entries j) := by have h_nn := LawOfExistence.defect_nonneg (c.entries_pos j) exact lt_of_le_of_ne h_nn (Ne.symm hj) have h_sum_pos : 0 < total_defect c := by 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) linarith intro i exact (LawOfExistence.defect_zero_iff_one (c.entries_pos i)).mp (h_terms i) · intro h_all_one simp only [total_defect] apply Finset.sum_eq_zero intro i _ rw [h_all_one i] exact LawOfExistence.defect_oneThe theorem zero_defect_iff_unity shows that a configuration has zero total defect if and only if every entry is exactly 1. zero_defect_iff_unity · IndisputableMonolith/Foundation/InitialCondition.leanTHEOREM past_theorem · IndisputableMonolith/Foundation/InitialCondition.lean
/-- **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_eqThe framework's own dynamics, which defines each tick as picking the feasible minimizer, makes total defect non-increasing over time. past_theorem · IndisputableMonolith/Foundation/InitialCondition.lean