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

toList

show as:
view Lean formalization →

Converts a LeptonMassRatios record to the ordered list of its three dimensionless ratios. ComputationBridge and SimplicialLedger modules cite it to supply mass data to ledger encodings and hinge summations. The definition is a direct list constructor on the mu_over_e, tau_over_e, and tau_over_mu fields.

claimFor a lepton mass ratio record $m$, toList$(m) = [m.μ/e, m.τ/e, m.τ/μ]$.

background

The ObservablePayloads module supplies strongly typed records for dimensionless observables, replacing earlier raw List ℝ fields. LeptonMassRatios is the structure holding the three inter-generation lepton ratios mu_over_e, tau_over_e, tau_over_mu. CkmMixingAngles supplies the parallel CKM structure but is not used by this conversion.

proof idea

One-line definition that applies the list constructor directly to the three fields of the LeptonMassRatios record.

why it matters in Recognition Science

Supplies the list interface required by LedgerComputation for observation encoding and by cubicHinges for constructing hinge lists in the simplicial ledger. It also feeds sensorEulerLedger constructions in NumberTheory, bridging typed payloads to the list-based machinery used in Regge sums and Euler event recording.

scope and limits

Lean usage

def example (m : LeptonMassRatios) : List ℝ := toList m

formal statement (Lean)

  34def toList (m : LeptonMassRatios) : List ℝ :=

proof body

Definition body.

  35  [m.mu_over_e, m.tau_over_e, m.tau_over_mu]
  36

used by (27)

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

depends on (2)

Lean names referenced from this declaration's body.