module module high

`IndisputableMonolith.Masses.BaselineDerivation`

This module supplies the recognition cost functional J and baseline mass quantities such as T_min and octave offsets for the Recognition Science mass derivations. Mass-spectrum researchers cite these objects when constructing the phi-ladder yardsticks. The module consists of definitions together with elementary algebraic properties that rest on the imported constants and anchor modules.

claim$J(x) = (x + x^{-1})/2 - 1$ for $x > 0$, together with the minimum tick count $T_0$ at three dimensions, the octave offset, and the total geometric content of the cubic ledger.

background

The module sits inside the Recognition Science forcing chain (T0-T8) and imports the RS-native time quantum τ₀ = 1 tick from Constants. It also draws the fine-structure derivation (4π from Gauss-Bonnet on the cubic ledger) from AlphaDerivation and the parameter-free mass anchors from Masses.Anchor. The central object is the J-cost functional, defined for positive reals and satisfying J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) via the Recognition Composition Law.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions supply the baseline layer that later mass theorems apply to obtain the phi-ladder spectrum. They connect directly to the mass manuscripts via the Anchor module and support the eight-tick octave and D = 3 spatial dimensions fixed by the forcing chain. The module closes the first step of the geometric-content calculation before higher rungs are added.

scope and limits

Does not claim numerical agreement with measured particle masses.
Does not derive specific particle masses beyond the geometric baseline.
Does not address higher-order corrections on the phi-ladder.
Does not extend the J functional outside positive reals.

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