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

entropy

show as:
view Lean formalization →

The declaration defines entropy of a configuration of N ledger entries as its total defect sum. Cosmologists working on the initial low-entropy state in Recognition Science cite this to identify zero defect with the minimum-entropy configuration. The definition is a one-line wrapper around the total_defect summation.

claimFor a configuration $c$ of $N$ positive real ledger entries, the entropy is defined by $S(c) :=$ sum of the individual J-costs of each entry.

background

In the InitialCondition module a Configuration is a structure of $N$ positive real entries representing ledger ratios. Total defect sums the J-cost of each entry via LawOfExistence.defect. The module formalizes F-005: the only RSExists state is unity (zero defect), so a full ledger of unity entries has total defect zero and is therefore the unique minimum-entropy state, converting the Past Hypothesis into the Past Theorem.

proof idea

One-line wrapper that applies the total_defect definition, which itself sums LawOfExistence.defect over the Fin N entries.

why it matters in Recognition Science

This definition supplies the entropy measure used by initial_state_minimum_entropy, nonunity_positive_entropy, cone_entropy_bound, and jcost_ground_state. It realizes the low-entropy initial condition forced by the cost axioms in the T0-T8 chain, making the Past Hypothesis a theorem rather than an assumption.

scope and limits

formal statement (Lean)

 115noncomputable def entropy {N : ℕ} (c : Configuration N) : ℝ :=

proof body

Definition body.

 116  total_defect c
 117
 118/-- **Theorem**: The initial state has minimum entropy. -/

used by (40)

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

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.