The Scaling Functional Equation E(2v)=4E(v)

This note classifies all real functions of one positive variable obeying the self-similarity relation

E(2v)=4E(v),\qquad v>0.

(1)

The result is a clean illustration of how much — and how little — a regularity hypothesis buys. Iterating the relation and substituting $v=2^t$ reduces it to a periodicity statement, giving the general solution

E(v)=v^2\,P(\log_2 v),

(2)

with $P$ an arbitrary 1-periodic function. The surprise, compared with Cauchy’s additive equation, is that imposing measurability — or even continuity, or smoothness — does not collapse this family to a single closed form: the power law $v^2$ is always multiplied by a free log-periodic modulation $P$ . The rigid solutions $E(v)=cv^2$ are exactly the case where $P$ is constant. This is the phenomenon of discrete scale invariance: the equation only ties together scales differing by a factor of 2, so a whole periodic “constant of integration” survives at every level of regularity.

Lean formalization

The proofs in this note are formalized in Lean 4 + Mathlib in ScalingFunctionalEquationFlow.lean, which reproduces the note’s derivations in order. It is self-contained apart from Mathlib and a single reused result from CstarHomomorphismFlow.lean: the Hamel-basis solution of Cauchy’s equation, used to build the non-measurable example. Each Lean proof dropdown below includes the corresponding declaration verbatim from the compiled source, so the displayed code cannot drift from what is actually checked. Continuous integration runs lake build (which fails on any error or sorry), so every displayed proof is guaranteed to type-check.

Lean’s kernel guarantees each proof is correct. Whether a Lean statement faithfully captures the informal claim is a human judgement, so each dropdown is placed next to the statement it formalizes, for direct comparison.

Iterating the equation¶

The equation relates the value of $E$ at $v$ to its value at $2v$ . Applying it repeatedly forward,

E(2^2 v)=4E(2v)=4^2E(v),

(3)

and inductively

E(2^n v)=4^n E(v),\qquad n\in\mathbb N.

(4)

It also runs backward: replacing $v$ by $v/2$ gives $E(v)=4E(v/2)$ , i.e. $E(v/2)=\tfrac14 E(v)$ , and inductively the same formula holds for every integer exponent,

E(2^n v)=4^n E(v),\qquad n\in\mathbb Z.

(5)

In particular, $E$ on all of $(0,\infty)$ is completely determined by its restriction to a single fundamental domain $[1,2)$ for multiplication by 2: every $v>0$ is $v=2^n u$ with $n=\lfloor\log_2 v\rfloor$ and $u\in[1,2)$ , and then $E(v)=4^n E(u)$ . The values of $E$ on $[1,2)$ are completely free; this already shows the solution set is enormous.

ScalingFunctionalEquationFlow.lean

/-- **Iterating forward.** `E (2 ^ n v) = 4 ^ n E v` for every natural `n`. -/
theorem iterate_nat {E : ℝ → ℝ} (h : IsSolution E) (n : ℕ) {v : ℝ} (hv : 0 < v) :
    E ((2 : ℝ) ^ n * v) = (4 : ℝ) ^ n * E v := by
  induction n with
  | zero => simp
  | succ n ih =>
    have hpos : 0 < (2 : ℝ) ^ n * v := by positivity
    have hstep : E (2 * ((2 : ℝ) ^ n * v)) = 4 * E ((2 : ℝ) ^ n * v) := h _ hpos
    have hrw : (2 : ℝ) ^ (n + 1) * v = 2 * ((2 : ℝ) ^ n * v) := by ring
    rw [hrw, hstep, ih]; ring

