initial_state_minimum_entropy
plain-language theorem explainer
The theorem establishes that the zero-defect configuration of any positive number of ledger entries carries zero entropy. Cosmologists resolving the low-entropy initial state would cite this to derive the Past Theorem directly from the cost axioms. The proof is a direct term application of the zero total defect property of the unity configuration.
Claim. For any positive integer $N$, the entropy of the configuration with all $N$ entries equal to 1 equals zero.
background
In this module the entropy of a configuration is defined as its total defect, so that zero defect yields the minimum entropy state. The unity configuration is the arrangement in which every ledger entry equals 1. The local setting is F-005, which replaces the Past Hypothesis with a theorem forced by the cost axioms: the only RSExists state is the zero-defect point, and a collection of N such states has total defect zero.
proof idea
The proof is a one-line term that applies the upstream theorem establishing zero total defect for the unity configuration.
why it matters
This declaration completes the core step of F-005 by showing that the initial state is the unique zero-cost configuration. It converts the low-entropy beginning from an assumption into a consequence of the recognition cost function. No downstream theorems are yet recorded, leaving the result as a foundational lemma for later dynamical arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.