Pith. sign in
module module moderate

IndisputableMonolith.Physics.ElectroweakZeroParamScoreCard

show as:
view Lean formalization →

Scorecard module comparing Standard Model electroweak free-parameter count against the Recognition Science claim of zero independent EW inputs. It packages four forcing inputs (masses, mixing, alpha, VEV/Fermi chain), four source theorems, and a certificate that the RS side multiplies to a zero residual. Cite it when auditing parameter reduction in the electroweak sector.

claimThe module records $N_{\mathrm{SM}}^{\mathrm{EW}}$ (Standard Model electroweak free-parameter count) versus $N_{\mathrm{RS}}^{\mathrm{EW}}=0$, together with four forcing inputs and four source theorems whose product score is positive on the SM side and zero on the RS side, conditional on $\alpha^{-1}$ lying in its certified band.

background

Recognition Science treats electroweak observables as derived, not fitted. Upstream, the Z mass sits on the phi-ladder (rung-1 EW sector: $m_Z = 2\varphi^{51}/10^6$ MeV). VEV consistency (P5a partial) shows the Higgs vacuum expectation value is fixed by the tree-level relation $v^2 = m_Z^2\sin^2\theta_W\cos^2\theta_W,\alpha^{-1}/\pi$, so $v$ is not an independent knob. FermiFromRSInputs then pushes that $v$ into $G_F = 1/(\sqrt{2},v^2)$.

AlphaBounds supplies interval control on $\alpha^{-1}$ in RS-native units. Constants fixes the RS time quantum. This module does not re-derive those identities; it tallies how many independent SM EW parameters remain once those chains are admitted, and asserts the RS residual count is zero.

proof idea

Definition-and-certificate module, not a single deep proof. It introduces integer parameter counts for SM versus RS, a bundle of four forcing inputs, and a parallel bundle of four source theorems. Score combinators (product and positivity) turn those into a numeric residual: SM reduction leaves a positive count; RS multiplies to zero. Alpha-in-band is the numeric gate from AlphaBounds. The top-level certificate aggregates the counts and scores into one electroweak zero-parameter claim object.

why it matters in Recognition Science

Closes the bookkeeping side of the electroweak zero-parameter claim: masses (ElectroweakMasses), VEV non-independence (VEVConsistency / P5a), Fermi constant from RS inputs, and the alpha band are not left as scattered lemmas but scored as a single reduction. No downstream consumers are wired yet (used_by empty), so this is a terminal physics audit artifact rather than an intermediate lemma. It sits beside the broader RS forcing chain (phi ladder, derived constants) as the EW-sector parameter census a referee checks before accepting "zero free EW parameters."

scope and limits

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (13)