Encyclopedia Information Information Local Cache Jcost Symmetry Forces Geometric Boundary

ARTICLE 3 claims 3 theorems

Information Local Cache Jcost Symmetry Forces Geometric Boundary

A proved symmetry in a cost function forces the boundary between two storage levels to sit at the geometric mean of their sizes.

Verify this page

The geometric boundary

When a system stores frequently used items close and rarely used items far, it faces a boundary question: at what distance does an item stop being worth the cost of storing it in the fast cache? The theorem Jcost_symmetry_forces_geometric_boundary answers that question for one specific cost function. It states that if the cost of a ratio equals the cost of its reciprocal, and the boundary balances the two costs, then the boundary distance d must satisfy either d/D = D'/d or d/D = (D'/d)⁻¹. The first solution is the geometric mean: d² = D·D'.

The cost function in question is J(x) = (x + 1/x)/2 − 1, which measures the price of a ratio x between two quantities. It has the symmetry J(x) = J(1/x), meaning the cost of overshooting a target equals the cost of undershooting by the same factor. The theorem takes that symmetry as its only input. It does not assume anything about what the items are, what the distances mean, or why the cost function has that form. Those questions belong to other results in the framework's machine-checked library of formal theorems.

The theorem's conclusion is a disjunction, not a single answer. It allows two possible boundary positions: the geometric mean, or the reciprocal of that mean. The first is the one the framework's formal development identifies as the optimal partition point, because it equalizes the two costs. The second is its mirror image, which arises from the same symmetry. The theorem itself does not select between them; that selection comes from an additional argument about which solution corresponds to a meaningful boundary.

The result matters because it turns a geometric intuition into a proved statement. The intuition is that a boundary should sit where the cost of being too close equals the cost of being too far. The theorem shows that this balance point, under the symmetry condition, is exactly the geometric mean. It is a small, clean result, but it is the kind of result that a larger theory can build on without rechecking the arithmetic each time.

What the theorem does not claim is just as important. It does not claim that the geometric mean is always the right boundary, only that it is one of two solutions to the balance equation. It does not claim that any real cache, memory system, or neural network actually uses this boundary. It does not claim that the cost function J is the only possible cost function, or that the symmetry condition is forced. Those are separate claims, made elsewhere and with their own evidence. This theorem is a conditional statement: if you have the symmetry and the balance, then you have the geometric mean.

The theorem also does not establish the Fibonacci recurrence that appears in the same file. That recurrence, K(ℓ+2) = K(ℓ+1) + K(ℓ), is a separate result derived from the geometric boundary. The theorem here is the boundary itself, not the sequence that follows from it. A reader who wants to know why cache levels grow like Fibonacci numbers must look at the next theorem in the chain, not this one.

THEOREM Jcost_symmetry_forces_geometric_boundary · IndisputableMonolith/Information/LocalCache.lean
Jcost_symmetry_forces_geometric_boundary · IndisputableMonolith/Information/LocalCache.lean:130 
/-- **LEMMA (Optimal Partition)**:
For J-cost with symmetry J(x) = J(1/x), the optimal boundary between
cache levels balances the "overshoot" cost J(d/D_ℓ) against the
"undershoot" cost J(D_{ℓ-1}/d). By symmetry, the optimal point
is where d/D_ℓ = D_{ℓ-1}/d, i.e., d² = D_ℓ · D_{ℓ-1}.

This geometric-mean boundary gives the partition:
  K_{ℓ+1} - K_ℓ = K_{ℓ-1}  (the Fibonacci recurrence). -/
