unnormalizedAmplSq
plain-language theorem explainer
Defines the unnormalized squared CKM amplitude between generation indices i and j on Fin 3: diagonal entries are 1, off-diagonal entries are φ raised to twice the structural suppression exponent. Anyone building CKM or Wolfenstein parameters from Q₃ torsion and Gray-code flip weights would cite it. The body is a direct piecewise definition, not a proved identity.
Claim. For generation indices $i,j \in \{0,1,2\}$, the unnormalized squared CKM amplitude is $1$ if $i=j$, and $\varphi^{2\,s(i,j)}$ otherwise, where $s(i,j)$ is the structural suppression exponent built from the torsion gap and flip-weight data, and $\varphi$ is the golden ratio.
background
The ambient module derives the CKM matrix from Recognition Science geometry on the $Q_3$ cube: mass eigenstates carry generation torsions ${0,11,17}$, weak eigenstates are labeled by even-sign-flip $SU(2)$ generators, and Gray-code chirality supplies flip counts $[4,2,2]$. Off-diagonal mass-basis overlap is suppressed by the J-cost of the torsion gap, schematically $\langle\mathrm{mass}_i|\mathrm{mass}j\rangle \propto \varphi^{-|\Delta\tau{ij}|}$.
Mixing angles are then expected to satisfy $\sin^2\theta_{ij} \propto (\mathrm{flip_count_ratio})\times\varphi^{-|\Delta\tau_{ij}|}$. Sibling definitions package the gaps ($\Delta\tau_{12}=11$, etc.), the suppression exponents, and the flip weights. The golden-ratio base $\varphi$ is the self-similar fixed point forced earlier in the RS chain (T6). This definition isolates the unnormalized $|V_{ij}|^2$ skeleton before unitarity fixes the overall scale.
proof idea
Not a proof: a noncomputable piecewise definition on $\mathrm{Fin},3\times\mathrm{Fin},3$. Equality of indices returns $1$. Otherwise the value is $\varphi$ raised to twice suppressionExponent i j, so an amplitude scaling as $\varphi^{s(i,j)}$ becomes an intensity scaling as $\varphi^{2s(i,j)}$. No lemmas are applied; the formula simply wires the already-defined suppression exponent into a real-valued matrix of squared amplitudes.
why it matters
This is the structural intensity kernel for CKM-from-cube: it encodes the claim that generation mixing is $\varphi$-suppressed by torsion gaps (with flip-weight structure living in the exponent siblings), while diagonals stay unsuppressed before normalization. The module doc frames $V_{ij}$ as the overlap of weak and mass eigenstates on the three-generation space; this definition supplies the unnormalized $|\mathrm{amplitude}|^2$ used when assembling Wolfenstein $\lambda,A,\rho,\eta$ and related mixing angles.
It sits downstream of the eight-tick / $Q_3$ gauge story and the torsion-forcing mass ladder, and upstream of any unitarity-normalized CKM construction in the same file. Exact numerical match to measured CKM entries is deferred: the nearby Wolfenstein commentary notes that pure $\varphi^{-11}$ is too small for $\lambda$, so overlap over the eight-tick cycle and Berry-phase refinements remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.