module module moderate

`IndisputableMonolith.Masses.BaselineDerivation`

Module BaselineDerivation supplies the J recognition cost functional together with T_min, octave_offset, and total geometric content for baseline mass derivations. Researchers constructing the phi-ladder mass formula from the forcing chain cite these objects. The module consists entirely of definitions and elementary properties with no theorems.

claim$J(x) = \frac12(x + x^{-1}) - 1$ (recognition cost), $J(1) = 0$, $J(x) \ge 0$ for $x > 0$, $T_{\min}$ at $D=3$, octave offset, total geometric content at $D=3$, and neutrino baseline integer.

background

The module imports Constants (with $\tau_0 = 1$ tick), AlphaDerivation (deriving $\alpha^{-1}$ from cubic ledger vertex deficits), and Masses.Anchor (canonical mass constants). It introduces the J-cost functional $J(x) = \frac12(x + x^{-1}) - 1$, defined for $x > 0$, along with its basic properties and extensions to $T_{\min}$, octave_offset, and total_geometric_content. These objects sit inside the Masses domain and prepare the phi-ladder mass formula.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the J functional and auxiliary quantities required by the mass derivation chain in Masses.Anchor. It directly implements the J-uniqueness step (T5) of the forcing chain and supports the eight-tick octave (T7) and $D=3$ (T8) structure used for baseline masses.

scope and limits

Does not derive numerical mass values for specific particles.
Does not claim experimental agreement.
Does not extend beyond baseline definitions to full mass ladder.
Does not address dynamics or interactions.

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