pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Gravity.CoherenceCollapse

show as:
view Lean formalization →

Gravity.CoherenceCollapse supplies the J-cost functional and derived objects for coherence collapse modeling in gravitational settings. It defines J(x) = ½(x + x^{-1}) - 1 together with action rates, Born weights, and coherent mass and time scales. Researchers deriving RS-based collapse rates or normalization conditions cite these objects. The module consists of direct definitions and elementary algebraic positivity statements.

claim$J(x) = ½(x + x^{-1}) - 1$, rate_action, recognition_action, born_weight = sin²θ with normalization, C = 2A, m_coh in kg, and τ_coh in s.

background

Recognition Science derives physics from a single functional equation whose core object is the J-cost. This module sits in the Gravity domain and imports the base time quantum τ₀ = 1 tick from Constants. It introduces J-cost as the recognition cost measure J(x) = ½(x + x^{-1}) - 1, non-negative rate quantities, and Born-rule weights.

proof idea

This is a definition module. It states Jcost by the standard formula, proves non-negativity by direct expansion, defines rate_action and recognition_action with positivity, sets born_weight = sin²θ together with its positivity and normalization, records the C_equals_2A relation, and introduces the physical scales m_coh_kg and tau_coh_s.

why it matters in Recognition Science

The module supplies the J-cost and coherence quantities that support gravitational collapse calculations within Recognition Science. It connects to the J-uniqueness step of the forcing chain and supplies objects used for mass-ladder and action derivations. No downstream theorems are listed in the current graph.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (17)