Cosmology Scale Invariance Selection Cert No Scale Change Is Free

The cost of doing nothing

In mathematics and physics, a scale transformation multiplies every length, time, or other quantity by a fixed positive number. The declaration no_scale_change_is_free states the simplest possible fact about such transformations: multiplying by 1 changes nothing, so the cost of that transformation is zero. In the framework's own terms, the cost function J(x) satisfies J(1·x) = J(x) for every positive x. This is not a deep discovery; it is a direct consequence of the definition of J, and the machine-checked proof is one line: by simp.

The statement matters because of what it does not say. It does not say that all scale changes are free, nor that the laws of physics are scale-invariant. The framework's own theorems show the opposite: the cost of a genuine rescaling by a factor c is bounded by a positive expression involving the cost of c itself. The relevant bound, proved in the same module, is J(cx) ≤ 2·J(c)·J(x) + 2·J(c) + 2·J(x). This is the "cost of scale change" principle: changing scale is not free, only the trivial change by 1 is.

The declaration is one component of a larger certificate, ScaleInvarianceCert, which packages four properties of the cost function J: the Recognition Composition Law, the scale-change cost bound, the free-at-unit property, and log-space symmetry (J(x) = J(1/x)). The certificate is used in the framework's account of why scale-invariant physical laws are selected by cost-minimisation. The full claim, that among all cost functions only the scale-invariant form is selected, is a paper argument; the Lean module formalises only the structural facts listed above.

For a reader outside the framework, the practical lesson is that the triviality of multiplying by 1 is a theorem, not an assumption. It is the zero point against which all real scale changes are measured. The framework does not claim that nature is scale-invariant, only that the cost function treats the identity transformation as costless, which is a consistency requirement any reasonable cost function must satisfy.

/-- If c = 1 (no scale change), cost is zero. -/
theorem no_scale_change_is_free {x : ℝ} (hx : 0 < x) :
    Jcost (1 * x) = Jcost x := by simp

/-- Scale-change cost: J(cx) is controlled by J(x) and J(c). -/
theorem scale_change_cost {c x : ℝ} (hc : 0 < c) (hx : 0 < x) :
    Jcost (c * x) ≤ 2 * Jcost c * Jcost x + 2 * Jcost c + 2 * Jcost x := by
  have h := rcl_equality hc hx
  -- J(cx) + J(c/x) = 2J(c)J(x) + 2J(c) + 2J(x)
  -- J(cx) ≤ 2J(c)J(x) + 2J(c) + 2J(x) since J(c/x) ≥ 0
  linarith [Jcost_nonneg (div_pos hc hx)]

structure ScaleInvarianceCert where
  rcl : ∀ {x y : ℝ}, 0 < x → 0 < y →
    Jcost (x * y) + Jcost (x / y) = 2 * Jcost x * Jcost y + 2 * Jcost x + 2 * Jcost y
  scale_cost_bound : ∀ {c x : ℝ}, 0 < c → 0 < x →
    Jcost (c * x) ≤ 2 * Jcost c * Jcost x + 2 * Jcost c + 2 * Jcost x
  free_at_unit : ∀ {x : ℝ}, 0 < x → Jcost (1 * x) = Jcost x
  log_symmetric : ∀ {x : ℝ}, 0 < x → Jcost x = Jcost x⁻¹

What this page does not claim

The declaration does not claim that all scale changes are free, only the trivial change by 1. The declaration does not claim that physical laws are scale-invariant in general. The full selection of scale-invariant laws by cost-minimisation is a paper argument, not a machine-checked theorem.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/ScaleInvarianceSelectionCert.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: