Foundation Initial Condition

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 Lean 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

THEOREM zero_defect_iff_unity · IndisputableMonolith/Foundation/InitialCondition.lean

THEOREM unity_unique_minimizer · past_theorem · IndisputableMonolith/Foundation/InitialCondition.lean

THEOREM initial_state_minimum_entropy · IndisputableMonolith/Foundation/InitialCondition.lean

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: