Cosmology Scale Invariance Selection Cert

Scale invariance and its cost

Scale invariance is the property that a physical law looks the same after you shrink or stretch all distances and times. The classical example is a fractal like the Koch snowflake: zoom in and the shape repeats itself at every magnification. In particle physics, scale invariance is an idealization that real theories break, because particles have masses that set a definite size. The question of why the universe's laws are not scale-invariant is one of the oldest in cosmology.

In Recognition Science, the framework models physical law as the outcome of a ledger, a discrete record of recognition events, where each event carries a forced cost (a number that measures how expensive that recognition is). The central theorem of the framework proves that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. This function is not scale-invariant: J(cx) does not equal J(x) when c differs from 1. The module called the scale-invariance selection certificate formalizes what scale change actually costs.

The key result is an inequality. For any positive scale factor c and any positive x, the cost of the scaled value J(cx) is bounded by a combination of J(c) and J(x): J(cx) ≤ 2·J(c)·J(x) + 2·J(c) + 2·J(x). In plain words, the cost of changing scale is controlled by the cost of the scale change itself, plus the cost of the original value. The bound comes from an exact equality, the Recognition Composition Law: J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This equality is proved in the machine-checked library of formal theorems, with no unproved assumptions.

Two consequences follow directly. First, if the scale factor is 1, meaning no change at all, the cost is zero: J(1·x) = J(x). Second, the cost function is symmetric under inversion in log-space: J(x) = J(1/x). These facts together form the certificate, a structure that packages the composition law, the scale-cost bound, the free unit change, and the log symmetry as a single object. The certificate does not claim that the universe is scale-invariant; it claims that the framework's cost function makes scale change a measurable, bounded expense.

What this changes is the status of scale invariance in the framework. Instead of being a symmetry that the laws either have or lack, scale change becomes a quantity with a price. The pre-Big-Bang paper argued that cost-minimisation selects scale-invariant laws; the certificate sharpens that claim. It shows that the cost function is not naively scale-invariant, but that the ratio of costs is bounded by the cost of the scale change itself. A reader can now see why the framework's unique cost function makes scale a resource with a definite price, not a free parameter.

/-- 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)]

/-- The Recognition Composition Law (RCL) in inequality form:
    J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).
    The cost of combining x and y is controlled by their individual costs. -/
theorem rcl_equality {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
    Jcost (x * y) + Jcost (x / y) = 2 * Jcost x * Jcost y + 2 * Jcost x + 2 * Jcost y := by
  rw [Jcost_eq_sq hx.ne', Jcost_eq_sq hy.ne',
      Jcost_eq_sq (mul_pos hx hy).ne',
      Jcost_eq_sq (div_pos hx hy).ne']
  field_simp [hx.ne', hy.ne']
  ring

/-- 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 invariance in log-space: J is symmetric under inversion. -/
theorem log_space_symmetry {x : ℝ} (hx : 0 < x) :
    Jcost x = Jcost x⁻¹ := Jcost_symm hx

What this page does not claim

The universe is scale-invariant in the framework's account. The cost function J(x) = (x + 1/x)/2 - 1 is derived in this module. Scale invariance holds exactly for any physical law. The certificate proves any claim about the actual early universe.

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: