C_kernel_competing_pos
The declaration proves that the competing kernel amplitude C' = φ^{-3/2} is strictly positive. Workers on the Information-Limited Gravity spatial kernel would cite it when contrasting the structurally forced amplitude φ^{-2} against the competing value φ^{-3/2}. The proof proceeds by a direct term-mode reduction that unfolds the definition and invokes positivity of real powers with positive base.
claimThe competing amplitude satisfies $0 < C' = 0 < ϕ^{-3/2}$.
background
In the ILG Spatial-Kernel module the amplitude C is derived as φ^{-2} from the half-rung budget identity J(φ) + φ^{-2} = 1/2. The competing amplitude is introduced separately as the definition C_kernel_competing := φ^{-3/2}. This distinction traces to two prior accounts: the entropy paper giving C = φ^{-2} and Gravity_From_Recognition giving C = φ^{-3/2}, which differ by the factor φ^{1/2}. The module formalizes the Fourier-space kernel w_ker(k) = 1 + C · (k_0/k)^α with α = (1 - φ^{-1})/2.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of C_kernel_competing to φ^{-3/2} and applies the lemma Real.rpow_pos_of_pos using the fact that φ is positive.
why it matters in Recognition Science
This result secures the positivity of the competing amplitude in the ILG kernel comparison, supporting the selection of C = φ^{-2} as the structurally forced value via the half-rung budget. It fills the sign check in the spatial kernel derivation within the Recognition Science framework, specifically in the gravity domain. No open questions are directly touched, as the claim is fully proved.
scope and limits
- Does not derive the competing exponent -3/2 from the Recognition Composition Law.
- Does not prove positivity of the structural amplitude C = φ^{-2}.
- Does not establish numerical bounds beyond strict positivity.
- Does not connect to the eight-tick octave or spatial dimension D = 3.
formal statement (Lean)
198theorem C_kernel_competing_pos : 0 < C_kernel_competing := by
proof body
Term-mode proof.
199 unfold C_kernel_competing
200 exact Real.rpow_pos_of_pos phi_pos _
201
202/-- The competing amplitude is strictly larger than the structurally
203 forced amplitude. -/