pith. machine review for the scientific record. sign in
theorem proved term proof high

canonicalRSBridge_alpha

show as:
view Lean formalization →

The theorem states that the alpha exponent carried by the canonical recognition bridge on any RSLedger equals the locked value alphaLock = (1 - 1/phi)/2. Workers deriving CKM angles from ledger geometry cite it to fix the fine-structure input. The proof is a one-line reflexivity that follows from the bridge definition.

claimFor any RSLedger $L$, the fine-structure exponent of the canonical recognition bridge on $L$ equals the locked constant $(1 - 1/phi)/2$.

background

RSBridge supplies the geometric structure that turns ledger counts into CKM mixing angles. The module derives V_ub from alpha/2, V_cb from the 24 edge-dual count, and V_us from a phi-ladder projection with radiative correction. alphaLock is the canonical locked fine-structure constant defined as (1 - 1/phi)/2.

proof idea

The proof is a one-line reflexivity that matches the alphaExponent field of canonicalRSBridge L directly to alphaLock.

why it matters in Recognition Science

It anchors the fine-structure constant inside the bridge used for all three CKM angles. The result closes the step from ILG self-similarity to observable couplings and supports the geometric derivation of mixing parameters rather than their free assignment.

scope and limits

formal statement (Lean)

 122@[simp] theorem canonicalRSBridge_alpha (L : RSLedger) :
 123    (canonicalRSBridge L).alphaExponent = alphaLock := rfl

proof body

Term-mode proof.

 124
 125/-! ## Canonical Mixing Angle Values -/
 126
 127/-- V_cb = 1/24 for canonical bridge -/

depends on (11)

Lean names referenced from this declaration's body.