unity_unique_minimizer
The theorem shows that any configuration of N positive real ledger entries whose total defect equals that of the all-ones configuration must have every entry exactly equal to 1. Cosmologists addressing the Past Hypothesis cite it to replace an assumed low-entropy beginning with a uniqueness result forced by the cost axioms. The proof is a term-mode reduction that rewrites the defect equality to zero and applies the equivalence between zero total defect and the all-ones state.
claimLet $c$ be any configuration of $N$ positive real numbers. Let $D(c)$ be the total defect given by the sum of individual $J$-costs over the entries. Let $u_N$ be the configuration whose every entry equals 1. If $D(c) = D(u_N)$, then every entry of $c$ equals 1.
background
The module F-005 formalizes the low-entropy initial condition as a theorem rather than a hypothesis. A Configuration of size $N$ is a structure whose entries map each index in Fin $N$ to a positive real; total_defect sums the individual defect values supplied by LawOfExistence.defect on those entries. Entropy is defined directly as total_defect, so zero defect is zero entropy. Upstream lemmas establish that the all-ones configuration has total defect zero and that total defect zero holds if and only if every entry equals 1.
proof idea
The term proof first rewrites the hypothesis total_defect c = total_defect (unity configuration) by the lemma that the unity configuration has zero defect. It then applies the forward direction of the equivalence between zero total defect and the all-ones configuration to conclude that every entry equals 1.
why it matters in Recognition Science
The result completes the argument that the initial state is the unique zero-defect configuration, converting the Past Hypothesis into the Past Theorem stated in the module documentation. It rests on the cost axioms and the Recognition Composition Law that force the J-function; the uniqueness supplies the minimal-entropy starting point required by the eight-tick octave and the phi-ladder mass formula. No open scaffolding remains for this finite-N case.
scope and limits
- Does not derive the integer N from the forcing chain T0-T8.
- Does not treat continuous or infinite-dimensional configurations.
- Does not compute explicit numerical values of defect or entropy.
- Does not address dynamical evolution away from the initial state.
formal statement (Lean)
105theorem unity_unique_minimizer {N : ℕ} (hN : 0 < N) (c : Configuration N) :
106 total_defect c = total_defect (unity_config N hN) →
107 ∀ i, c.entries i = 1 := by
proof body
Term-mode proof.
108 rw [unity_defect_zero hN]
109 exact (zero_defect_iff_unity hN c).mp
110
111/-! ## Entropy and Defect -/
112
113/-- Entropy of a configuration is proportional to its total defect.
114 Zero defect = zero entropy = minimum entropy state. -/