kernel_ratio_dimensionless
plain-language theorem explainer
The theorem proves that the ratio a/(k τ₀) in the ILG kernel remains unchanged under simultaneous rescaling of a and k by any nonzero real λ. Researchers deriving self-similar forms for the kernel exponent α would cite this to justify working exclusively with the dimensionless combination. The proof is a one-line term-mode simplification that cancels the common factor λ.
Claim. For any nonzero real number $λ$ and real numbers $k,a,τ_0$, the equality $λa/((λk)τ_0)=a/(kτ_0)$ holds.
background
The ILG kernel is defined as w(k,a)=1+C(a/(kτ₀))^α, where τ₀ denotes the fundamental tick duration taken from Constants.tau0. The module establishes that the kernel is well-defined and positive for physical parameter ranges and reduces to 1 when a equals kτ₀. Upstream results supply the definition of τ₀ as the duration of one tick in RS-native units together with structures for nuclear densities and crystal lattices that contextualize the kernel parameters.
proof idea
The proof is a one-line wrapper that applies field_simp to the hypothesis lam≠0, which cancels the common factor lam from numerator and denominator.
why it matters
This result underpins the scale-invariance assumption used in the module's Self-Similarity Derivation of α section. It ensures the kernel depends only on the dimensionless ratio a/(kτ₀), consistent with the Recognition Science requirement that physical quantities occupy discrete φ-tiers. No downstream theorems are listed, so the lemma serves as a local algebraic prerequisite within the ILG.Kernel formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.