pith. machine review for the scientific record. sign in
def definition def or abbrev high

maximal_theta23

show as:
view Lean formalization →

Recognition Science sets the atmospheric neutrino mixing angle to its symmetric maximum by assigning sin²θ₂₃ exactly 1/2. Neutrino modelers building φ-quantized PMNS matrices cite this as the baseline before small corrections. The definition is a direct constant assignment with no reduction steps or lemmas.

claimThe maximal atmospheric mixing satisfies sin²θ₂₃ = 1/2.

background

The module derives the PMNS neutrino mixing matrix from Recognition Science by treating the three angles as φ-quantized. Large mixing distinguishes neutrinos from quarks: θ₁₂ ≈ 34°, θ₂₃ ≈ 45°, θ₁₃ ≈ 8.6°. The local setting notes that maximal θ₂₃ signals an underlying symmetry, with observed sin²θ₂₃ ≈ 0.545 lying close but offset by a possible φ correction.

proof idea

The definition is a direct constant assignment of the real number 1/2.

why it matters in Recognition Science

This supplies the symmetric baseline hypothesis for θ₂₃ inside the PMNS construction from φ-angles. It fills the paper proposition on neutrino mixing angles from golden ratio geometry. The result touches the open deviation question and sits inside the broader forcing chain where T7 eight-tick periodicity and D = 3 spatial dimensions generate the symmetry.

scope and limits

formal statement (Lean)

  97noncomputable def maximal_theta23 : ℝ := 1 / 2

proof body

Definition body.

  98
  99/-- **Hypothesis 3: θ₁₃ from φ/10**
 100
 101    sin²θ₁₃ ≈ φ/100 = 0.01618
 102
 103    Observed ≈ 0.022, within 30%. Not great. -/

depends on (2)

Lean names referenced from this declaration's body.