correction_derivation_verified
plain-language theorem explainer
The declaration certifies that the integer coefficients 6, 10, and 3/2 in the PMNS radiative corrections are forced by the face and edge counts of a three-dimensional cube. Neutrino physicists modeling mixing angles would cite it to replace free parameters with geometric counting from the cubic ledger. The proof constructs the certificate structure via reflexivity for two fields, a geometric lemma for the third, and constructor tactics that invoke the three numerical equality theorems.
Claim. The certificate asserting atmospheric coefficient equals the face count of the 3-cube, solar coefficient equals the edge count of the 3-cube minus 2, Cabibbo coefficient equals the face count divided by 4, and that these equal 6, 10, and 3/2 respectively.
background
The module derives the integer coefficients appearing in the PMNS mixing angle predictions from geometric principles. The predictions are sin²θ₁₃ = φ⁻⁸, sin²θ₁₂ = φ⁻² − 10α, and sin²θ₂₃ = ½ + 6α, where the integers 6, 10, and 3/2 arise from cube topology: a 3-cube has 6 faces for the atmospheric correction, 12 edges minus 2 for the solar correction, and 6 faces over 4 for the Cabibbo correction. Upstream results supply the numerical equalities atmospheric_coefficient_eq_6, solar_coefficient_eq_10, and cabibbo_coefficient_eq_3_2 together with the geometric derivation cabibbo_coefficient_from_geometry.
proof idea
The proof is a tactic-mode construction of the CorrectionDerivationCert structure. It assigns the atmospheric field by reflexivity, the solar field by reflexivity, the cabibbo field by the lemma cabibbo_coefficient_from_geometry, and the coefficients_match field by a nested constructor that applies atmospheric_coefficient_eq_6, solar_coefficient_eq_10, and cabibbo_coefficient_eq_3_2.
why it matters
This theorem closes the geometric derivation of the PMNS correction coefficients, confirming they are forced by the 3-cube topology rather than free parameters. It supports the angle predictions that incorporate the eight-tick octave and D = 3 spatial dimensions from the Recognition Science chain. No downstream uses are recorded, leaving open whether the certificate will be invoked in a larger mixing-angle theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.