C_kernel_competing_pos
plain-language theorem explainer
The theorem establishes strict positivity of the competing amplitude C' = φ^{-3/2} inside the ILG spatial kernel. Workers deriving kernel modifications or comparing amplitude channels cite the result when checking sign constraints on φ-powers. The proof is a one-line wrapper that unfolds the definition and invokes positivity of real exponentiation on a positive base.
Claim. $0 < ϕ^{-3/2}$
background
The module derives the ILG spatial-kernel amplitude from the half-rung budget identity J(φ) + φ^{-2} = 1/2, which follows from φ² = φ + 1 alone. This identity selects C = φ^{-2} as the structurally forced value over the earlier competing proposal C' = φ^{-3/2}. The referenced definition states C_kernel_competing : ℝ := phi ^ (-(3/2 : ℝ)) and records that C' is the competing amplitude.
proof idea
One-line wrapper that unfolds C_kernel_competing and applies Real.rpow_pos_of_pos with the upstream phi_pos hypothesis.
why it matters
The result supplies the sign check required when the module contrasts the forced amplitude C = φ^{-2} against the competing value C' = φ^{-3/2} that appears in prior three-channel arguments. It sits inside the spatial-kernel derivation that resolves the factor-of-φ^{1/2} discrepancy between the two accounts of C and is consistent with the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.