pith. sign in
module module high

IndisputableMonolith.RecogSpec.ObservablePayloads

show as:
view Lean formalization →

ObservablePayloads supplies the canonical dimensionless structures for lepton mass ratios and CKM mixing angles. Mass-law and bridge derivations cite these payloads to standardize outputs from the RSLedger and RSBridge. The module is definition-only and contains no theorems or proofs.

claimThe module declares the payload structures LeptonMassRatios with components mu/e, tau/e, tau/mu and CkmMixingAngles with components V_us, V_cb, V_ub, all expressed as dimensionless quantities.

background

Recognition Science places all masses on the phi-ladder derived from the J-cost function and the Recognition Composition Law. This module isolates the lepton-sector inter-generation ratios as scale-independent observables. It supplies the data structures consumed by downstream modules that derive explicit ratio values from ledger tiers.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds LeptonMassRatios into MassLawFromLedger, which derives the ratios mu/e = phi^11, tau/e = phi^17, tau/mu = phi^6 from RSLedger tier structure. It also supplies CkmMixingAngles to BridgeDerivation for mixing-angle and g-2 results. The structures standardize observable outputs within the RecogSpec domain.

scope and limits

used by (3)

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

declarations in this module (9)