total_defect_nonneg
plain-language theorem explainer
The theorem shows that the total defect of any finite configuration of positive real ledger entries is non-negative. Foundational physicists addressing the Past Hypothesis would cite it to establish that zero defect is the absolute lower bound on entropy. The proof is a direct one-line application of the finite-sum non-negativity lemma together with the per-entry non-negativity of the defect functional.
Claim. Let $N$ be a natural number and let $c$ be any configuration of $N$ positive real ledger entries. Then the total defect satisfies $0 ≤ ∑_{i=0}^{N-1} J(c_i)$, where $J$ denotes the defect functional.
background
The InitialCondition module formalizes the low-entropy initial state required by Recognition Science. A Configuration is a structure holding an array of $N$ positive reals (the ledger entries) together with the proof that each entry is positive. Total defect is defined as the sum of the individual defect values, where defect coincides with the J-cost functional on positive reals. The module converts the classical Past Hypothesis into a theorem by showing that the only zero-cost state is the all-unity configuration.
proof idea
The proof applies the Finset.sum_nonneg lemma to the defining sum of total_defect. For each index it invokes the upstream defect_nonneg result from LawOfExistence, using the entries_pos field of the configuration to supply the required positivity hypothesis.
why it matters
This non-negativity result is invoked by unity_is_global_minimum to prove that the unity configuration is the global minimizer, and by multiple theorems in VariationalDynamics (equilibrium_attractive, unity_is_equilibrium, variational_dynamics_certificate) to guarantee that defect is bounded below along any trajectory. It thereby supplies the lower bound required by the forcing chain (T0–T8) and the Recognition Composition Law, closing the argument that the initial condition is uniquely forced to zero defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.