/-- **Iterating in both directions.** `E (2 ^ n v) = 4 ^ n E v` for every integer `n`. -/
theorem iterate_int {E : ℝ → ℝ} (h : IsSolution E) (n : ℤ) {v : ℝ} (hv : 0 < v) :
    E ((2 : ℝ) ^ n * v) = (4 : ℝ) ^ n * E v := by
  induction n using Int.induction_on with
  | zero => simp
  | succ n ih =>
    have hpos : 0 < (2 : ℝ) ^ (n : ℤ) * v := by positivity
    have hstep : E (2 * ((2 : ℝ) ^ (n : ℤ) * v)) = 4 * E ((2 : ℝ) ^ (n : ℤ) * v) := h _ hpos
    have e2 : (2 : ℝ) ^ ((n : ℤ) + 1) = (2 : ℝ) ^ (n : ℤ) * 2 := by
      rw [zpow_add₀ (by norm_num : (2 : ℝ) ≠ 0), zpow_one]
    have e4 : (4 : ℝ) ^ ((n : ℤ) + 1) = (4 : ℝ) ^ (n : ℤ) * 4 := by
      rw [zpow_add₀ (by norm_num : (4 : ℝ) ≠ 0), zpow_one]
    rw [e2, e4]
    have harg : (2 : ℝ) ^ (n : ℤ) * 2 * v = 2 * ((2 : ℝ) ^ (n : ℤ) * v) := by ring
    rw [harg, hstep, ih]; ring
  | pred n ih =>
    have hpos : 0 < (2 : ℝ) ^ (-(n : ℤ) - 1) * v := by positivity
    have hstep : E (2 * ((2 : ℝ) ^ (-(n : ℤ) - 1) * v)) = 4 * E ((2 : ℝ) ^ (-(n : ℤ) - 1) * v) :=
      h _ hpos
    have e2 : (2 : ℝ) ^ (-(n : ℤ)) = 2 * (2 : ℝ) ^ (-(n : ℤ) - 1) := by
      rw [zpow_sub₀ (by norm_num : (2 : ℝ) ≠ 0), zpow_one]; ring
    have e4 : (4 : ℝ) ^ (-(n : ℤ)) = 4 * (4 : ℝ) ^ (-(n : ℤ) - 1) := by
      rw [zpow_sub₀ (by norm_num : (4 : ℝ) ≠ 0), zpow_one]; ring
    have hmul : 2 * ((2 : ℝ) ^ (-(n : ℤ) - 1) * v) = (2 : ℝ) ^ (-(n : ℤ)) * v := by
      rw [e2]; ring
    rw [hmul, ih, e4] at hstep
    linear_combination (-1 / 4 : ℝ) * hstep

The forward case is an induction using the equation; the integer case adds the backward step, recovering $E(2^{n-1}v)$ from $E(2^{n}v)=4E(2^{n-1}v)$ .

Reduction to a periodic gauge¶

To organize the free data, pass to the logarithmic variable. Every $v>0$ is $v=2^t$ with $t=\log_2 v\in\mathbb R$ , so set

F(t)=E(2^t).

(6)

Because $2\cdot 2^t=2^{t+1}$ , the equation $E(2v)=4E(v)$ becomes

F(t+1)=4F(t).

(7)

This is the discrete analogue of an exponential growth law. Divide out the expected growth by setting

G(t)=\frac{F(t)}{4^t}=\frac{E(2^t)}{4^t}.

(8)

Then (7) turns into pure periodicity:

G(t+1)=\frac{F(t+1)}{4^{t+1}}=\frac{4F(t)}{4\cdot 4^t}=\frac{F(t)}{4^t}=G(t).

(9)

So $G$ is an arbitrary function of period 1 — equivalently, an arbitrary function on the circle $\mathbb R/\mathbb Z$ .

ScalingFunctionalEquationFlow.lean

/-- **The heart of the reduction.** For a solution `E`, the gauge `G t = E (2 ^ t) / 4 ^ t` is
`1`-periodic: `G (t + 1) = G t`.  This is `F (t + 1) = 4 F t` divided by `4 ^ (t + 1)`. -/
theorem gauge_periodic {E : ℝ → ℝ} (h : IsSolution E) : Function.Periodic (gauge E) 1 := by
  intro t
  have h2 : (0 : ℝ) < (2 : ℝ) ^ t := Real.rpow_pos_of_pos (by norm_num) t
  have h4 : (0 : ℝ) < (4 : ℝ) ^ t := Real.rpow_pos_of_pos (by norm_num) t
  have hnum : E ((2 : ℝ) ^ (t + 1)) = 4 * E ((2 : ℝ) ^ t) := by
    have he : (2 : ℝ) ^ (t + 1) = 2 * (2 : ℝ) ^ t := by
      rw [Real.rpow_add (by norm_num), Real.rpow_one]; ring
    rw [he, h ((2 : ℝ) ^ t) h2]
  have hden : (4 : ℝ) ^ (t + 1) = 4 * (4 : ℝ) ^ t := by
    rw [Real.rpow_add (by norm_num), Real.rpow_one]; ring
  simp only [gauge, hnum, hden]
  field_simp

The Lean gauge E t is $G(t)=E(2^t)/4^t$ ; gauge_periodic is exactly $G(t+1)=G(t)$ .

Undoing the substitution is immediate. Using the real logarithm of the positive number $v$ , we have $2^{\log_2 v}=v$ and therefore $4^{\log_2 v}=(2^{\log_2 v})^2=v^2$ , so for every $v>0$

E(v)=v^2\,G(\log_2 v).

(10)

This is a definitional identity that needs only $v>0$ ; the content is that $G$ is 1-periodic.

ScalingFunctionalEquationFlow.lean

/-- **Reconstruction.** For *any* `E` and any `v > 0`, `E v = v ^ 2 * G (logb 2 v)` where
`G = gauge E`.  This is a definitional identity (`2 ^ (logb 2 v) = v`, `4 ^ (logb 2 v) = v ^ 2`),
needing only `v > 0`; combined with `gauge_periodic` it yields the general solution. -/
theorem eq_sq_mul_gauge {E : ℝ → ℝ} {v : ℝ} (hv : 0 < v) :
    E v = v ^ 2 * gauge E (Real.logb 2 v) := by
  have h2 : (2 : ℝ) ^ Real.logb 2 v = v := Real.rpow_logb (by norm_num) (by norm_num) hv
  have h4 : (4 : ℝ) ^ Real.logb 2 v = v ^ 2 := four_rpow_logb hv
  have hv2 : v ^ 2 ≠ 0 := by positivity
  simp only [gauge, h2, h4]
  field_simp

The general solution¶

Combining (9) and (10) gives the complete description of the solutions.

The converse direction is a direct computation: if $P$ has period 1 then $\log_2(2v)=\log_2 v+1$ gives

(2v)^2 P(\log_2(2v))=4v^2 P(\log_2 v+1)=4v^2P(\log_2 v)=4\bigl[v^2P(\log_2 v)\bigr].

(12)

ScalingFunctionalEquationFlow.lean

