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

total_defect

show as:
view Lean formalization →

Total defect sums the J-cost of each ledger entry in a configuration of N positive real ratios. Cosmologists and foundational physicists cite it when deriving the Past Theorem from the cost axioms. The definition is the direct finite sum of the defect functional over the Fin N entries.

claimLet $c$ be a configuration of $N$ ledger entries with positive real values $c_i$. The total defect is $D(c) = N^{-1} sum_{i=1}^N J(c_i)$, where $J(x) = (x + x^{-1})/2 - 1$ is the defect functional.

background

Configuration is the structure of N ledger entries, each a positive real ratio. The defect functional equals J for positive arguments, with J the J-cost from the Recognition Composition Law. In the Initial Condition module the total defect measures cumulative deviation from the unique zero-cost state x=1, formalizing the low-entropy initial condition as the only RSExists state.

proof idea

The definition is the direct summation over Fin N of defect applied to each configuration entry. It uses the defect definition from LawOfExistence and the entries field of Configuration.

why it matters in Recognition Science

This definition underpins the entropy function and the Past Theorem, which asserts that the initial state is the unique zero-defect configuration. It is invoked by initial_state_is_zero_defect and no_singularity to resolve the Past Hypothesis as a mathematical necessity forced by the cost axioms. It sits inside the F-005 registry item and supports the eight-tick octave and D=3 landmarks by anchoring the minimum-cost ledger state.

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.