Pith. sign in
module module moderate

IndisputableMonolith.Gravity.CoherenceCollapse

show as:
view Lean formalization →

Module packaging the J-cost functional and the action/weight primitives used for coherence collapse in RS gravity. Defines recognition and rate actions, Born weights (including the sin-squared form), and SI coherence mass/time scales. Gravity and collapse calculations cite these definitions. Content is mostly definitional, with short nonnegativity and positivity lemmas.

claimModule introducing the J-cost $J(x)=\frac12(x+x^{-1})-1$, rate and recognition actions, the identity linking cost to action, Born weight $w=\sin^2(\theta)$ with positivity and normalization, and coherence scales $m_{\mathrm{coh}}$ (kg) and $\tau_{\mathrm{coh}}$ (s).

background

Recognition Science fixes a unique symmetric cost on positive reals, the J-cost $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$). It is the T5 landmark of the forcing chain and obeys the Recognition Composition Law. This Gravity-domain module records that cost together with the action functionals and Born-rule weights needed for coherence-collapse estimates.

Upstream Constants supplies the RS time quantum $\tau_0=1$ tick. From it the module exposes coherence mass $m_{\mathrm{coh}}$ and coherence time $\tau_{\mathrm{coh}}$ in SI units, so gravitational decoherence rates can be written in laboratory language.

Sibling declarations cover nonnegativity of $J$, positivity of rate action and Born weight, the relation $C=2A$ between cost and action, the trigonometric identity for the Born weight, and its normalization.

proof idea

Definition module, not a theorem chain. Jcost is introduced by the standard closed form; Jcost_nonneg is a direct algebraic nonnegativity argument. rate_action and recognition_action are defined and shown positive. C_equals_2A is an algebraic identity. born_weight is defined, proved positive, identified with $\sin^2$, and normalized. m_coh_kg and tau_coh_s are unit-converted constants built from Constants. No multi-step forcing or analytic estimates appear here.

why it matters in Recognition Science

Supplies the cost, action, and Born-weight layer for gravitational coherence collapse inside Recognition Science. J-cost is the T5 forcing-chain landmark; the Born-weight block connects collapse amplitudes to the same cost structure. Coherence mass and time give SI handles on collapse thresholds (Berry scale, dream fraction) when gravity is present. The import graph currently lists no downstream clients, so this module is a definitional base for later Gravity results rather than a leaf theorem. It does not itself close any open scaffold.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (17)