module module moderate

`IndisputableMonolith.Physics.WeakForceEmergence`

WeakForceEmergence supplies definitions for the Fermi constant G_F and related weak-interaction quantities in Recognition Science units. Physicists deriving electroweak scales from the phi-ladder and J-cost ledger would cite these objects. The module assembles definitions that rest on the imported PhiForcing and ElectroweakBosons results, with no internal theorem proofs.

claimThe Fermi constant is the quantity $G_F$ (in GeV$^{-2}$) obtained from the RS time quantum and the golden-ratio ladder after the electroweak boson masses are fixed.

background

The module imports the RS time quantum τ₀ = 1 tick from Constants and the self-similarity argument that forces φ from a discrete ledger with J-cost from PhiForcing. It further imports the RS derivation of W and Z masses via the Higgs mechanism and weak mixing angle from ElectroweakBosons. The local setting is therefore the emergence of the weak nuclear force as a consequence of the eight-tick octave and three-dimensional spatial structure already established upstream.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete weak-force parameters that sit between the phi-forcing chain (T5–T8) and any later unification or decay calculations. It therefore closes the interface from the abstract J-cost ledger to the observable Fermi constant and boson counts that appear in the sibling declarations.

scope and limits

Does not derive the full electroweak Lagrangian.
Does not compute numerical decay widths or cross sections.
Does not address neutrino masses or mixing angles beyond the listed doublets.
Does not prove gauge invariance of the SU(2) generators.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.PhiForcing module_import
IndisputableMonolith.Physics.ElectroweakBosons module_import

declarations in this module (28)

def fermiConstant L53
def hbar_c_GeV_fm L56
def weakRange_fm L59
def su2Generators L64
def weakBosonCount L67
theorem su2_from_3d L70
theorem weak_bosons_eq_generators L73
def leftHandedCouples L78
def rightHandedCouples L81
theorem parity_violation L84
def leptonDoublet L90
def quarkDoublet L93
def doubletsPerGeneration L96
def totalDoublets L99
theorem weak_range_short L104
def gf_from_mw L110
theorem gf_matches L116
def totalWeakPolarizations L202
theorem weak_polarizations_near_8 L204
theorem nine_eq_8_plus_1 L207
def weakIsospin L210
theorem doublet_from_isospin L213
def betaDecayViaW L218
def muonDecayViaW L221
theorem charged_current_uses_W L224
def ckmDimension L230
def ckmParameters L233
theorem ckm_params_3_plus_1 L236