pith. sign in
module module high

IndisputableMonolith.Foundation.InitialCondition

show as:
view Lean formalization →

The InitialCondition module defines Configuration as a finite tuple of positive real ratios that serve as ledger entries. Cosmologists deriving early-universe conditions and foundational researchers building variational dynamics cite this object when initializing the Recognition ledger from the Law of Existence. The module contains only type and constant definitions with no theorems.

claimA configuration is an $N$-tuple $C = (r_1, r_2, ..., r_N)$ where each $r_i > 0$ is a ledger-entry ratio.

background

This module belongs to the Foundation layer and imports the J-cost structure, the Law of Existence (x exists iff defect(x) = 0), and the ontology predicates that reduce existence and truth to cost-minimization outcomes under the unique J function. It supplies the basic ledger object used by all downstream foundation modules. The supplied doc-comment states that a configuration consists of N ledger entries, each a positive real ratio.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the initial ledger object required by EarlyUniverse (EU-001 on t=0 conditions and dark sector), StillnessGenerative (ground-state instability from zero defect), TopologicalConservation, VariationalDynamics, and WindingCharges. It closes the gap between the abstract Law of Existence and concrete starting states for the forcing chain.

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)