unity_is_global_minimum
plain-language theorem explainer
The declaration shows that for any N greater than zero and any configuration of N positive real ledger entries, the all-ones unity configuration has total defect no larger than that of the given configuration. Foundational physicists addressing the Past Hypothesis would cite it to derive the low-entropy initial state directly from cost axioms. The proof is a one-line wrapper that substitutes the zero-defect property of unity_config and invokes non-negativity of the total defect sum.
Claim. For any natural number $N > 0$ and any configuration $c$ of $N$ positive real entries, the total defect of the unity configuration (all entries equal to 1) satisfies $D(u) ≤ D(c)$, where $D$ denotes the sum of individual defect costs.
background
The module F-005 formalizes the initial low-entropy condition as a mathematical necessity rather than a contingent choice. A Configuration is a structure whose entries field maps each index in Fin N to a positive real ratio; total_defect sums the individual defect values drawn from LawOfExistence over those entries. The upstream theorem total_defect_nonneg establishes that this sum is always at least zero because each defect term is nonnegative. unity_config constructs the special case with every entry equal to 1, and unity_defect_zero shows that this case yields exactly zero total defect.
proof idea
The term proof first rewrites the left-hand side via unity_defect_zero to replace it by zero, then applies total_defect_nonneg to the arbitrary configuration c to obtain the required inequality.
why it matters
This result is invoked directly by past_theorem to complete the Past Theorem resolution of F-005, establishing that the zero-defect state is both minimal and unique, thereby answering Penrose's question on the special initial condition of the Big Bang. It is also used in no_singularity to ground the claim that the early universe begins with zero total defect and therefore lacks a singularity. Within the Recognition framework the theorem closes the step from the cost axioms and J-function properties to the forced low-entropy starting point, consistent with the eight-tick octave and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.