initial_state_minimum_entropy
plain-language theorem explainer
The theorem states that the configuration of N ledger entries each equal to one has zero entropy. Cosmologists addressing the past hypothesis would cite this as the Recognition Science derivation of the forced low-entropy initial state. The proof is a one-line wrapper that invokes the zero total defect of the unity configuration.
Claim. For any positive integer $N$, let $C_N$ be the configuration of $N$ ledger entries each equal to one. Then the entropy of $C_N$, defined as its total defect, equals zero.
background
The module F-005 formalizes why the universe begins in a low-entropy state. Entropy of a configuration is defined as its total defect, so that zero defect yields the minimum entropy state of zero. The unity configuration is the zero-defect state in which every entry equals one. The upstream theorem unity_defect_zero establishes that the total defect of this configuration is zero by unfolding the defect definition and summing the zero contributions from LawOfExistence.defect_at_one.
proof idea
The proof is a one-line wrapper that applies unity_defect_zero hN.
why it matters
This declaration supplies the content for registry item F-005, converting the cosmological past hypothesis into a past theorem forced by the cost axioms. It rests on the zero-defect property of the unity configuration and the definition of entropy as total defect. No downstream theorems are recorded yet, and the result does not invoke the Recognition Composition Law or the T5-T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.