C_kernel_competing
plain-language theorem explainer
Definition of the competing amplitude C' = φ^{-3/2} in the ILG spatial kernel. Researchers comparing kernel amplitudes against the half-rung budget would cite this value when testing the alternative from Gravity_From_Recognition. The definition is a direct real-power assignment of phi to the exponent -3/2.
Claim. The competing amplitude is defined by $C' = ϕ^{-3/2}$.
background
The ILG Spatial-Kernel module writes the Fourier modification as w_ker(k) = 1 + C · (k_0/k)^α with α already fixed. The structural amplitude satisfies the identity J(φ) + C = 1/2, which follows from φ² = φ + 1 and yields C = φ^{-2}. The module contrasts this with a prior account that produced the larger value φ^{-3/2}.
proof idea
Direct definition as the real power phi ^ (-(3/2 : ℝ)). No lemmas or tactics are invoked.
why it matters
Supplies the benchmark value used by C_competing_gt_C_kernel and C_competing_violates_budget to demonstrate that the alternative exceeds the half-rung budget. It marks the ambiguity between the two prior accounts of C that the module resolves in favor of the structurally forced φ^{-2}. Connects to the RCL-derived half-rung identity and the ILGSpatialKernelCert clauses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.