SelfSimilarKernel
plain-language theorem explainer
SelfSimilarKernel packages the self-similarity condition on the ILG kernel exponent α, requiring that scaling the argument by φ multiplies the deviation term by φ^α. Cosmologists working on modified gravity kernels cite this structure when deriving α from the golden-ratio fixed point. The declaration is a direct record type whose single field encodes the functional equation without further proof steps.
Claim. A structure consisting of a real exponent α together with the property that for any kernel parameter bundle P with the same α, and for all wave numbers k and scale factors a, the kernel satisfies w(k, φ a) = 1 + C φ^α (max(0.01, a/(k τ₀)) )^α.
background
The ILG kernel is defined as w(k,a) = 1 + C (a/(k τ₀))^α with α = (1-1/φ)/2. KernelParams bundles the exponent α, amplitude C, and reference time τ₀ together with the axiom 0 < τ₀. Upstream, τ₀ is the fundamental tick duration imported from Constants.tick and from the derivation sqrt(hbar_codata G_codata / (π c_codata^3))/c_codata. The golden ratio φ enters via the scale function φ^k in LargeScaleStructureFromRS.
proof idea
This declaration is a structure definition that directly encodes the self-similarity property without additional lemmas or tactics.
why it matters
It supplies the hypothesis hSS for the downstream theorem alpha_from_self_similarity, which applies the fixed-point equation φ² = φ + 1 to constrain α. In the Recognition Science setting the structure implements the self-similarity step that fixes the ILG exponent inside the kernel used for large-scale structure. The doc-comment notes it remains a placeholder pending the full derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.