pith. sign in
module module high

IndisputableMonolith.Foundation.LawOfExistence

show as:
view Lean formalization →

The LawOfExistence module defines the canonical cost functional J and states the Law of Existence via defect collapse and unity equivalences. Researchers deriving constants or early-universe conditions cite it as the cost-theoretic base layer. The module supplies definitions and direct equivalences imported from Cost, with no complex proof structure.

claim$J(x) = \frac12(x + x^{-1}) - 1$, with defect measuring deviation from unity and the Law of Existence given by the equivalences $\mathrm{Exists}(x) \iff \mathrm{defect}(x) = 0$ and unity as the unique existent.

background

The module imports the Cost module and centers on the J-cost functional whose doc-comment states it is the canonical form $J(x) = \frac12(x + x^{-1}) - 1$. It introduces defect as the non-negative deviation measure, the Exists predicate for recognized existence, and basic lemmas such as defect_nonneg together with the equivalences exists_iff_unity and unity_unique_existent. The local setting is the Recognition Science foundation in which all subsequent structure (constants, determinism, discreteness) is built from minimization of this cost.

proof idea

This is a definition module, no proofs. It states J directly from the Cost import, defines defect and Exists as auxiliary objects, and records the Law of Existence through the listed equivalences and collapse lemmas.

why it matters in Recognition Science

This module supplies the core cost definitions that feed ConstantDerivations (for deriving c, ħ, G, α), Determinism (unique minimizer from strict convexity), DiscretenessForcing (convex bowl at unity), DimensionalConstraints.CostLayer, and Cosmology.EarlyUniverse (EU-001/D-002/D-003). It occupies the initial position in the RS chain before the forcing steps T5–T8 and the Recognition Composition Law.

scope and limits

used by (24)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (21)