/-- **Converse.** For any `1`-periodic `P`, the map `v ↦ v ^ 2 * P (logb 2 v)` is a solution. -/
theorem isSolution_of_periodic (P : ℝ → ℝ) (hP : Function.Periodic P 1) :
    IsSolution (fun v => v ^ 2 * P (Real.logb 2 v)) := by
  intro v hv
  have hlog : Real.logb 2 (2 * v) = Real.logb 2 v + 1 := by
    rw [Real.logb_mul (by norm_num) hv.ne', Real.logb_self_eq_one (by norm_num)]; ring
  simp only [hlog, hP (Real.logb 2 v)]
  ring

ScalingFunctionalEquationFlow.lean

/-- **General solution (characterization).** `E` solves `E (2 v) = 4 E v` on `(0, ∞)` **iff**
there is a `1`-periodic `P` with `E v = v ^ 2 * P (logb 2 v)` for all `v > 0`. -/
theorem isSolution_iff_exists_periodic {E : ℝ → ℝ} :
    IsSolution E ↔
      ∃ P : ℝ → ℝ, Function.Periodic P 1 ∧
        Set.EqOn E (fun v => v ^ 2 * P (Real.logb 2 v)) (Set.Ioi 0) := by
  constructor
  · intro h
    exact ⟨gauge E, gauge_periodic h, fun v hv => eq_sq_mul_gauge hv⟩
  · rintro ⟨P, hP, hEq⟩ v hv
    have hv2 : (0 : ℝ) < 2 * v := by positivity
    have key := isSolution_of_periodic P hP v hv
    rw [hEq (show v ∈ Set.Ioi 0 from hv), hEq (show 2 * v ∈ Set.Ioi 0 from hv2)]
    exact key

The iff is the boxed classification: IsSolution E holds exactly when E agrees on $(0,\infty)$ with $v\mapsto v^2P(\log_2 v)$ for a 1-periodic P.

Classification by regularity¶

Formula (11) sets up a bijection

P\ \longleftrightarrow\ E,\qquad E(v)=v^2P(\log_2 v),\qquad P(t)=\frac{E(2^t)}{4^t},

(13)

between 1-periodic functions $P$ and solutions $E$ . Both directions are built from the smooth, smoothly invertible maps $v\mapsto v^2$ and $v\mapsto\log_2 v$ on $(0,\infty)$ (and $t\mapsto 2^t$ , $t\mapsto 4^t$ going back), so the regularity of $E$ equals the regularity of $P$ : $E$ is measurable / continuous / smooth iff $P$ is. The classification is therefore the classification of 1-periodic functions of the corresponding regularity, which is the crux of the matter.

Rigid solutions $cv^2$ ¶

The constant periodic functions $P\equiv c$ correspond to the rigid power-law solutions

E(v)=cv^2,\qquad c\in\mathbb R.

(14)

These always solve the equation ( $c(2v)^2=4cv^2$ ), and conversely the gauge of $cv^2$ is the constant $c$ , so they are exactly the constant- $P$ slice of (11).

ScalingFunctionalEquationFlow.lean

/-- The rigid family `E v = c v ^ 2` solves the equation (this is the constant-gauge case). -/
theorem isSolution_const_mul_sq (c : ℝ) : IsSolution (fun v => c * v ^ 2) := by
  intro v hv; ring

/-- The gauge of a rigid solution `c v ^ 2` is the constant `c`: rigid solutions are exactly the
constant-`P` case of the general solution. -/
theorem gauge_const_mul_sq (c : ℝ) (t : ℝ) : gauge (fun v => c * v ^ 2) t = c := by
  have hne : ((2 : ℝ) ^ t) ^ 2 ≠ 0 := by positivity
  simp only [gauge, four_rpow_eq]
  field_simp

Measurable and continuous solutions: regularity is not enough¶

Because regularity transfers across the bijection, the measurable solutions are exactly $E(v)=v^2P(\log_2 v)$ with $P$ a measurable 1-periodic function, and the continuous solutions are exactly those with $P$ continuous and 1-periodic.

ScalingFunctionalEquationFlow.lean

/-- If a solution `E` is measurable, so is its gauge `P = G`. -/
theorem measurable_gauge_of_measurable {E : ℝ → ℝ} (hE : Measurable E) :
    Measurable (gauge E) := by
  have h2 : Measurable (fun t : ℝ => (2 : ℝ) ^ t) := (continuous_rpow_base (by norm_num)).measurable
  have h4 : Measurable (fun t : ℝ => (4 : ℝ) ^ t) := (continuous_rpow_base (by norm_num)).measurable
  unfold gauge
  exact (hE.comp h2).div h4

/-- If `P` is measurable, so is the solution `v ↦ v ^ 2 * P (logb 2 v)`. -/
theorem measurable_solution_of_periodic {P : ℝ → ℝ} (hP : Measurable P) :
    Measurable (fun v => v ^ 2 * P (Real.logb 2 v)) := by
  have hlog : Measurable (fun v : ℝ => Real.logb 2 v) := by
    simp only [Real.logb]; exact Real.measurable_log.div_const _
  exact (continuous_pow 2).measurable.mul (hP.comp hlog)

This is the decisive difference from Cauchy’s additive equation. There, $a(x+y)=a(x)+a(y)$ together with measurability forces the single-parameter family $a(x)=cx$ (see Homomorphisms $\mathbb C^*\to\mathbb C^*$ ). Here, neither measurability nor continuity nor smoothness collapses the family: the space of continuous 1-periodic $P$ is already infinite dimensional. For a concrete witness, take $P(t)=\cos(2\pi t)$ , which gives the smooth solution

E(v)=v^2\cos(2\pi\log_2 v).

(15)

It is continuous on $(0,\infty)$ and solves $E(2v)=4E(v)$ , yet it is not of the form $cv^2$ : at $v=1$ it equals 1 (forcing $c=1$ ), while at $v=2^{1/2}$ it equals $2\cos\pi=-2$ (forcing $c=-1$ ).

ScalingFunctionalEquationFlow.lean

/-- `cosSolution` solves the equation. -/
theorem cosSolution_isSolution : IsSolution cosSolution :=
  isSolution_of_periodic _ cos_two_pi_periodic

/-- `cosSolution` is continuous on `(0, ∞)` (in fact smooth). -/
theorem cosSolution_continuousOn : ContinuousOn cosSolution (Set.Ioi 0) := by
  have hlog : ContinuousOn (fun v : ℝ => Real.logb 2 v) (Set.Ioi 0) := by
    apply Real.continuousOn_logb.mono
    intro x hx
    simp only [Set.mem_compl_iff, Set.mem_singleton_iff]
    exact (Set.mem_Ioi.mp hx).ne'
  have hcos : ContinuousOn (fun v : ℝ => Real.cos (2 * Real.pi * Real.logb 2 v)) (Set.Ioi 0) :=
    Real.continuous_cos.comp_continuousOn (continuousOn_const.mul hlog)
  exact (continuous_pow 2).continuousOn.mul hcos

/-- **Regularity is not enough.** `cosSolution` is continuous but is **not** of the rigid form
`c v ^ 2`: evaluating at `v = 1` forces `c = 1`, and at `v = 2 ^ (1/2)` forces `c = -1`. -/
theorem cosSolution_not_rigid : ¬ ∃ c : ℝ, ∀ v : ℝ, 0 < v → cosSolution v = c * v ^ 2 := by
  rintro ⟨c, hc⟩
  -- v = 1 forces c = 1
  have e1 : cosSolution 1 = c * 1 ^ 2 := hc 1 (by norm_num)
  have hc1 : c = 1 := by
    have : cosSolution 1 = 1 := by simp [cosSolution, Real.logb_one]
    rw [this] at e1; linarith
  -- v = 2 ^ (1/2) forces c = -1
  have hpos : (0 : ℝ) < (2 : ℝ) ^ ((1 : ℝ) / 2) := Real.rpow_pos_of_pos (by norm_num) _
  have e2 : cosSolution ((2 : ℝ) ^ ((1 : ℝ) / 2)) = c * ((2 : ℝ) ^ ((1 : ℝ) / 2)) ^ 2 := hc _ hpos
  have hsq : ((2 : ℝ) ^ ((1 : ℝ) / 2)) ^ 2 = 2 := by
    rw [pow_two, ← Real.rpow_add (by norm_num : (0 : ℝ) < 2),
      show (1 : ℝ) / 2 + 1 / 2 = 1 by norm_num, Real.rpow_one]
  have hval : cosSolution ((2 : ℝ) ^ ((1 : ℝ) / 2)) = -2 := by
    have hlog : Real.logb 2 ((2 : ℝ) ^ ((1 : ℝ) / 2)) = 1 / 2 :=
      Real.logb_rpow (by norm_num) (by norm_num)
    have hcos : Real.cos (2 * Real.pi * (1 / 2)) = -1 := by
      rw [show 2 * Real.pi * (1 / 2) = Real.pi by ring, Real.cos_pi]
    simp only [cosSolution, hlog, hsq, hcos]; ring
  rw [hval, hc1, hsq] at e2
  norm_num at e2

Recovering rigidity needs a second, incommensurable scale

What singles out $E(v)=cv^2$ is an extra constraint that kills all nonconstant periodic $P$ . The cleanest is a second scaling law $E(\lambda v)=\lambda^2 E(v)$ for some $\lambda>0$ with $\log_2\lambda$ irrational. Then $P$ has the two incommensurable periods 1 and $\log_2\lambda$ , so its group of periods is dense. A measurable function with a dense group of periods is almost everywhere constant (a Steinhaus-type argument), giving $E(v)=cv^2$ . Without measurability the dichotomy of Cauchy’s equation reappears: a Hamel basis of $\mathbb R$ over $\mathbb Q$ produces nonconstant functions with a dense period group, hence pathological non-rigid solutions. This stronger two-scale statement is not formalized here.

Non-measurable solutions¶

Without any regularity, $P$ may be any 1-periodic function, including non-measurable ones, which then yield non-measurable solutions $E$ . Such $P$ exist only through the axiom of choice. A convenient construction reuses Cauchy’s additive equation: take a non-linear additive map $a_0:\mathbb R\to\mathbb R$ (built from a Hamel basis, hence non-measurable) and normalize it to $a(x)=a_0(x)-a_0(1)\,x$ , so that $a$ is additive with $a(1)=0$ . Then $a$ is 1-periodic, since $a(t+1)=a(t)+a(1)=a(t)$ , and still non-measurable, so

E(v)=v^2\,a(\log_2 v)

(16)

is a non-measurable solution of $E(2v)=4E(v)$ .

ScalingFunctionalEquationFlow.lean

/-- **Without regularity the equation has non-measurable solutions.** There is a solution `E`
of `E (2 v) = 4 E v` that is not Lebesgue measurable.  The periodic factor is a non-linear additive
solution `a` of Cauchy's equation normalized so that `a 1 = 0` (hence `1`-periodic); such an `a`
exists by `CstarFlow.exists_additive_not_linear`, depends on a Hamel basis of `ℝ` over `ℚ`, and is
non-measurable by `CstarFlow.cauchy_additive_measurable_linear`. -/
theorem exists_isSolution_not_measurable :
    ∃ E : ℝ → ℝ, IsSolution E ∧ ¬ Measurable E := by
  classical
  obtain ⟨a0, hadd0, hnl0⟩ := CstarFlow.exists_additive_not_linear
  -- normalize the additive function so that it vanishes at `1`
  set a : ℝ → ℝ := fun x => a0 x - a0 1 * x with ha
  have hadd : ∀ x y, a (x + y) = a x + a y := by
    intro x y; simp only [ha]; rw [hadd0 x y]; ring
  have ha1 : a 1 = 0 := by simp [ha]
  have hnl : ¬ ∃ c, ∀ x, a x = c * x := by
    rintro ⟨c, hc⟩
    refine hnl0 ⟨c + a0 1, fun x => ?_⟩
    have hx := hc x; simp only [ha] at hx; linear_combination hx
  -- `a` is `1`-periodic and non-measurable
  have hper : Function.Periodic a 1 := by
    intro t; rw [hadd t 1, ha1, add_zero]
  have hnmeas : ¬ Measurable a := by
    intro hmeas
    exact hnl ⟨a 1, CstarFlow.cauchy_additive_measurable_linear a hadd hmeas⟩
  -- the corresponding solution is non-measurable
  refine ⟨fun v => v ^ 2 * a (Real.logb 2 v), isSolution_of_periodic a hper, ?_⟩
  intro hEmeas
  apply hnmeas
  have h2 : Measurable (fun t : ℝ => (2 : ℝ) ^ t) := (continuous_rpow_base (by norm_num)).measurable
  have h4 : Measurable (fun t : ℝ => (4 : ℝ) ^ t) := (continuous_rpow_base (by norm_num)).measurable
  have hcomp : Measurable
      (fun t : ℝ => ((2 : ℝ) ^ t) ^ 2 * a (Real.logb 2 ((2 : ℝ) ^ t)) / (4 : ℝ) ^ t) :=
    (hEmeas.comp h2).div h4
  have hgoal :
      (fun t : ℝ => ((2 : ℝ) ^ t) ^ 2 * a (Real.logb 2 ((2 : ℝ) ^ t)) / (4 : ℝ) ^ t) = a := by
    funext t
    have hlog : Real.logb 2 ((2 : ℝ) ^ t) = t := Real.logb_rpow (by norm_num) (by norm_num)
    have hne : ((2 : ℝ) ^ t) ^ 2 ≠ 0 := by positivity
    rw [hlog, four_rpow_eq t, mul_comm (((2 : ℝ) ^ t) ^ 2) (a t), mul_div_assoc, div_self hne,
      mul_one]
  rwa [hgoal] at hcomp

The non-measurability of $a$ comes from the measurable additive theorem CstarFlow.cauchy_additive_measurable_linear: a measurable additive map equals $a(1)\,x=0$ , contradicting non-linearity. Non-measurability of $E$ is then transported back to $a$ via $a(t)=E(2^t)/4^t$ . #print axioms exists_isSolution_not_measurable confirms the expected dependence on Classical.choice.

Summary¶

Hypothesis on $E$	Solutions of $E(2v)=4E(v)$ , $v>0$
none	$E(v)=v^2P(\log_2 v)$ , $P$ any 1-periodic function
measurable	$E(v)=v^2P(\log_2 v)$ , $P$ measurable 1-periodic (still infinite-dimensional)
continuous	$E(v)=v^2P(\log_2 v)$ , $P$ continuous 1-periodic (e.g. $v^2\cos(2\pi\log_2 v)$ )
$E=cv^2$	exactly $P\equiv c$ constant

The single relation $E(2v)=4E(v)$ fixes the power ( $v^2$ ) but leaves a full log-periodic gauge free; only an additional incommensurable scale, together with measurability, reduces the answer to the one-parameter family $cv^2$ .

The Scaling Functional Equation E(2v)=4E(v)

Iterating the equation¶

Reduction to a periodic gauge¶

The general solution¶

Classification by regularity¶

Rigid solutions cv2cv^2cv2¶

Measurable and continuous solutions: regularity is not enough¶

Non-measurable solutions¶

Summary¶

Rigid solutions $cv^2$ ¶