pith. sign in
module module high

IndisputableMonolith.Foundation.LawOfExistence

show as:
view Lean formalization →

The LawOfExistence module defines the canonical cost functional J and the Law of Existence in the Recognition Science foundation. It introduces J(x) = ½(x + x⁻¹) - 1 together with defect measures and equivalences linking existence to unity. Researchers deriving constants or cosmological models cite it as the entry point for cost-based arguments. The module consists of definitions and short equivalences with no complex proofs.

claimThe cost functional is $J(x) = ½(x + x^{-1}) - 1$. The Law of Existence asserts that a state exists if and only if its defect vanishes, written exists_iff_unity, with unity_unique_existent establishing uniqueness of the existent state.

background

This module occupies the base of the Foundation layer and imports only the Cost module. It defines J as the recognition cost of a positive real x, with defect quantifying deviation from the fixed point at unity. Sibling declarations include defect_at_one, defect_nonneg, and the collapse statements that tie zero defect to existence. The local setting is the cost landscape whose unique minimum at x = 1 forces subsequent structure.

proof idea

This is a definition module, no proofs. It declares J, the defect function, and the chain of equivalences exists_implies_defect_zero, defect_zero_implies_exists, and exists_iff_unity, together with the uniqueness statement unity_unique_existent.

why it matters in Recognition Science

The module supplies the cost-theoretic starting point for the entire framework. It is imported by ConstantDerivations to derive c, ħ, G and α, by Determinism to obtain uniqueness of minimizers, by DiscretenessForcing to establish the convex bowl, and by EarlyUniverse for the t = 0 conditions. It corresponds to the initial step of the T0–T8 forcing chain where J-uniqueness is first stated.

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)