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

Configuration

show as:
view Lean formalization →

A Configuration of N ledger entries is a structure consisting of a function from Fin N to positive reals that represents ratios in the recognition ledger. Cosmologists and foundational physicists cite it when establishing that the zero-defect state is the unique minimum-entropy initial condition. The definition is a direct structure declaration that encodes the positivity requirement as an explicit field predicate.

claimLet $N$ be a natural number. A configuration of $N$ ledger entries consists of a function $e : [N] → ℝ$ together with a proof that $e(i) > 0$ for every index $i$.

background

The module F-005 formalizes the low-entropy initial state by showing that the only zero-cost ledger state is the unity configuration where every entry equals 1. The defect functional, imported from LawOfExistence, equals the J-cost J(x) for positive x and vanishes exactly at unity. Upstream LedgerFactorization supplies the underlying multiplicative group structure on positive reals, while PhiForcingDerived and RecognitionForcing supply the J-cost definition and the uniqueness of recognition extraction.

proof idea

Direct structure definition with a single positivity field predicate; no tactics or lemmas are applied.

why it matters in Recognition Science

This structure is the central object of the Past Theorem in the same module, which proves that the unity configuration is the unique zero-total-defect state and therefore the minimum-entropy initial condition. It is used to derive the entropy definition, the non-unity positive entropy theorem, and the no-singularity result in EarlyUniverse. The construction closes the F-005 registry item by converting the Past Hypothesis into a theorem forced by the cost axioms and the uniqueness of the x=1 fixed point.

scope and limits

formal statement (Lean)

  40structure Configuration (N : ℕ) where
  41  entries : Fin N → ℝ
  42  entries_pos : ∀ i, 0 < entries i
  43
  44/-- Total defect of a configuration: sum of individual J-costs. -/

used by (40)

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

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.