pmns_weight
The pmns_weight definition supplies the exponential weight W(dτ) = exp(−dτ ⋅ J_bit) for rung differences in the PMNS mixing matrix. Neutrino physicists deriving mixing angles from the Recognition ladder would cite this when normalizing Born-rule probabilities. It is a direct definition that transcribes the J-cost decay into real numbers, with the algebraic identity to φ^{-dτ} proved separately.
claimThe weight for a neutrino transition spanning rung difference $dτ$ is $W(dτ) = e^{-dτ · J_{bit}}$, equivalently $φ^{-dτ}$.
background
In Recognition Science the J-cost function measures the recognition defect between states on the phi-ladder, with J_bit the per-bit cost extracted from the PhiForcingDerived structure. The PMNS weights are the Born-rule probabilities over discrete rung steps in the neutrino sector, where dτ is the integer rung difference supplied by the RSBridge rung map. Upstream results fix the RS-native units with τ₀ = 1 tick and c = 1, while the ledger factorization supplies the J calibration and the integration gap A enforces the φ-power balance at D = 3.
proof idea
This is a one-line definition that applies the real exponential to the product of the rung difference cast to ℝ and the J-bit cost constant.
why it matters in Recognition Science
This definition is used by pmns_prob to normalize probabilities and by pmns_weight_eq_phi_pow to establish the phi-power form. It supplies the weight tensor required by the PMNSUnitarity structure. It implements the T5 J-uniqueness and T6 phi fixed point in the neutrino mixing sector, with the eight-tick octave constraining the rung spacing. The existence of a unitary matrix realizing these weights remains a quarantined conjecture.
scope and limits
- Does not assert that a unitary PMNS matrix exists.
- Does not provide numerical values for the mixing angles.
- Does not depend on the full PMNS construction conjecture.
- Applies only to integer rung differences.
Lean usage
noncomputable def example_prob : ℝ := pmns_prob 1 (pmns_weight 0 + pmns_weight 1 + pmns_weight 2)formal statement (Lean)
12noncomputable def pmns_weight (dτ : ℤ) : ℝ :=
proof body
Definition body.
13 Real.exp (- (dτ : ℝ) * J_bit)
14
15/-- **DEFINITION: PMNS Unitarity Forcing**
16 A matrix `U` satisfies `PMNSUnitarity U` if it is unitary and its Born-rule
17 probabilities `‖U i j‖^2` match the framework’s predicted weight tensor.
18
19 Note: existence of such a `U` is currently treated as a quarantined conjecture
20 (`IndisputableMonolith/Physics/PMNS/Construction.lean`). The certified particle
21 claims do **not** depend on that existence statement. -/