nonunity_positive_entropy
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of a configuration with all entries equal to one.
- Does not compute numerical entropy values for concrete configurations.
- Does not address time evolution or entropy decrease under dynamics.
- Does not invoke the Recognition Composition Law or the full T0-T8 forcing chain.
formal statement (Lean)
123theorem nonunity_positive_entropy {N : ℕ} (_hN : 0 < N) (c : Configuration N)
124 (h : ∃ i, c.entries i ≠ 1) : 0 < entropy c := by
proof body
Tactic-mode proof.
125 obtain ⟨j, hj⟩ := h
126 have hj_pos : 0 < LawOfExistence.defect (c.entries j) :=
127 LawOfExistence.defect_pos_of_ne_one (c.entries_pos j) hj
128 calc 0 < LawOfExistence.defect (c.entries j) := hj_pos
129 _ ≤ ∑ i : Fin N, LawOfExistence.defect (c.entries i) := by
130 apply Finset.single_le_sum (f := fun i => LawOfExistence.defect (c.entries i))
131 (fun i _ => LawOfExistence.defect_nonneg (c.entries_pos i))
132 (Finset.mem_univ j)
133
134/-! ## The Past Hypothesis Becomes a Theorem -/
135
136/-- **The Past Theorem (F-005 Resolution)**:
137
138 The universe's initial condition is not a contingent fact but a
139 mathematical necessity. The unique zero-cost configuration IS the
140 low-entropy initial state. There is no other option.
141
142 This resolves:
143 - Penrose's "Why was the Big Bang so special?"
144 - Albert's "Past Hypothesis"
145 - Boltzmann's "Why didn't we start in thermal equilibrium?"
146
147 Answer: Because thermal equilibrium (maximum defect) is infinitely
148 costly, while the zero-defect state is the unique cost minimum. -/