Pith. sign in
module module moderate

IndisputableMonolith.Foundation.InitialCondition

show as:
view Lean formalization →

Ledger configurations are N-tuples of positive real ratios; total defect is the sum of J-costs and is nonnegative. Unity (all ones) is the unique zero-defect state and unique global minimizer. Entropy is minimized exactly there, so the initial state is the unique minimum-entropy past. Cosmology and foundation modules import this as the t=0 boundary condition.

claimA configuration is $c:\{1,\ldots,N\}\to\mathbb{R}_{>0}$. Total defect is $\sum_i J(c_i)$ for the Recognition cost $J$. The unity configuration $c_i\equiv 1$ has defect zero, and defect vanishes if and only if $c$ is unity; hence unity is the unique global minimizer. Entropy is minimized precisely at this initial state (the past theorem).

background

Recognition Science treats existence operationally: by the Law of Existence, $x$ exists if and only if its defect is zero. Ontology predicates cast existence and truth as selection outcomes under cost minimization for the unique $J$ (from the Cost module: $J(x)=(x+x^{-1})/2-1$).

This module lifts single-entry defect to a finite ledger. A configuration is an $N$-tuple of positive real ratios (ledger entries). Total defect sums the per-entry $J$-costs. Unity is the constant-one configuration. Entropy is built from the same cost structure so that thermodynamic and cosmological initial-value statements can cite a single mathematical object.

The local setting is pure foundation: no continuum limit, no dynamics, only the static variational characterization of the zero-cost past.

proof idea

Definitions introduce Configuration, total defect, unity, and entropy. Nonnegativity of total defect follows from nonnegativity of $J$ on $\mathbb{R}_{>0}$. Unity has defect zero by $J(1)=0$. The converse (zero defect implies unity) uses that $J$ vanishes only at $1$, entrywise. Global minimality and uniqueness of the minimizer are then immediate from nonnegativity plus the zero-defect characterization. Entropy inequalities (initial state minimum; non-unity positive entropy) are the same comparison restated in entropy language. The past theorem packages the unique minimum-entropy initial state.

why it matters in Recognition Science

EarlyUniverse imports this for EU-001 (what happened at $t=0$): the Big Bang boundary is the unique zero-defect, minimum-entropy unity configuration, feeding dark-sector and cosmological-constant claims. Thermodynamics (F-011) needs the same minimum as the zero-temperature / zero-entropy reference. VariationalDynamics (F-008) and ContinuumLimit (F-014) take unity as the rest state before discrete updates and long-wavelength limits. MeasurementMechanism, TopologicalConservation, and WindingCharges inherit a well-defined initial ledger against which defects, charges, and projections are measured. In the forcing chain this is the static past dual of T5 $J$-uniqueness: once $J$ is fixed, the unique cost-zero past is forced.

scope and limits

used by (7)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (12)