pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.RecogSpec.ObservablePayloads

show as:
view Lean formalization →

The ObservablePayloads module specifies canonical dimensionless structures for lepton inter-generation mass ratios and CKM mixing angles. Researchers connecting Recognition Science ledger tiers to particle observables cite these payloads when mapping phi-ladder results to measurable quantities. The module consists of structure definitions together with list-conversion functions and basic extensionality properties.

claimLeptonMassRatios encodes the dimensionless ratios among electron, muon and tau masses; CkmMixingAngles encodes the CKM elements $V_{us}$, $V_{cb}$, $V_{ub}$.

background

In the RecogSpec domain the module introduces the primary observable payloads for the lepton sector. LeptonMassRatios and CkmMixingAngles are defined as structures whose fields hold the inter-generation ratios and mixing parameters. These objects rest on the phi-ladder and Recognition Composition Law already established in the unified forcing chain (T0-T8).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The payloads supply the canonical semantics consumed by MassLawFromLedger, which derives explicit phi-power expressions for the ratios from RSLedger tiers, and by BridgeDerivation, which obtains the mixing angles from RSBridge geometry. The module therefore anchors the observable sector of the Recognition framework.

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)