pith. machine review for the scientific record. sign in
theorem proved term proof high

alpha_from_self_similarity

show as:
view Lean formalization →

The theorem establishes that any self-similar ILG kernel whose exponent is fixed to (1 - 1/phi)/2 equals the canonical locked value alphaLock. ILG cosmologists cite it to anchor the perturbation exponent from the phi fixed point. The proof is a one-line simplification that equates the hypothesis directly to the definition of alphaLock.

claimLet $K$ be a self-similar kernel with exponent $alpha$. If $alpha = (1 - phi^{-1})/2$, then $alpha$ equals the locked constant $alpha_{lock}$.

background

The ILG kernel takes the form $w(k,a) = 1 + C (a/(k tau_0))^alpha$, where $tau_0$ is the fundamental recognition tick. SelfSimilarKernel is the structure that encodes the scaling property: the kernel evaluated at scale factor $phi a$ equals the original kernel scaled by $phi^alpha$. The upstream constant alphaLock is defined exactly as $(1 - 1/phi)/2$, the value forced by the phi fixed-point equation $phi^2 = phi + 1$.

proof idea

The proof is a one-line term-mode simplification that substitutes the constraint hypothesis into the definition of alphaLock and verifies syntactic identity.

why it matters in Recognition Science

This result discharges the placeholder derivation noted in the SelfSimilarKernel structure, confirming the exponent matches the locked value used throughout the kernel module. It supports downstream kernel properties such as positivity and monotonicity in scale factor. In the Recognition framework it instantiates the T6 self-similar fixed point for the ILG exponent, consistent with the eight-tick octave.

scope and limits

formal statement (Lean)

 194theorem alpha_from_self_similarity (hSS : SelfSimilarKernel)
 195    (h_constraint : hSS.alpha = (1 - 1 / phi) / 2) :
 196    hSS.alpha = alphaLock := by

proof body

Term-mode proof.

 197  simp [h_constraint, alphaLock]
 198
 199/-! ## Causality bounds (Beltracchi 2026 resolution)
 200
 201Two pathologies of the literal Riemann–Liouville / Fourier-only ILG formulation
 202were identified by P. Beltracchi (April 2026 internal note):
 203
 2041. **Cumulative-time growth.** Reading the time-domain RL form
 205   `ρ_eff(t) = ρ(t) + C τ₀⁻ᵅ Iᵅ[ρ(t)]` literally for an isolated mass `M`,
 206   the gravitational acceleration grows as `t^α` without bound.
 207
 2082. **Infrared divergence.** The Fourier-space kernel
 209   `w(k,a) = 1 + C (a / (k τ₀))^α` diverges as `k → 0`, making the
 210   homogeneous-background limit incoherent and naive perturbation theory
 211   ill-defined.
 212
 213Both pathologies are forced by reading the kernel as (i) a cumulative-time
 214convolution and (ii) a free-running k-space multiplier. The resolution from
 215the recognition-operator forcing chain is structural:
 216
 217- The ledger lag is **per recognition tick**, not per cumulative cosmic time.
 218  At rest in equilibrium, the ledger is at `J(1) = 0` and there is no
 219  "memory backlog" to integrate. The working kernel is a **dynamical-time**
 220  kernel `w(T_dyn)`, not a cumulative-time RL convolution.
 221- The kernel acts on **gradient flow** of the ledger, not on the ledger value.
 222  A homogeneous distribution sits at `J = 0` with no flow, so the background
 223  mode is unaffected (`kernel_background = 1`).
 224- The IR is bounded by the **recognition horizon** `R_H = c/H`. Below
 225  `k_min = a H / c`, no causal ledger update can occur, and the kernel
 226  saturates at `kernel(k_min)`.
 227
 228This section formalizes the IR-bounded perturbation kernel, proves the
 229boundedness theorem, and exposes the perturbation/background split that
 230makes ILG self-consistent for cosmological perturbation theory.
 231
 232The original `kernel` definition above is preserved unchanged for backward
 233compatibility; the new `kernel_perturbation` and `kernel_background`
 234distinguish the two physical regimes.
 235-/
 236
 237/-- The IR-bounded ILG perturbation kernel:
 238
 239  `w_pert(k_min, k, a) = 1 + C · (a / (max(k_min, k) · τ₀))^α`
 240
 241For `k ≥ k_min` this collapses to the original `kernel P k a`. For `k < k_min`
 242the wavenumber saturates at `k_min`, capping the enhancement at
 243`kernel(k_min)`. The IR cutoff `k_min` is physically the inverse recognition
 244horizon `a H / c`. -/

depends on (37)

Lean names referenced from this declaration's body.

… and 7 more