theorem Jcost_symmetry_forces_geometric_boundary
    (d D_ℓ D_prev : ℝ) (hd : 0 < d) (hD : 0 < D_ℓ) (hDp : 0 < D_prev)
    (hbalance : Jcost (d / D_ℓ) = Jcost (D_prev / d)) :
    -- J-symmetry: Jcost(x) = Jcost(1/x), so balance ⟺ d/D_ℓ = d/D_prev or d/D_ℓ = D_prev/d
    -- The non-trivial solution is d² = D_ℓ · D_prev (geometric mean)
    d / D_ℓ = D_prev / d ∨ d / D_ℓ = (D_prev / d)⁻¹ := by
  -- From J(a) = J(b), either a = b or a = 1/b (by J-symmetry + injectivity on (0,1] ∪ [1,∞))
  -- We leave both branches as the disjunction
  let a : ℝ := d / D_ℓ
  let b : ℝ := D_prev / d
  have ha : 0 < a := by
    unfold a
    exact div_pos hd hD
  have hb : 0 < b := by
    unfold b
    exact div_pos hDp hd
  have ha0 : a ≠ 0 := ne_of_gt ha
  have hb0 : b ≠ 0 := ne_of_gt hb
  have hab : Jcost a = Jcost b := by
    simpa [a, b] using hbalance
  rw [Jcost_eq_sq ha0, Jcost_eq_sq hb0] at hab
  have hcross : (a - 1) ^ 2 * b = (b - 1) ^ 2 * a := by
    have h2a : (2 * a) ≠ 0 := by positivity
    have h2b : (2 * b) ≠ 0 := by positivity
    have htmp := hab
    field_simp [h2a, h2b] at htmp
    linarith
  have hfactor : (a - b) * (a * b - 1) = 0 := by
    nlinarith [hcross]
  have hsplit : a - b = 0 ∨ a * b - 1 = 0 := mul_eq_zero.mp hfactor
  cases hsplit with
  | inl habEq =>
      left
      linarith
  | inr habInv =>
      right
      have hmul : a * b = 1 := by linarith [habInv]
      have hInv : a = b⁻¹ := by
        have hInv' : a⁻¹ = b := inv_eq_of_mul_eq_one_right hmul
        exact (inv_eq_iff_eq_inv).1 hInv'
      simpa [a, b] using hInv
THEOREM Jcost_symmetry_forces_geometric_boundary · IndisputableMonolith/Information/LocalCache.lean
Jcost_symmetry_forces_geometric_boundary · IndisputableMonolith/Information/LocalCache.lean:130 
/-- **LEMMA (Optimal Partition)**:
For J-cost with symmetry J(x) = J(1/x), the optimal boundary between
cache levels balances the "overshoot" cost J(d/D_ℓ) against the
"undershoot" cost J(D_{ℓ-1}/d). By symmetry, the optimal point
is where d/D_ℓ = D_{ℓ-1}/d, i.e., d² = D_ℓ · D_{ℓ-1}.

This geometric-mean boundary gives the partition:
  K_{ℓ+1} - K_ℓ = K_{ℓ-1}  (the Fibonacci recurrence). -/
theorem Jcost_symmetry_forces_geometric_boundary
    (d D_ℓ D_prev : ℝ) (hd : 0 < d) (hD : 0 < D_ℓ) (hDp : 0 < D_prev)
    (hbalance : Jcost (d / D_ℓ) = Jcost (D_prev / d)) :
    -- J-symmetry: Jcost(x) = Jcost(1/x), so balance ⟺ d/D_ℓ = d/D_prev or d/D_ℓ = D_prev/d
    -- The non-trivial solution is d² = D_ℓ · D_prev (geometric mean)
    d / D_ℓ = D_prev / d ∨ d / D_ℓ = (D_prev / d)⁻¹ := by
  -- From J(a) = J(b), either a = b or a = 1/b (by J-symmetry + injectivity on (0,1] ∪ [1,∞))
  -- We leave both branches as the disjunction
  let a : ℝ := d / D_ℓ
  let b : ℝ := D_prev / d
  have ha : 0 < a := by
    unfold a
    exact div_pos hd hD
  have hb : 0 < b := by
    unfold b
    exact div_pos hDp hd
  have ha0 : a ≠ 0 := ne_of_gt ha
  have hb0 : b ≠ 0 := ne_of_gt hb
  have hab : Jcost a = Jcost b := by
    simpa [a, b] using hbalance
  rw [Jcost_eq_sq ha0, Jcost_eq_sq hb0] at hab
  have hcross : (a - 1) ^ 2 * b = (b - 1) ^ 2 * a := by
    have h2a : (2 * a) ≠ 0 := by positivity
    have h2b : (2 * b) ≠ 0 := by positivity
    have htmp := hab
    field_simp [h2a, h2b] at htmp
    linarith
  have hfactor : (a - b) * (a * b - 1) = 0 := by
    nlinarith [hcross]
  have hsplit : a - b = 0 ∨ a * b - 1 = 0 := mul_eq_zero.mp hfactor
  cases hsplit with
  | inl habEq =>
      left
      linarith
  | inr habInv =>
      right
      have hmul : a * b = 1 := by linarith [habInv]
      have hInv : a = b⁻¹ := by
        have hInv' : a⁻¹ = b := inv_eq_of_mul_eq_one_right hmul
        exact (inv_eq_iff_eq_inv).1 hInv'
      simpa [a, b] using hInv
THEOREM Jcost_symmetry_forces_geometric_boundary · IndisputableMonolith/Information/LocalCache.lean
Jcost_symmetry_forces_geometric_boundary · IndisputableMonolith/Information/LocalCache.lean:130 
/-- **LEMMA (Optimal Partition)**:
For J-cost with symmetry J(x) = J(1/x), the optimal boundary between
cache levels balances the "overshoot" cost J(d/D_ℓ) against the
"undershoot" cost J(D_{ℓ-1}/d). By symmetry, the optimal point
is where d/D_ℓ = D_{ℓ-1}/d, i.e., d² = D_ℓ · D_{ℓ-1}.

This geometric-mean boundary gives the partition:
  K_{ℓ+1} - K_ℓ = K_{ℓ-1}  (the Fibonacci recurrence). -/
theorem Jcost_symmetry_forces_geometric_boundary
    (d D_ℓ D_prev : ℝ) (hd : 0 < d) (hD : 0 < D_ℓ) (hDp : 0 < D_prev)
    (hbalance : Jcost (d / D_ℓ) = Jcost (D_prev / d)) :
    -- J-symmetry: Jcost(x) = Jcost(1/x), so balance ⟺ d/D_ℓ = d/D_prev or d/D_ℓ = D_prev/d
    -- The non-trivial solution is d² = D_ℓ · D_prev (geometric mean)
    d / D_ℓ = D_prev / d ∨ d / D_ℓ = (D_prev / d)⁻¹ := by
  -- From J(a) = J(b), either a = b or a = 1/b (by J-symmetry + injectivity on (0,1] ∪ [1,∞))
  -- We leave both branches as the disjunction
  let a : ℝ := d / D_ℓ
  let b : ℝ := D_prev / d
  have ha : 0 < a := by
    unfold a
    exact div_pos hd hD
  have hb : 0 < b := by
    unfold b
    exact div_pos hDp hd
  have ha0 : a ≠ 0 := ne_of_gt ha
  have hb0 : b ≠ 0 := ne_of_gt hb
  have hab : Jcost a = Jcost b := by
    simpa [a, b] using hbalance
  rw [Jcost_eq_sq ha0, Jcost_eq_sq hb0] at hab
  have hcross : (a - 1) ^ 2 * b = (b - 1) ^ 2 * a := by
    have h2a : (2 * a) ≠ 0 := by positivity
    have h2b : (2 * b) ≠ 0 := by positivity
    have htmp := hab
    field_simp [h2a, h2b] at htmp
    linarith
  have hfactor : (a - b) * (a * b - 1) = 0 := by
    nlinarith [hcross]
  have hsplit : a - b = 0 ∨ a * b - 1 = 0 := mul_eq_zero.mp hfactor
  cases hsplit with
  | inl habEq =>
      left
      linarith
  | inr habInv =>
      right
      have hmul : a * b = 1 := by linarith [habInv]
      have hInv : a = b⁻¹ := by
        have hInv' : a⁻¹ = b := inv_eq_of_mul_eq_one_right hmul
        exact (inv_eq_iff_eq_inv).1 hInv'
      simpa [a, b] using hInv

What this page does not claim

The theorem does not claim the geometric mean is always the correct boundary, only that it is one of two solutions to the balance equation. The theorem does not claim that any real cache or memory system actually uses this boundary. The theorem does not establish the Fibonacci recurrence, which is a separate result derived from the geometric boundary.

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/Information/LocalCache.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