pith. sign in
module module high

IndisputableMonolith.Masses.BosonVerification

show as:
view Lean formalization →

The BosonVerification module supplies experimental mass values and electroweak bounds for the W, Z, and Higgs bosons to support Recognition Science mass comparisons. Researchers verifying phi-ladder outputs against collider data cite these constants. The module consists entirely of definitions and numerical bounds imported from Anchor and Constants, with no theorems or proofs.

claimThe module defines experimental quantities $m_W^exp$, $m_Z^exp$, $m_H^exp$, bounds on $sin^2 theta_W$, and relations such as $m_W^2 / m_Z^2 = cos^2 theta_W$ together with their experimental intervals.

background

This module sits in the Masses domain and imports the RS time quantum tau_0 = 1 tick from Constants together with the canonical mass constants from Anchor. Anchor centralises parameter-free constants derived from first principles in the Model layer, with no proofs claiming experimental agreement. The module adds experimental boson masses and electroweak mixing parameters to enable direct comparison with the phi-ladder mass formula.

proof idea

This is a definition module, no proofs. It organises experimental constants and simple algebraic relations for the electroweak sector as sibling definitions.

why it matters in Recognition Science

The module supplies the experimental interface required by the derivation chain in Anchor, feeding the overall mass verification structure in the Recognition Science framework. It anchors the T5 J-uniqueness and T8 D=3 steps by providing concrete comparison points for the phi-ladder yardstick formula.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (14)