kernel_ratio_dimensionless
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 λ.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not determine the numerical value of the exponent α.
- Does not constrain the amplitude constant C.
- Does not establish positivity or monotonicity of the kernel.
- Does not reference J-cost, defectDist, or the forcing chain T0-T8.
formal statement (Lean)
178theorem kernel_ratio_dimensionless (lam : ℝ) (hlam : lam ≠ 0) (k a tau0 : ℝ) :
179 (lam * a) / ((lam * k) * tau0) = a / (k * tau0) := by
proof body
Term-mode proof.
180 field_simp [hlam]
181
182/-! ## Self-Similarity Derivation of α -/
183
184/-- Structure encoding the self-similarity assumption for α derivation. -/