pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.InitialCondition

show as:
view Lean formalization →

The module defines an initial ledger configuration as N positive real ratios. Early-universe modelers and variational dynamicists cite it to anchor derivations in the zero-defect ground state. Supporting lemmas establish that total defect is nonnegative, vanishes only at the unity configuration, and that entropy reaches its global minimum there.

claimLet $C = (r_1, r_2, ..., r_N)$ with each $r_i > 0$ a ledger ratio. The total defect is $D(C) = sum J(r_i)$ where $J(x) = (x + x^{-1})/2 - 1$. The unity configuration satisfies $r_i = 1$ for all $i$, yielding $D(C) = 0$ and minimum entropy.

background

Recognition Science models physical states as ledger entries whose ratios are positive reals. This module defines the initial condition as a finite configuration of such entries. It builds directly on the Law of Existence, which states that x exists if and only if defect(x) = 0, and on OntologyPredicates that operationalize existence via cost minimization under the J-function.

proof idea

This is a definition module, no proofs. It introduces Configuration and proves auxiliary facts such as total_defect_nonneg, unity_defect_zero, and initial_state_minimum_entropy using the imported LawOfExistence and Cost primitives.

why it matters in Recognition Science

Downstream modules in Cosmology.EarlyUniverse rely on this initial condition to derive Big Bang conditions and dark sector properties. StillnessGenerative uses it to show that the zero-defect state is the source of all structure. It fills the foundational slot between the abstract Law of Existence and concrete variational dynamics or topological conservation arguments.

scope and limits

used by (5)

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)