pmns_unitarity_exists
plain-language theorem explainer
The declaration defines the open proposition asserting existence of a 3 by 3 unitary complex matrix whose squared moduli reproduce the Recognition Science PMNS weight assignments from rung differences. Neutrino mixing researchers in the RS framework would cite it as the standing conjecture quarantined from certified claims. The definition consists of a direct existential quantification over the PMNSUnitarity predicate.
Claim. There exists a unitary matrix $U$ in $M_3(ℂ)$ such that for all indices $i,j$ the squared modulus $|U_{ij}|^2$ equals one-third the PMNS weight derived from the rung difference between the corresponding neutrino generations on the phi-ladder.
background
In the PMNS construction module the local setting introduces the PMNS matrix via the Recognition Science weight tensor on the phi-ladder. The predicate PMNSUnitarity requires both that the matrix be unitary and that its Born-rule probabilities match the predicted weights: for each entry the squared modulus equals pmns_weight of the rung difference divided by 3, where rungs label the neutrino states nu1, nu2, nu3. Upstream the RS-native units fix the gauge with tau0 equal to one tick and ell0 equal to one voxel. The Recognition structure supplies the base equality relation used in the weight construction.
proof idea
The definition is a direct existential quantification over the PMNSUnitarity structure, which itself decomposes into the unitarity condition and the weight-matching condition on rung differences.
why it matters
This declaration quarantines the existence claim for the PMNS matrix, ensuring it does not enter the hard-falsifiable angle and mass-splitting derivations in the MixingDerivation module. It touches the open question whether the weight tensor from the J-cost and phi-ladder admits a unitary realization. No downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.