torsion_differences
plain-language theorem explainer
The theorem establishes the torsion differences tau 1 minus tau 0 equals 11, tau 2 minus tau 1 equals 6, and tau 2 minus tau 0 equals 17 in the Recognition Science particle model. Quark flavor physicists deriving the CKM matrix from torsion geometry would cite this to fix the generation schedule. The proof reduces the claim to arithmetic identities by unfolding tau through the passive field edges and wallpaper groups definitions then applying omega.
Claim. Let $tau_0, tau_1, tau_2$ denote the torsion parameters for the three generations. Then $tau_1 - tau_0 = 11 land tau_2 - tau_1 = 6 land tau_2 - tau_0 = 17$.
background
In the CKM derivation module the torsion schedule is extracted from the three-dimensional cube geometry. The passive_field_edges function returns cube_edges D minus active_edges_per_tick, which equals 11 when D equals 3. The wallpaper_groups constant is set to 17, the number of distinct two-dimensional wallpaper groups enumerated by Fedorov.
proof idea
The proof applies simp only to the identifiers tau, E_passive, W, passive_field_edges, cube_edges, active_edges_per_tick, D, and wallpaper_groups. This unfolds the differences into concrete numerals. The omega tactic then resolves the resulting conjunction of equalities.
why it matters
The result populates the torsion_structure component of the CKMCert constructed in the downstream ckm_cert_exists theorem. It realizes the generation torsion schedule {0, 11, 17} outlined in the module documentation for the CKM derivation from phi-geometry. Within the Recognition Science framework this supplies the numerical anchor for the Wolfenstein parameters lambda, lambda squared, and lambda cubed that match the PDG values for V_us, V_cb, and V_ub.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.