pith. machine review for the scientific record. sign in
def definition def or abbrev high

total_defect

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  45noncomputable def total_defect {N : ℕ} (c : Configuration N) : ℝ :=

proof body

Definition body.

  46  ∑ i : Fin N, LawOfExistence.defect (c.entries i)
  47
  48/-- Total defect is non-negative (each term is non-negative). -/

used by (29)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.