H_entry
plain-language theorem explainer
H_entry supplies the Higgs boson data point for PDG fits in the Recognition Science framework, recording observed mass 125.25 GeV, uncertainty 0.17, and exact match to the predicted mass. Researchers fitting Standard Model particles to the phi-ladder would cite this entry when verifying zero defect for the Higgs. The definition is a direct record construction from the SpeciesEntry structure.
Claim. The Higgs entry is the record with name ``H'', observed mass $125.25$, uncertainty $0.17$, and predicted mass $125.25$.
background
The PDG.Fits module organizes particle data using the SpeciesEntry structure, which consists of a string name, observed mass, experimental uncertainty sigma, and model-predicted mass. This structure supports direct comparison of observed values against Recognition Science predictions derived from the J-cost function and phi-ladder mass formula. Upstream results include the shifted cost H(x) = J(x) + 1 from CostAlgebra, which converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y), though the entry here employs H solely as a particle label. The sigma field denotes measurement uncertainty, distinct from sigma-charge in decision models or the divisor function.
proof idea
The definition is a one-line record construction that populates the SpeciesEntry fields directly with the Higgs parameters.
why it matters
H_entry is assembled into the bosonsWitness list and supports the lemma z_H_zero that establishes zero defect for this entry. It demonstrates an exact match of the Higgs mass to the Recognition Science mass formula on the phi-ladder, consistent with the eight-tick octave and D = 3. No open scaffolding questions are resolved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.