pith. machine review for the scientific record. sign in
theorem proved term proof high

bottomMSBarCert_holds

show as:
view Lean formalization →

The theorem certifies that the bottom quark MS-bar mass satisfies the Recognition Science scorecard at rung 21. It confirms the rung assignment, the PDG central value of 4.18 GeV, and positivity of the RS-predicted mass for positive couplings. The proof is a direct term construction of the certificate structure using reflexivity for the equalities and two prior positivity theorems.

claimThe bottom quark MS-bar mass certificate holds: the Recognition Science rung for the bottom quark equals 21, the PDG value satisfies $m_b(m_b) = 4.18$ GeV and is positive, and the RS-predicted mass is positive whenever the strong coupling at the bottom scale and at the Z scale are both positive.

background

The Bottom Quark MS-bar Mass Scorecard module records the RS assignment of the bottom quark (down-type, third generation) to rung 21 on the phi-ladder, together with the PDG 2024 central value 4.18 GeV for the MS-bar mass evaluated at the bottom scale. The certificate is formalized as a structure requiring four fields: rung equality to 21, positivity of the PDG mass, equality of that mass to the central value 4.18, and positivity of the RS-predicted mass for any positive values of the strong coupling at the bottom and Z scales. The module imports the constants file and the two-loop alpha_s and mass anomalous dimension modules from the QCD RGE sector.

proof idea

The proof is a term-mode construction of the BottomMSBarCert structure. It supplies reflexivity for the rung equality and the central-value equality, the theorem establishing PDG positivity, and the theorem establishing predicted-mass positivity (itself obtained by applying the running-mass positivity result to the bottom-at-MZ value).

why it matters in Recognition Science

This theorem closes the scorecard verification for the bottom quark mass in the RS framework, confirming consistency between the phi-ladder mass formula at rung 21 and the PDG central value. It supports the overall forcing chain (T5 J-uniqueness through T8 D=3) by supplying an explicit, proved instance of the mass prediction without axioms or sorrys. No downstream results currently depend on it.

scope and limits

formal statement (Lean)

  60theorem bottomMSBarCert_holds : BottomMSBarCert :=

proof body

Term-mode proof.

  61  { rung_eq_21 := rfl
  62    pdg_pos := m_b_PDG_pos
  63    pdg_central := rfl
  64    prediction_pos := m_b_predicted_pos }
  65
  66end
  67
  68end IndisputableMonolith.Physics.BottomMSBarScoreCard

depends on (3)

Lean names referenced from this declaration's body.