unity_is_global_minimum
Unity configuration minimizes total defect over all configurations of N positive real ledger entries. Cosmologists resolving the initial entropy puzzle cite this to derive the forced low-entropy start. The term proof rewrites unity defect to zero and invokes non-negativity of total defect.
claimLet $N > 0$ be a natural number and let $c$ be any configuration of $N$ positive real ratios. Then the total defect of the unity configuration (all entries equal to 1) satisfies $0 = J(1) + J(1) + ... + J(1) ≤ J(c_1) + J(c_2) + ... + J(c_N)$, where $J$ is the defect function.
background
In Foundation.InitialCondition a Configuration of $N$ ledger entries is a structure holding $N$ positive real ratios, each an entry in the recognition ledger. The total_defect function sums the individual $J$-costs of those entries, with $J$ the defect function supplied by LawOfExistence. The unity_config is the explicit all-ones configuration, shown by unity_defect_zero to carry total defect exactly zero. The upstream total_defect_nonneg theorem establishes that every such sum is nonnegative because each $J$-term is nonnegative.
proof idea
Term-mode one-line wrapper. It rewrites the left side via unity_defect_zero to obtain zero, then applies total_defect_nonneg directly to the arbitrary configuration $c$.
why it matters in Recognition Science
The result supplies the inequality half of past_theorem, which asserts that the unity configuration is the unique zero-defect state and therefore the forced low-entropy initial condition (F-005). It is also invoked inside no_singularity to conclude that the initial ledger carries zero total defect, removing any singularity. Within the Recognition Science chain this closes the argument that the initial state is dictated by the cost axioms rather than chosen, converting the Past Hypothesis into the Past Theorem.
scope and limits
- Does not compute explicit defect values for non-unity configurations.
- Does not address subsequent recognition dynamics or time evolution.
- Does not prove uniqueness of the minimizer (handled in unity_unique_minimizer).
- Does not fix a specific value of $N$ or introduce physical units.
Lean usage
theorem downstream_use {N : ℕ} (hN : 0 < N) (c : Configuration N) : total_defect (unity_config N hN) ≤ total_defect c := unity_is_global_minimum hN cformal statement (Lean)
99theorem unity_is_global_minimum {N : ℕ} (hN : 0 < N) (c : Configuration N) :
100 total_defect (unity_config N hN) ≤ total_defect c := by
proof body
Term-mode proof.
101 rw [unity_defect_zero hN]
102 exact total_defect_nonneg c
103
104/-- **Theorem**: The unity configuration is the UNIQUE global minimizer. -/