module module high

`IndisputableMonolith.Masses.BaselineDerivation`

BaselineDerivation module defines the J recognition cost and computes baseline mass quantities such as neutrino_baseline_int using the phi-ladder at D=3. Mass researchers working from first principles cite its T_min_at_D3 and total_geometric_at_D3 results. The module assembles definitions and short algebraic lemmas on J and geometric content.

claim$J(x) = \frac12(x + x^{-1}) - 1$ for $x > 0$, with $T_{\min}$ at three dimensions, octave offset, total geometric content, and neutrino baseline integral.

background

The module sits in the Masses domain and imports the RS time quantum $\tau_0 = 1$ tick from Constants, the $\alpha^{-1}$ derivation from cubic ledger geometry in AlphaDerivation, and canonical mass anchors from Masses.Anchor.

It introduces the J-cost functional $J(x) = \frac12(x + x^{-1}) - 1$ (equivalently $\cosh(\log x) - 1$), its nonnegativity, value at one, and the Recognition Composition Law. Sibling definitions cover $T_{\min}$, octave_offset, total_geometric_content at D=3, and neutrino_baseline_int.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the J-cost and baseline objects that support the mass formula yardstick $\times \phi^{{\rm rung}-8+{\rm gap}(Z)}$ on the phi-ladder. It fills the T5 J-uniqueness and T7 eight-tick octave steps, linking the alpha band and D=3 geometry to mass baselines in the Anchor module.

scope and limits

Does not claim numerical agreement with measured particle masses.
Does not derive the complete particle mass spectrum.
Does not incorporate interactions or higher-order corrections.
Does not extend beyond RS-native units or the phi-ladder.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import
IndisputableMonolith.Masses.Anchor module_import

declarations in this module (35)

def J L53
theorem J_at_one L55
theorem J_nonneg L58
theorem J_eq_zero_imp_one L72
theorem nontriviality_from_cost L84
def T_min L96
theorem T_min_at_D3 L99
def octave_offset L103
theorem octave_offset_eq L105
def total_geometric_content L117
theorem total_geometric_at_D3 L122
def neutrino_baseline_int L125
theorem neutrino_baseline_eq L127
def lepton_baseline L141
theorem lepton_baseline_eq L143
theorem lepton_baseline_matches_anchor L148
def edges_per_face L159
theorem edges_per_face_at_D3 L162
def quark_baseline L165
theorem quark_baseline_eq L167
theorem quark_baseline_matches_anchor_up L172
theorem quark_baseline_matches_anchor_down L176
def color_offset L188
theorem color_offset_eq L190
theorem color_offset_eq_quark_baseline L194
theorem generation_ordering L205
theorem generation_ordering_general L215
def W_endo L231
theorem W_endo_at_D3 L234
def Z_poly L246
theorem Z_strictly_increasing L250
theorem minimal_complete_coefficients L267
theorem lepton_rungs L277
theorem quark_rungs L289
theorem neutrino_rung L301