pith. sign in
module module high

IndisputableMonolith.Foundation.InitialCondition

show as:
view Lean formalization →

The InitialCondition module defines a configuration as a finite tuple of positive real ratios serving as ledger entries. It establishes the unity configuration (all entries equal to 1) as the unique state with zero total defect and minimum entropy, consistent with the Law of Existence. Cosmologists and foundational RS researchers cite it for t=0 conditions and ground-state derivations. The module consists of successive definitions followed by direct verification lemmas on defect and entropy.

claimA configuration is a tuple $(x_1,…,x_N)$ with each $x_i>0$. The total defect is the sum of individual defects, vanishing if and only if the tuple is the unity configuration with all $x_i=1$. The initial state is this unity configuration, which also minimizes the associated entropy functional.

background

The module sits inside the Recognition Science foundation and imports the J-cost from the Cost module together with the Law of Existence (x exists iff defect(x)=0) and the OntologyPredicates that tie existence to cost minimization under the unique J function. It introduces Configuration as a finite sequence of positive real ledger-entry ratios, total_defect as their summed defect, unity_config as the all-ones tuple, and entropy as a non-negative measure that is zero precisely on the unity tuple.

proof idea

This is a definition module, no proofs. It defines Configuration, total_defect, unity_config, entropy and initial_state, then states the lemmas total_defect_nonneg, unity_defect_zero, zero_defect_iff_unity, unity_is_global_minimum, unity_unique_minimizer, initial_state_minimum_entropy and nonunity_positive_entropy.

why it matters in Recognition Science

The module supplies the initial ledger state required by EarlyUniverse (EU-001 on t=0), StillnessGenerative (ground-state instability from T0–T8), VariationalDynamics (ledger update rule), TopologicalConservation and WindingCharges (topological conservation in D=3). It closes the gap between the Law of Existence and the first concrete state from which all structure is generated by cost minimization.

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)