total_defect
plain-language theorem explainer
The total defect of a configuration sums the J-costs of its N ledger entries. Cosmologists deriving the Past Theorem and the no-singularity result cite this definition when quantifying the initial low-entropy state. It is introduced as a direct finite sum of the individual defect terms.
Claim. Let $c$ be a configuration of $N$ positive real ratios $c_1, c_2, ..., c_N$. The total defect is defined by $D(c) = sum_{i=1}^N J(c_i)$, where $J$ is the defect functional with $J(1)=0$.
background
A configuration consists of a finite collection of positive real ratios, each representing a ledger entry. The defect of an individual entry equals the J-functional, which is zero precisely when the ratio equals unity. This module (F-005) treats the low-entropy initial condition as a forced consequence of the cost axioms rather than an additional hypothesis.
proof idea
The definition is a direct summation over the finite index set of entries, applying the defect functional to each component.
why it matters
This supplies the cost functional used by the Past Theorem, which states that the initial state is the unique zero-defect configuration and therefore the global minimum-entropy state. It feeds the no-singularity theorem and the entropy definition in the same module, closing the argument that the Big Bang initial condition is the null ledger forced by J-uniqueness and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.