Standard Model Pmns Reactor Theta13 Rs

The reactor angle

Neutrinos change flavor as they travel, and the PMNS matrix is the standard model's bookkeeping for that mixing. One of its entries, theta_13, controls how much electron neutrinos from a reactor can turn into other flavors over a few kilometers. Reactor experiments such as Daya Bay and RENO measured sin^2(theta_13) to be about 0.0218, a small but nonzero number that was a major prize in the 2010s because it opened the door to measuring CP violation in neutrinos.

In Recognition Science, the module named PMNS_Reactor_Theta13_RS does not derive that measured value. Its docstring floats a research note: maybe sin^2(theta_13) relates to J(phi)^{1.7} or another power, where J(phi) is the framework's cost function and phi is the golden ratio. The note is explicit that this is where the idea was meant to go, not a result. The actual Lean code proves three general facts about the cost function applied to a ratio m/e: it is zero when m equals e, it is nonnegative for positive inputs, and the constant phi minus 3/2 is positive. Those facts are true for any positive inputs, so they say nothing specific to neutrinos.

In Recognition Science, a ledger, a discrete record of events, assigns a forced cost to any ratio of two quantities. The module defines domainCost as that cost applied to m divided by e, and then packages the three proved facts into a certificate structure. The certificate is inhabited, which means the facts are consistent, but the definition never ties m or e to reactor flux, baseline, or any neutrino observable. The module is a template, shared verbatim with 2383 sibling modules; what would make it a statement about theta_13 is a definition of m and e in the neutrino experiment's own terms.

The plain-language takeaway is a boundary: the framework's library proves the cost function's basic hygiene, and the reactor angle remains an open target, not a derived number. A reader should not mistake the certificate for a prediction. The module is honest about that, and the honest status is itself the useful fact: it marks where a derivation would have to start, with a physical definition of the ratio, before any comparison to Daya Bay's measurement could mean anything.

noncomputable def cert : PMNSTheta13Cert where
  cost_at_eq := domainCost_at_eq
  cost_nonneg := domainCost_nonneg
  threshold_pos := canonicalThreshold_pos

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The module derives the value of sin^2(theta_13) from the framework. The module proves any relation between the golden ratio and neutrino mixing. The certificate structure is a physical model of reactor antineutrino oscillations.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/StandardModel/PMNS_Reactor_Theta13_RS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: