Encyclopedia Cost Cost Aczel Proof

ARTICLE 3 claims 3 theorems

Cost Aczel Proof

A classical theorem from 1966, machine-checked, is the hidden engine that turns a simple continuity assumption into the full force of the cost function.

Verify this page

The smoothness theorem

The d'Alembert functional equation, H(t + u) + H(t - u) = 2·H(t)·H(u), is a symmetry condition that appears across mathematics and physics. It asks for functions whose value at a sum and difference of two points is determined by the product of their individual values. The classical question, answered by János Aczél in his 1966 Lectures on Functional Equations, is: what must such a function look like if it is merely continuous?

Aczél's answer is a smoothness theorem. Any continuous solution with H(0) = 1 is not just continuous but infinitely differentiable, and in fact real analytic, meaning it can be written as a convergent power series. The proof proceeds in three stages. First, an integration bootstrap: a continuous function can be integrated to produce an antiderivative, and the functional equation forces that antiderivative to be differentiable, which in turn forces the original function to be smoother. Iterating this argument shows the solution is C^∞. Second, differentiating the functional equation twice yields an ordinary differential equation, H'' = c·H, with c = H''(0). Third, solving that ODE gives the complete classification: the only continuous solutions are the constant 1, the hyperbolic cosine cosh(α·x), and the ordinary cosine cos(α·x), for some real parameter α.

In Recognition Science, this theorem is the load-bearing wall behind the derivation of the cost function. The framework models recognition as a forced cost, and the cost function J(x) = (x + 1/x)/2 - 1 is proved to be the unique function satisfying five plain conditions. One of those conditions is a composition law that, after a logarithmic change of variables, becomes exactly the d'Alembert equation. The Aczél theorem is what upgrades the continuity assumption in that setting to full analyticity, and the classification it provides is what pins down the unique form of the cost.

The framework's machine-checked library of formal theorems contains a complete, verified proof of Aczél's classification. The theorem dAlembert_classification states that any continuous H with H(0) = 1 satisfying the equation is exactly one of the three forms above. The proof in the library follows the same three-phase structure: integration bootstrap to C^∞, derivation of the ODE, and then uniqueness arguments for each branch of the trichotomy on the constant c. The final result is packaged as an instance of the AczelSmoothnessPackage, ready to be used as a black box by later developments.

What this establishes in plain language is that a single, mild assumption of continuity, combined with a natural symmetry condition, has enormous consequences. There is no room for exotic or pathological solutions. The functional equation is so rigid that it forces the solution to be one of three familiar, well-behaved functions. For the framework, this means the cost function is not an arbitrary choice but a mathematical inevitability, once the five conditions are accepted. The Aczél theorem is the reason the framework can claim uniqueness with confidence.

THEOREM dAlembert_classification · IndisputableMonolith/Cost/AczelProof.lean
dAlembert_classification · IndisputableMonolith/Cost/AczelProof.lean:291 
/-- **Aczél–Kannappan classification of the d'Alembert functional equation.**

Any continuous H : ℝ → ℝ with H(0) = 1 satisfying
  H(t+u) + H(t−u) = 2·H(t)·H(u)
is exactly one of:
* the constant 1,
* `Real.cosh (α·)` for some α ∈ ℝ, or
* `Real.cos  (α·)` for some α ∈ ℝ.

Proof: continuity ⇒ C^∞ via the integration bootstrap (`dAlembert_contDiff_smooth`);
C² + d'Alembert ⇒ H'' = c·H with c = H''(0) (`dAlembert_to_ODE_general`);
ODE uniqueness in each branch of the trichotomy on c gives the explicit formula. -/
theorem dAlembert_classification (H : ℝ → ℝ)
    (h_one : H 0 = 1) (h_cont : Continuous H)
    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
    (∀ x, H x = 1) ∨
    (∃ α : ℝ, ∀ x, H x = Real.cosh (α * x)) ∨
    (∃ α : ℝ, ∀ x, H x = Real.cos (α * x)) := by
  have h_sm : ContDiff ℝ smooth H := dAlembert_contDiff_smooth H h_one h_cont h_dAl
  have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_sm) 2
  have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  have h_H'0 : deriv H 0 = 0 :=
    even_deriv_at_zero H (dAlembert_even H h_one h_dAl) hDiff.differentiableAt
  have h_ode := dAlembert_to_ODE_general H h_sm h_dAl
  set c := deriv (deriv H) 0 with hc_def
  have hDD : Differentiable ℝ (deriv H) := by
    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
    exact (contDiff_succ_iff_deriv.mp h2).2.2.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  by_cases hc_pos : 0 < c
  · -- c > 0: H = cosh(√c · t)
    right; left; refine ⟨Real.sqrt c, ?_⟩
    have hsc_ne : Real.sqrt c ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hc_pos)
    let g : ℝ → ℝ := fun s => H (s / Real.sqrt c)
    have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c) (Real.sqrt c)⁻¹ s := fun s => by
      have := (hasDerivAt_id s).div_const (Real.sqrt c); simp only [id, one_div] at this; exact this
    have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹) s :=
      fun s => (hDiff _).hasDerivAt.comp s (h_div s)
    have hg_ode : ∀ t, deriv (deriv g) t = g t := by
      intro s
      have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ :=
        funext fun s => (hg_d s).deriv
      have h_dd_g : HasDerivAt (deriv g)
          ((deriv (deriv H) (s / Real.sqrt c) * (Real.sqrt c)⁻¹) * (Real.sqrt c)⁻¹) s := by
        rw [hg1]
        exact ((hDD (s / Real.sqrt c)).hasDerivAt.comp s (h_div s)).mul_const _
      rw [h_dd_g.deriv, h_ode (s / Real.sqrt c)]
      simp only [g]
      rw [show c * H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ =
          H (s / Real.sqrt c) * (c * ((Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹)) from by ring,
          show (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ = (Real.sqrt c * Real.sqrt c)⁻¹ from
            (mul_inv_rev _ _).symm,
          Real.mul_self_sqrt (le_of_lt hc_pos),
          mul_inv_cancel₀ (ne_of_gt hc_pos), mul_one]
    intro t
    have := ode_cosh_uniqueness_contdiff g (h2.comp (contDiff_id.div_const _))
      hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
      (Real.sqrt c * t)
    simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
  · by_cases hc_neg : c < 0
    · -- c < 0: H = cos(√(−c) · t)
      right; right; refine ⟨Real.sqrt (-c), ?_⟩
      set c' := -c
      have hsc_ne : Real.sqrt c' ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr (neg_pos.mpr hc_neg))
      let g : ℝ → ℝ := fun s => H (s / Real.sqrt c')
      have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c') (Real.sqrt c')⁻¹ s := fun s => by
        have := (hasDerivAt_id s).div_const (Real.sqrt c'); simp only [id, one_div] at this; exact this
      have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹) s :=
        fun s => (hDiff _).hasDerivAt.comp s (h_div s)
      have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
        intro s
        have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹ :=
          funext fun s => (hg_d s).deriv
        have h_dd_g : HasDerivAt (deriv g)
            ((deriv (deriv H) (s / Real.sqrt c') * (Real.sqrt c')⁻¹) * (Real.sqrt c')⁻¹) s := by
          rw [hg1]
          exact ((hDD (s / Real.sqrt c')).hasDerivAt.comp s (h_div s)).mul_const _
        rw [h_dd_g.deriv, h_ode (s / Real.sqrt c')]
        simp only [g, c']
        rw [show c * H (s / Real.sqrt (-c)) * (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ =
            H (s / Real.sqrt (-c)) * (c * ((Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹)) from by ring,
            show (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ = (Real.sqrt (-c) * Real.sqrt (-c))⁻¹ from
              (mul_inv_rev _ _).symm,
            Real.mul_self_sqrt (le_of_lt (neg_pos.mpr hc_neg)),
            show c * (-c)⁻¹ = -(1 : ℝ) from by
              have hc_ne : c ≠ 0 := ne_of_lt hc_neg
              field_simp]
        ring
      intro t
      have := ode_cos_uniqueness g (h2.comp (contDiff_id.div_const _))
        hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
        (Real.sqrt c' * t)
      simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
    · -- c = 0: H ≡ 1
      left
      have hc0 : c = 0 := le_antisymm (not_lt.mp hc_pos) (not_lt.mp hc_neg)
      have h_H'_zero : ∀ t, deriv H t = 0 := by
        have := is_const_of_deriv_eq_zero hDD (fun t => by rw [h_ode t, hc0, zero_mul])
        intro t; have := this t 0; simp [h_H'0] at this; exact this
      intro t
      have := is_const_of_deriv_eq_zero hDiff h_H'_zero t 0
      simp [h_one] at this; exact this
THEOREM dAlembert_contDiff_smooth · dAlembert_to_ODE_general · IndisputableMonolith/Cost/AczelProof.lean
dAlembert_contDiff_smooth · IndisputableMonolith/Cost/AczelProof.lean:165 
private theorem dAlembert_contDiff_smooth (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H)
    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
    ContDiff ℝ smooth H :=
  contDiff_infty.mpr (dAlembert_contDiff_nat H h_one h_cont h_dAl)
dAlembert_to_ODE_general · IndisputableMonolith/Cost/AczelProof.lean:172 
private theorem dAlembert_to_ODE_general (H : ℝ → ℝ)
    (h_smooth : ContDiff ℝ smooth H)
    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
    ∀ t, deriv (deriv H) t = deriv (deriv H) 0 * H t := by
  have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_smooth) 2
  have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  have hCDiff1_H' : ContDiff ℝ 1 (deriv H) := by
    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
    rw [contDiff_succ_iff_deriv] at h2; exact h2.2.2
  have hDiffDeriv : Differentiable ℝ (deriv H) :=
    hCDiff1_H'.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  have hsh_add : ∀ (s v : ℝ), HasDerivAt (fun u => s + u) (1 : ℝ) v := fun s v => by
    have h := (hasDerivAt_id v).add_const s; simp only [id] at h
    rwa [show (fun u : ℝ => u + s) = fun u => s + u from funext fun u => add_comm u s] at h
  have hsh_sub : ∀ (s v : ℝ), HasDerivAt (fun u => s - u) (-1 : ℝ) v := fun s v => by
    have h1 : HasDerivAt (fun u : ℝ => -u) (-1 : ℝ) v := by
      have := (hasDerivAt_id v).neg; simp only [id] at this; exact this
    have h2 := h1.const_add s
    rwa [show (fun u : ℝ => s + -u) = fun u => s - u from funext fun u => by ring] at h2
  intro t
  have h_feq : (fun u => H (t + u) + H (t - u)) = (fun u => 2 * H t * H u) :=
    funext (h_dAl t)
  have key : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 =
             deriv (deriv (fun u => 2 * H t * H u)) 0 :=
    congr_arg (fun f => deriv (deriv f) 0) h_feq
  have lhs_eq : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 =
      2 * deriv (deriv H) t := by
    have h_plus : ∀ v, HasDerivAt (fun u => H (t + u)) (deriv H (t + v)) v := fun v => by
      have h := ((hDiff (t + v)).hasDerivAt).comp v (hsh_add t v)
      simp only [mul_one, Function.comp_def] at h; exact h
    have h_minus : ∀ v, HasDerivAt (fun u => H (t - u)) (-deriv H (t - v)) v := fun v => by
      have hcomp := ((hDiff (t - v)).hasDerivAt).comp v (hsh_sub t v)
      simp only [mul_neg, mul_one, Function.comp_apply] at hcomp; exact hcomp
    have hfirst : deriv (fun u => H (t + u) + H (t - u)) =
        fun v => deriv H (t + v) - deriv H (t - v) := funext fun v => by
      have h12 := ((h_plus v).add (h_minus v)).deriv
      rw [show (fun u => H (t + u)) + (fun u => H (t - u)) =
          fun u => H (t + u) + H (t - u) from by ext u; rfl] at h12; linarith [h12]
    have hd2p : HasDerivAt (fun v => deriv H (t + v)) (deriv (deriv H) t) 0 := by
      have := ((hDiffDeriv (t + 0)).hasDerivAt).comp 0 (hsh_add t 0)
      simpa using this
    have hd2m : HasDerivAt (fun v => deriv H (t - v)) (-deriv (deriv H) t) 0 := by
      have := ((hDiffDeriv (t - 0)).hasDerivAt).comp 0 (hsh_sub t 0)
      simpa using this
    rw [congr_fun (congr_arg deriv hfirst) 0,
        show (fun v => deriv H (t + v) - deriv H (t - v)) =
          (fun v => deriv H (t + v)) - (fun v => deriv H (t - v)) from rfl]
    linarith [(hd2p.sub hd2m).deriv]
  have rhs_eq : deriv (deriv (fun u => 2 * H t * H u)) 0 =
      2 * H t * deriv (deriv H) 0 := by
    have hf : deriv (fun u => 2 * H t * H u) = fun v => 2 * H t * deriv H v :=
      funext fun v => ((hDiff v).hasDerivAt.const_mul (2 * H t)).deriv
    rw [congr_fun (congr_arg deriv hf) 0, ((hDiffDeriv 0).hasDerivAt.const_mul (2 * H t)).deriv]
  rw [lhs_eq, rhs_eq] at key; linarith
THEOREM dAlembert_classification · IndisputableMonolith/Cost/AczelProof.lean
dAlembert_classification · IndisputableMonolith/Cost/AczelProof.lean:291 
/-- **Aczél–Kannappan classification of the d'Alembert functional equation.**

Any continuous H : ℝ → ℝ with H(0) = 1 satisfying
  H(t+u) + H(t−u) = 2·H(t)·H(u)
is exactly one of:
* the constant 1,
* `Real.cosh (α·)` for some α ∈ ℝ, or
* `Real.cos  (α·)` for some α ∈ ℝ.

Proof: continuity ⇒ C^∞ via the integration bootstrap (`dAlembert_contDiff_smooth`);
C² + d'Alembert ⇒ H'' = c·H with c = H''(0) (`dAlembert_to_ODE_general`);
ODE uniqueness in each branch of the trichotomy on c gives the explicit formula. -/
theorem dAlembert_classification (H : ℝ → ℝ)
    (h_one : H 0 = 1) (h_cont : Continuous H)
    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
    (∀ x, H x = 1) ∨
    (∃ α : ℝ, ∀ x, H x = Real.cosh (α * x)) ∨
    (∃ α : ℝ, ∀ x, H x = Real.cos (α * x)) := by
  have h_sm : ContDiff ℝ smooth H := dAlembert_contDiff_smooth H h_one h_cont h_dAl
  have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_sm) 2
  have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  have h_H'0 : deriv H 0 = 0 :=
    even_deriv_at_zero H (dAlembert_even H h_one h_dAl) hDiff.differentiableAt
  have h_ode := dAlembert_to_ODE_general H h_sm h_dAl
  set c := deriv (deriv H) 0 with hc_def
  have hDD : Differentiable ℝ (deriv H) := by
    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
    exact (contDiff_succ_iff_deriv.mp h2).2.2.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  by_cases hc_pos : 0 < c
  · -- c > 0: H = cosh(√c · t)
    right; left; refine ⟨Real.sqrt c, ?_⟩
    have hsc_ne : Real.sqrt c ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hc_pos)
    let g : ℝ → ℝ := fun s => H (s / Real.sqrt c)
    have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c) (Real.sqrt c)⁻¹ s := fun s => by
      have := (hasDerivAt_id s).div_const (Real.sqrt c); simp only [id, one_div] at this; exact this
    have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹) s :=
      fun s => (hDiff _).hasDerivAt.comp s (h_div s)
    have hg_ode : ∀ t, deriv (deriv g) t = g t := by
      intro s
      have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ :=
        funext fun s => (hg_d s).deriv
      have h_dd_g : HasDerivAt (deriv g)
          ((deriv (deriv H) (s / Real.sqrt c) * (Real.sqrt c)⁻¹) * (Real.sqrt c)⁻¹) s := by
        rw [hg1]
        exact ((hDD (s / Real.sqrt c)).hasDerivAt.comp s (h_div s)).mul_const _
      rw [h_dd_g.deriv, h_ode (s / Real.sqrt c)]
      simp only [g]
      rw [show c * H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ =
          H (s / Real.sqrt c) * (c * ((Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹)) from by ring,
          show (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ = (Real.sqrt c * Real.sqrt c)⁻¹ from
            (mul_inv_rev _ _).symm,
          Real.mul_self_sqrt (le_of_lt hc_pos),
          mul_inv_cancel₀ (ne_of_gt hc_pos), mul_one]
    intro t
    have := ode_cosh_uniqueness_contdiff g (h2.comp (contDiff_id.div_const _))
      hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
      (Real.sqrt c * t)
    simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
  · by_cases hc_neg : c < 0
    · -- c < 0: H = cos(√(−c) · t)
      right; right; refine ⟨Real.sqrt (-c), ?_⟩
      set c' := -c
      have hsc_ne : Real.sqrt c' ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr (neg_pos.mpr hc_neg))
      let g : ℝ → ℝ := fun s => H (s / Real.sqrt c')
      have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c') (Real.sqrt c')⁻¹ s := fun s => by
        have := (hasDerivAt_id s).div_const (Real.sqrt c'); simp only [id, one_div] at this; exact this
      have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹) s :=
        fun s => (hDiff _).hasDerivAt.comp s (h_div s)
      have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
        intro s
        have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹ :=
          funext fun s => (hg_d s).deriv
        have h_dd_g : HasDerivAt (deriv g)
            ((deriv (deriv H) (s / Real.sqrt c') * (Real.sqrt c')⁻¹) * (Real.sqrt c')⁻¹) s := by
          rw [hg1]
          exact ((hDD (s / Real.sqrt c')).hasDerivAt.comp s (h_div s)).mul_const _
        rw [h_dd_g.deriv, h_ode (s / Real.sqrt c')]
        simp only [g, c']
        rw [show c * H (s / Real.sqrt (-c)) * (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ =
            H (s / Real.sqrt (-c)) * (c * ((Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹)) from by ring,
            show (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ = (Real.sqrt (-c) * Real.sqrt (-c))⁻¹ from
              (mul_inv_rev _ _).symm,
            Real.mul_self_sqrt (le_of_lt (neg_pos.mpr hc_neg)),
            show c * (-c)⁻¹ = -(1 : ℝ) from by
              have hc_ne : c ≠ 0 := ne_of_lt hc_neg
              field_simp]
        ring
      intro t
      have := ode_cos_uniqueness g (h2.comp (contDiff_id.div_const _))
        hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
        (Real.sqrt c' * t)
      simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
    · -- c = 0: H ≡ 1
      left
      have hc0 : c = 0 := le_antisymm (not_lt.mp hc_pos) (not_lt.mp hc_neg)
      have h_H'_zero : ∀ t, deriv H t = 0 := by
        have := is_const_of_deriv_eq_zero hDD (fun t => by rw [h_ode t, hc0, zero_mul])
        intro t; have := this t 0; simp [h_H'0] at this; exact this
      intro t
      have := is_const_of_deriv_eq_zero hDiff h_H'_zero t 0
      simp [h_one] at this; exact this

What this page does not claim

This page does not derive the cost function J(x) itself, only the smoothness and classification theorem that supports it. This page does not claim the Aczél theorem is original to Recognition Science; it is a classical result from 1966. This page does not claim the classification holds without the continuity assumption; discontinuous solutions exist.

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/Cost/AczelProof.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND