pith. sign in
module module high

IndisputableMonolith.RecogSpec.BridgeDerivation

show as:
view Lean formalization →

This module derives CKM mixing angles from the geometric cycle structure of the RS bridge. Flavor physicists in Recognition Science cite it to obtain V_cb and related parameters from ledger geometry rather than ad-hoc formulas. The module supplies typed definitions that map bridge cycles to observable mixing payloads.

claimMixing angles obtained from bridge cycles: $V_{cb} = g_2($loops$)$ and canonical forms derived from the RSBridge geometry.

background

The module imports Constants (defining the RS time quantum τ₀ = 1 tick), ObservablePayloads (providing typed records for dimensionless mass-ratio and mixing-angle payloads), and RSBridge (defining the rich bridge structure with geometric couplings). RSBridge states that in Recognition Science, CKM mixing angles come from ledger geometry. The local setting replaces raw List ℝ encodings with strongly typed payloads that carry canonical semantics for position-dependent quantities.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the bridge-to-mixing derivation that feeds the observable CKM parameters in the Recognition framework. It realizes the geometric origin of flavor mixing stated in the RSBridge module doc-comment.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (5)