pith. machine review for the scientific record. sign in
def definition def or abbrev high

C_kernel_competing

show as:
view Lean formalization →

The definition introduces the competing amplitude C' = φ^{-3/2} as a benchmark value drawn from an earlier three-channel argument. It is cited in downstream comparisons that establish its violation of the half-rung budget identity when added to J(φ). The definition is a direct real-power expression using the golden ratio.

claimThe competing amplitude is given by the real number $C' = ϕ^{-3/2}$.

background

The ILG spatial kernel modifies the Newton-Poisson relation in Fourier space as w_ker(k) = 1 + C · (k_0/k)^α with α = (1 - φ^{-1})/2. The module derives the structurally forced amplitude C = φ^{-2} from the half-rung budget identity J(φ) + C = 1/2, which follows from φ² = φ + 1 alone. Two prior accounts differ: the entropy paper gives C = φ^{-2} via three-channel factorization, while Gravity_From_Recognition gives C = φ^{-3/2}.

proof idea

One-line definition that directly assigns the real power phi raised to -3/2.

why it matters in Recognition Science

It supplies the benchmark value used by C_competing_gt_C_kernel and C_competing_violates_budget to show that φ^{-3/2} exceeds the half-rung budget when paired with J(φ). This contrast selects the forced amplitude C = φ^{-2} (equivalently 2 - φ) that satisfies the RCL-derived identity and lies in the observed band (0.380, 0.385).

scope and limits

formal statement (Lean)

 195def C_kernel_competing : ℝ := phi ^ (-(3 / 2 : ℝ))

proof body

Definition body.

 196
 197/-- `C'` is positive. -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.