Pith. sign in
module module moderate

IndisputableMonolith.Gravity.CoherenceCollapse

show as:
view Lean formalization →

Gravity-sector module for coherence collapse: it packages the J-cost, recognition and rate actions, Born weights, and the coherence mass and lifetime scales. Gravity and measurement workers in RS cite these defs when linking collapse rates to the phi-ladder. The file is mostly definitions plus elementary positivity and normalization lemmas.

claimDefines the cost $J(x)=\frac{1}{2}(x+x^{-1})-1$, the rate and recognition actions built from $J$, the identity relating coherence cost to twice the action, Born weights $w=\sin^2$ with positivity and normalization, and the coherence mass and lifetime scales $m_{\mathrm{coh}}$ (kg) and $\tau_{\mathrm{coh}}$ (s).

background

Recognition Science measures mismatch with the symmetric cost $J(x)=\frac12(x+x^{-1})-1$, fixed uniquely in the forcing chain (T5) and obeying the Recognition Composition Law. In the gravity domain this cost is the seed for collapse and coherence bookkeeping rather than a free phenomenological potential.

The module sits on Constants (RS-native tick $\tau_0=1$) and Mathlib. Sibling definitions introduce nonnegativity of $J$, a rate action and its positivity, a recognition action, the relation that the coherence cost equals twice the action, Born weights with positivity, the $\sin^2$ identification, normalization, and dimensionful coherence mass and lifetime in SI units.

Local setting: coherence collapse as a gravity-side recognition process, with Born-type weights and explicit $m_{\mathrm{coh}}$, $\tau_{\mathrm{coh}}$ scales for later dynamical use.

proof idea

Definition module, not a single theorem. Core objects are defs: $J$, rate and recognition actions, Born weight, and the coherence mass/time constants. Supporting lemmas are elementary: nonnegativity of $J$ and of the rate action, positivity of Born weights, the trigonometric identity that the weight is $\sin^2$, Born normalization, and the algebraic identity that coherence cost equals twice the action. No deep tactic scripts; proofs are direct unfoldings and standard real-analysis facts.

why it matters in Recognition Science

Gives the gravity stack a single place for collapse cost, action, and Born weight so later gravity theorems can quote one vocabulary. The $J$-cost is the T5 landmark; packaging it with recognition action and $C=2A$ ties collapse bookkeeping to the same functional that forces $\phi$ and the eight-tick structure elsewhere. Born weight and normalization connect the collapse side to measurement-style probabilities. Dimensionful $m_{\mathrm{coh}}$ and $\tau_{\mathrm{coh}}$ supply SI anchors for phenomenological gravity or tabletop coherence estimates. No downstream edges are recorded yet; the module is an upstream definitions hub for the Gravity domain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (17)