module module moderate

`IndisputableMonolith.PDG.Fits`

This module defines structures and predicates for verifying the acceptability of all lepton species against PDG thresholds using chi-squared measures. Particle physicists and Recognition Science modelers would cite it to confirm zero-deviation fits for electron, muon, and tau entries. The module is built from type definitions and explicit zero-chi2 witnesses for the leptons.

claimThe module introduces $SpeciesEntry$, the scaling map $z$, the deviation measure $chi^2$, the acceptability predicate, and zero-$chi^2$ witnesses $z_e=0$, $z_mu=0$, $z_tau=0$, $chi^2_{leptons}=0$.

background

In the PDG domain, this module provides the interface for fitting experimental particle data to the Recognition Science framework. It defines SpeciesEntry as a data record holding species-specific parameters, z as the normalized position on the phi-ladder, chi2 as the squared error from target values, and concrete entries e_entry, mu_entry, tau_entry for the three charged leptons. The leptonsWitness and associated zero lemmas establish that these entries satisfy the acceptability condition exactly.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the lepton-sector data that supports the broader Recognition Science claims on mass quantization and the eight-tick octave structure. It feeds into theorems establishing the phi-ladder consistency for fundamental particles by providing the explicit zero-chi2 fits at the model's predicted z values.

scope and limits

Does not include numerical evaluations or plots of the chi2 surfaces.
Does not cover quark or boson species beyond leptons.
Does not derive the z values from first principles.
Does not address threshold variations beyond the defined acceptable predicate.

declarations in this module (60)

structure SpeciesEntry L7
def z L14
def chi2 L17
def acceptable L20
def e_entry L25
def mu_entry L28
def tau_entry L31
def leptonsWitness L34
lemma z_e_zero L36
lemma z_mu_zero L39
lemma z_tau_zero L42
lemma chi2_leptons_zero L45
lemma acceptable_leptons L48
def u_entry L60
def d_entry L61
def s_entry L62
def c_entry L63
def b_entry L64
def t_entry L65
def quarksWitness L67
lemma z_u_zero L69
lemma z_d_zero L70
lemma z_s_zero L71
lemma z_c_zero L72
lemma z_b_zero L73
lemma z_t_zero L74
lemma chi2_quarks_zero L76
lemma acceptable_quarks L79
def W_entry L94
def Z_entry L95
def H_entry L96
def bosonsWitness L98
lemma z_W_zero L100
lemma z_Z_zero L101
lemma z_H_zero L102
lemma chi2_bosons_zero L104
lemma acceptable_bosons L107
def p_entry L119
def n_entry L120
def Delta_pp_entry L121
def Delta_p_entry L122
def Delta_0_entry L123
def Delta_m_entry L124
def baryonsWitness L126
lemma z_p_zero L129
lemma z_n_zero L130
lemma z_Dpp_zero L131
lemma z_Dp_zero L132
lemma z_D0_zero L133
lemma z_Dm_zero L134
lemma chi2_baryons_zero L136
lemma acceptable_baryons L139
structure Thresholds L155
structure Dataset L160
def defaultDataset L167
def acceptable_all L175
lemma acceptable_mono L182
lemma acceptable_all_mono L193
lemma acceptable_all_default_zero L205
def loadDatasetFromJson L216