Pith. sign in
module module moderate

IndisputableMonolith.Foundation.LawOfExistence

show as:
view Lean formalization →

Equates ledger existence with vanishing J-cost defect, uniquely at the unit configuration x = 1. Foundation modules on determinism, continuum limits, constants, and early-universe cosmology import it as the cost-to-existence bridge. Argument is elementary real analysis on the canonical cost: nonnegativity, unique zero at unity, and the existence–defect biconditional.

claimWith the canonical cost $J(x)=\frac{1}{2}(x+x^{-1})-1$ and its defect, a configuration exists if and only if its defect is zero; defect vanishes if and only if $x=1$ (unity), so existence is equivalent to unity and the zero-defect existent is unique.

background

Recognition Science builds physics from a single cost functional on positive reals. The module imports that cost layer and treats $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$) as the canonical ledger cost: nonnegative, strictly convex on $(0,\infty)$, and minimized uniquely at $x=1$ where $J(1)=0$.

Defect measures departure from that minimum. The local setting is the Foundation domain: before dimensional forcing, continuum limits, or constant derivations, one needs a precise meaning of "what exists" on the ledger. Sibling definitions package $J$, defect, nonnegativity, the collapse of defect to the unit point, and an Exists predicate tied to zero defect.

Upstream is the shared Cost module; downstream Foundation and Cosmology files consume the existence–unity equivalence as a primitive.

proof idea

Definition-heavy module with short analytic lemmas, not a single deep proof. It introduces $J$ and defect, records $J(1)=0$ and defect nonnegativity, then proves defect vanishes iff the argument is $1$. Existence is defined (or characterized) by zero defect; the two directions give the biconditional law of existence. Corollaries restate existence iff unity and uniqueness of the zero-defect existent. No heavy tactics: algebraic identities for $J$ and standard order facts on $\mathbb{R}_{>0}$.

why it matters in Recognition Science

Supplies the existence–defect–unity link that later Foundation results treat as given. Determinism uses strict convexity of $J$ and unique minimizers for ledger updates. ContinuumLimit lifts discrete $J$-cost dynamics on $\mathbb{Z}^3$ to a Klein-Gordon-like diffusion. ConstantDerivations derives $c$, $\hbar$, $G$, and $\alpha$ from the same cost geometry. BiconditionalSelfNegation cites the unique zero-defect existent at $x=1$ when ruling out real configurations satisfying $P\leftrightarrow\neg P$ on defect. EarlyUniverse imports the package for $t=0$ and dark-sector registry items. In the forcing chain this sits with T5 $J$-uniqueness: once $J$ is fixed, existence collapses to unity and the rest of the octave and dimension arguments have a clean ontic base.

scope and limits

used by (22)

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)