lambda_structural_discrepancy
plain-language theorem explainer
The RS structural Wolfenstein λ (from the φ⁻³ rung) and the PDG reference differ by under 6% relatively. CKM and flavor workers cite it as the raw geometric match before any face-flux correction. The proof is pure interval arithmetic: bounds from lambda_RS_interval against the fixed PDG number, closed by linarith.
Claim. The relative discrepancy between the Recognition Science structural Wolfenstein parameter $\lambda_{\mathrm{RS}}$ and the PDG reference $\lambda_{\mathrm{PDG}}$ satisfies $|\lambda_{\mathrm{RS}}-\lambda_{\mathrm{PDG}}|/\lambda_{\mathrm{PDG}}<0.06$.
background
The module CKMExact derives Wolfenstein CKM parameters from Q₃ cube geometry: Gray-code flip counts (4,2,2) on the three axes, generation torsion gaps Δτ₁₂=11 and Δτ₂₃=6, and face-flux ratios that correct the structural A to 9/11. The same geometry governs the Cabibbo-scale parameter λ.
In RS, the structural λ sits on the φ-ladder at the dream-fraction rung φ⁻³ (primer landmark). The PDG reference used here is the fixed real 0.2265. An upstream interval lemma supplies strict bounds on the RS value, reported in-module as the structural window (0.234, 0.238), while the experimental band is roughly (0.222, 0.232).
The eight-tick octave (T7) and the face-flux ratio faceFlux₂₃/faceFlux₁₂ = 4/6 enter only as the pending multiplicative correction sketched after the proof; this theorem itself compares the uncorrected structural number to PDG.
proof idea
Tactic proof, no deep lemmas. Unfold the PDG constant to the concrete positive real 0.2265. Clear the division via div_lt_iff₀ (denominator positivity by norm_num). Project the two sides of lambda_RS_interval as lower and upper bounds on λ_RS. Rewrite the absolute-value claim as a two-sided linear inequality (abs_sub_lt_iff), then discharge both sides by linarith against those bounds and the fixed PDG value.
why it matters
Places the Cabibbo-scale Wolfenstein λ inside the same Q₃ story that produces A_corrected = 9/11 and the 44-link among α⁻¹, η_B ≈ φ⁻⁴⁴, and CKM. The doc-comment frames it as confirmation of the φ⁻³ origin, with only a small geometric correction still open.
That correction is stated as a precise hypothesis in the following comment: λ_corrected = λ_RS × (faceFlux₂₃/faceFlux₁₂)^(1/8) ≈ 0.236 × (4/6)^(1/8) ≈ 0.224, landing inside the PDG band, and tied to eight-tick periodicity (T7). No downstream theorems yet consume this lemma (used_by empty); it is a certified discrepancy bound awaiting the Real.rpow formalization of (2/3)^(1/8) ∈ (0.948, 0.955).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.