wolfenstein_A_structural
plain-language theorem explainer
Defines the structural Wolfenstein A as the absolute torsion-gap ratio |Δτ₂₃|/|Δτ₁₂| on the generation ladder {0,11,17}. Anyone deriving CKM angles or the Jarlskog invariant from Q₃ cube geometry cites this constant. The body is a two-line quotient of natAbs of torsion gaps, not a proved equality.
Claim. The structural Wolfenstein $A$ parameter is the real number $A_{\mathrm{struct}} := |\Delta\tau_{23}|/|\Delta\tau_{12}|$, where $\Delta\tau_{ij}=\tau_j-\tau_i$ are the generation torsion gaps on the ladder $\tau\in\{0,11,17\}$.
background
The module builds the CKM matrix as the overlap between mass and weak eigenstates on the three-generation space Fin 3, both fixed by Q₃ cube geometry. Mass eigenstates carry generation torsions $\tau\in{0,11,17}$ (ground, edge-dressed, edge+face-dressed). Off-diagonal mass overlaps are J-cost suppressed as $\varphi^{-|\Delta\tau_{ij}|}$.
The torsion gap $\mathrm{torsionGap},i,j:=\tau_j-\tau_i$ is the integer difference of those levels. The Wolfenstein $A$ parameter sets the scale of $V_{cb}$ (and enters $V_{ub}$, $V_{ts}$). In the exact CKM layer the same idea appears as $A_{\mathrm{structural}}=\Delta\tau_{23}/\Delta\tau_{12}$; here the cube module re-expresses it via absolute gaps so the ratio is a nonnegative real.
Gray-code chirality and even-sign-flip weak generators fix the angular skeleton; torsion gaps fix the hierarchical amplitudes. The doc notes the bare ratio is $6/11\approx 0.545$, with flip corrections still needed to approach the observed $A\approx 0.82$.
proof idea
Definitional, not a proof. The body evaluates $\mathrm{natAbs}(\mathrm{torsionGap},1,2)/\mathrm{natAbs}(\mathrm{torsionGap},0,1)$, i.e. $|\tau_2-\tau_1|/|\tau_1-\tau_0|$. With the fixed ladder $\tau=(0,11,17)$ this is the integer quotient $6/11$ once unfolded; that numerical identity is discharged later by A_structural_value via simp on torsionGap and τ plus norm_num.
why it matters
Supplies the RS-native Wolfenstein $A$ that every structural CKM and CP observable in this stack multiplies by. Downstream, A_structural_value pins the constant at $6/11$. The Jarlskog package uses it directly: jarlskog_structural := A_{\mathrm{struct}}^2\lambda_{\mathrm{struct}}^6\sin\delta$, and both jarlskog_positiveandcp_small_but_nonzero` open by positivity of this $A$.
In the broader framework this is the amplitude piece of CKM-from-cube: torsion gaps from the generation ladder (linked to eight-tick / cube structure and mass-basis J-cost suppression) replace fitted Wolfenstein parameters. The bare $6/11$ is intentionally pre-correction; flip-weight factors elsewhere close the gap toward the experimental $A\approx 0.82$. Without this def, structural $J$ and the claim that CP is small-but-nonzero from $\lambda^6$ rather than fine-tuning have no $A$ input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.