Encyclopedia Foundation Foundation Initial Condition

ARTICLE 5 claims 4 theorems 1 open

Foundation Initial Condition

Foundation initial condition is the established uniqueness and global minimality of the zero-defect configuration, without any temporal claim that it is the past.

Verify this page

The Initial Condition

Foundation initial condition is the name for what the cost axioms force about the lowest-defect state of a ledger. A ledger is the record of recognition events, and a configuration of N ledger entries is an assignment of a positive real ratio to each entry. The defect of an entry is its J-cost, the unique mismatch formula forced by the combining rule and one local scale fix. The total defect of a configuration is the sum of the individual defects.

The module establishes three facts. First, the configuration in which every entry equals 1 has total defect 0. Second, it is the only configuration with total defect 0: if the total defect vanishes, every entry must be 1. Third, it is the unique global minimum of total defect, meaning no configuration has lower total defect. These facts are machine-checked by the kernel-checked library kernel, and they follow from the cost axioms alone. Because entropy is defined as total defect, the unity configuration has minimum entropy, and any non-unity configuration has positive entropy.

The word "initial" is not earned by these facts. Minimality is a fact about the potential, not about the direction of travel along it. In the variational dynamics, each tick is defined to pick the feasible minimizer, so total defect is non-increasing in the tick index by construction. The unity configuration is therefore the attractor every trajectory runs toward, not the state it runs from. Calling the minimum "the past" would reverse the tree's own dynamics. The Past Hypothesis, the traditional cosmological claim that the universe started in a low-entropy state, remains an open question, not a theorem. The module states this gate explicitly as past_theorem, and notes that the temporal reading belongs to the empty ledger record, not to the configuration, in the TwoClocks module.

What is established is substantial: thermal equilibrium is not merely improbable but uniquely non-minimal, and there is exactly one zero-cost configuration. The question of which end of time sits at that minimum is a separate and strictly stronger claim, and it is not established here.

THEOREM unity_defect_zero · IndisputableMonolith/Foundation/InitialCondition.lean
unity_defect_zero · IndisputableMonolith/Foundation/InitialCondition.lean:79 
/-- The unity configuration has zero total defect. -/
theorem unity_defect_zero {N : ℕ} (hN : 0 < N) :
    total_defect (unity_config N hN) = 0 := by
  unfold total_defect unity_config
  simp only [LawOfExistence.defect_at_one]
  exact Finset.sum_const_zero
THEOREM zero_defect_iff_unity · IndisputableMonolith/Foundation/InitialCondition.lean
zero_defect_iff_unity · IndisputableMonolith/Foundation/InitialCondition.lean:88 
/-- **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 unity_unique_minimizer · past_theorem · IndisputableMonolith/Foundation/InitialCondition.lean
unity_unique_minimizer · IndisputableMonolith/Foundation/InitialCondition.lean:124 
/-- **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
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

What this page does not claim

Not claimed: that the universe actually started in the unity configuration. Not claimed: that the Past Hypothesis is established. Not claimed: that the minimum 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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND