maximal_mixing
plain-language theorem explainer
The declaration proves that the tangent of pi divided by four equals one, encoding maximal mixing for the atmospheric neutrino angle at forty-five degrees in the PMNS matrix. Neutrino modelers in the Recognition Science framework cite it to fix the symmetric mixing point where the J-cost reaches zero. The proof is a direct one-line simplification using the standard tangent identity for pi over four.
Claim. $ tan(pi/4) = 1 $, the condition for maximal mixing in the atmospheric sector of the PMNS neutrino matrix.
background
The PMNS Neutrino Mixing Angles from RS module identifies the atmospheric angle theta_23 with pi over four. This corresponds to maximal mixing where the J-cost function, defined as (x plus x inverse over two) minus one, attains its minimum of zero at the symmetric point x equals one. The module equates the five PMNS parameters (theta_12, theta_23, theta_13, delta_CP, and two Majorana phases) to the configuration dimension D equals five.
proof idea
The proof is a one-line wrapper that applies the simp tactic with the Real.tan_pi_div_four lemma to reduce the expression directly to equality with one.
why it matters
This theorem supplies the maximal_mix field inside the pmnsCert definition, which certifies the complete set of five PMNS parameters. It anchors the atmospheric angle at the J-minimum, aligning with T5 J-uniqueness in the forcing chain and the structural observation that maximal mixing equals J equals zero. The module records zero sorrys and zero axioms for the full set of PMNS observations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.