pith. sign in
module module high

IndisputableMonolith.Gravity.CoherenceCollapse

show as:
view Lean formalization →

Gravity.CoherenceCollapse supplies the J-cost functional and auxiliary definitions for quantifying recognition costs during coherence collapse in Recognition Science gravity models. It defines J(x) = ½(x + x^{-1}) - 1 together with rate_action, born_weight, and coherence scales m_coh_kg and tau_coh_s. Researchers constructing gravitational dynamics from the phi-ladder and Recognition Composition Law cite these when building collapse thresholds. The module consists entirely of definitions and elementary nonnegativity statements.

claim$J(x) = \frac12(x + x^{-1}) - 1$, together with the associated rate_action, born_weight, and coherence mass/time scales in the gravity domain.

background

The module resides in the Gravity domain and imports only Mathlib plus IndisputableMonolith.Constants, whose sole documented object is the fundamental RS time quantum τ₀ = 1 tick. It introduces the J-cost functional exactly as stated in its module doc-comment, along with sibling definitions Jcost_nonneg, rate_action_pos, born_weight_is_sin_sq, born_normalization, m_coh_kg and tau_coh_s. These objects operate under the Recognition Composition Law and the J-uniqueness fixed point of the forcing chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the J-cost and coherence-collapse primitives that later gravity constructions rely upon; no downstream declarations are listed in the current dependency graph. It directly encodes the J-uniqueness step (T5) inside the gravity setting and prepares the ground for deriving collapse thresholds from the eight-tick octave and phi-ladder.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (17)