nonunity_positive_entropy
plain-language theorem explainer
Any configuration of N positive real ledger entries that is not uniformly equal to one has strictly positive entropy. Cosmologists addressing the low-entropy initial state of the universe cite this result to convert the Past Hypothesis into a theorem. The proof extracts a single witness entry whose defect is positive and shows it is bounded above by the total sum of defects.
Claim. Let $N$ be a positive integer and let $c$ be a configuration of $N$ positive real numbers. If at least one entry of $c$ is not equal to 1, then the entropy of $c$, defined as the sum of the defects of its entries, satisfies $0 <$ entropy$(c)$.
background
A Configuration of $N$ ledger entries is a structure that assigns a positive real ratio to each of $N$ positions. Entropy of such a configuration is defined as its total defect, the sum of the individual defect values. The defect functional equals $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$, which vanishes only at unity and is nonnegative elsewhere. This module formalizes the claim that the universe begins in the unique zero-cost state, turning the Past Hypothesis into a theorem.
proof idea
The tactic proof obtains a witness index $j$ where the entry differs from 1. It applies the upstream lemma defect_pos_of_ne_one to produce a strictly positive defect at that position. It then uses single_le_sum over the full Finset of indices, invoking defect_nonneg on every term, to conclude that the single positive defect is at most the total sum, which equals the entropy.
why it matters
This result supplies the positive-entropy half of the argument that the initial condition must be the minimum-entropy state. It is referenced in the module's commentary on the Past Theorem (F-005), which resolves Penrose's Weyl curvature hypothesis and Albert's Past Hypothesis by showing that thermal equilibrium carries infinite cost. In the Recognition Science framework it closes the step from zero-defect uniqueness to the forced low-entropy beginning, consistent with the eight-tick octave and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.