pith. machine review for the scientific record. sign in
def definition def or abbrev high

charm_quark_pred

show as:
view Lean formalization →

Charm quark structural mass is defined as the golden ratio to the 45th power divided by two million in MeV. Quark scorecard verifications and absolute bridge certifications cite this value to confirm phi-power ratios with up and top quarks. The definition is a direct arithmetic expression based on the phi constant and the rung assignment for charm.

claim$phi^{45}/2000000$ MeV, where $phi$ is the golden ratio fixed point of the Recognition Composition Law, gives the structural mass prediction for the charm quark at rung 15 in the UpQuark sector.

background

Recognition Science assigns structural masses to fermions via a phi-ladder scaled by sector-specific factors. The rung function maps charm to 15 within the UpQuark sector, as defined in the Anchor module. Upstream results establish phi as the self-similar fixed point (T6) and provide the rung mappings for all fermions.

proof idea

This is a one-line definition that directly computes the golden ratio constant raised to the 45th power and divides by 2000000. It applies no lemmas beyond the built-in real exponentiation and the definition of phi.

why it matters in Recognition Science

The definition populates the charm entry in QuarkScoreCardCert, supporting the verification that ZOf equals 276 for up, charm, and top quarks and that their structural ratios match phi powers. It also enables the absolute bridge theorems establishing charm to up ratio as phi to the 11 and top to charm as phi to the 6. This completes the structural mass slot for rung 15 on the UpQuark phi-ladder, consistent with the eight-tick octave (T7) and three-dimensional spatial structure (T8).

scope and limits

formal statement (Lean)

 357noncomputable def charm_quark_pred : ℝ :=

proof body

Definition body.

 358  Constants.phi ^ (45 : ℕ) / 2000000
 359
 360/-- The top-quark structural mass (UpQuark sector, rung 21). -/

used by (14)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.