Cosmology Polarized Birth Interface Cost Run Cost Growth

The growth of the cost

A polarized birth field assigns each cell a charge of +1, 0, or -1. Adjacent cells of equal charge are carried (the engine moves them together), while adjacent cells of different charge form an interface (the boundary between charge regions). The framework's recognition cost, the forced price J(x) = (x + x⁻¹)/2 - 1, is evaluated at the gap in the golden-ratio ladder between two cells' charges. A carried edge spans zero rungs, so it costs J(1) = 0 exactly. An interface edge spans one rung, so it costs J(φ) = (√5 - 2)/2, a positive number.

Because carried edges cost nothing, the entire cost of the field is the interface count times J(φ). In a 2D diamond of time t, the total cost is (8t - 4) · J(φ). In a 3D octahedron, it is (8t² - 8t + 4) · J(φ). The declaration runCost_growth subtracts the cost at t = 1 to isolate the growth from the initial seed. For the diamond, the growth from the first step to time T is (8T - 8) · J(φ). For the octahedron, it is (8T² - 8T) · J(φ).

The pattern is the point. In the diamond, cost grows linearly with the side length, which is the size of the boundary. In the octahedron, it grows quadratically, again matching the surface area of the boundary. The volume inside, the bulk that the engine carries for free, never appears in the cost. This is the literal cost-unit statement of the framework's compute-watch law: recognition activity scales with the codimension-1 interface, not with the bulk volume.

These are theorems over the real and natural numbers, with no sorry and only the three standard axioms (propext, Classical.choice, Quot.sound). The framework's library of formal theorems proves the formulas for both shapes. The result is a sharp account of how the engine's forced cost behaves as a polarized birth field grows.

/-- A zero-rung gap (a carried, monochromatic edge) costs nothing: `J(φ^0) = J(1) = 0`. -/
lemma Jpow_zero : Jpow 0 = 0 := by
  rw [Jpow, zpow_zero, Cost.Jcost_unit0]

/-- `J(φ) > 0`: a forced interface distinction has a genuine, strictly positive recognition cost.
`J(φ) = (φ - 1)²/(2φ) = (√5 - 2)/2`. -/
lemma Jcost_phi_pos : 0 < Cost.Jcost Constants.phi := by
  rw [Cost.Jcost_eq_sq Constants.phi_ne_zero]
  apply div_pos
  · have hne : Constants.phi - 1 ≠ 0 := sub_ne_zero.mpr Constants.phi_ne_one
    positivity
  · have := Constants.phi_pos; linarith

/-- The total cost in real-multiplication form, `(8t - 4) * J(φ)` (`t ≥ 1`). -/
theorem totalCost_mul (t : ℕ) (ht : 1 ≤ t) :
    totalCost t = ((8 * t - 4 : ℕ) : ℝ) * Cost.Jcost Constants.phi := by
  rw [totalCost_card t ht, nsmul_eq_mul]

/-- The total cost in real-multiplication form, `(8t - 4) * J(φ)` (`t ≥ 1`). -/
theorem totalCost_mul (t : ℕ) (ht : 1 ≤ t) :
    totalCost t = ((8 * t - 4 : ℕ) : ℝ) * Cost.Jcost Constants.phi := by
  rw [totalCost_card t ht, nsmul_eq_mul]

/-- **The run-total recognition cost over a full forward run** from radius `1` to `T` is exactly
`8(T - 1) • J(φ)`. The cost the engine posts to grow the whole world is `Θ(T)`, strictly
sub-extensive against the brute-force volume-times-ticks `Θ(T³)`: the compute-watch law in cost
units, integrated over the run. -/
theorem runCost_growth (T : ℕ) (hT : 1 ≤ T) :
    totalCost T - totalCost 1 = ((8 * T - 8 : ℕ) : ℝ) * Cost.Jcost Constants.phi := by
  rw [totalCost_mul T hT, totalCost_mul 1 le_rfl]
  have h4 : 4 ≤ 8 * T := by omega
  have h8 : 8 ≤ 8 * T := by omega
  have e1 : ((8 * T - 4 : ℕ) : ℝ) = 8 * (T : ℝ) - 4 := by
    rw [Nat.cast_sub h4]; push_cast; ring
  have e2 : ((8 * 1 - 4 : ℕ) : ℝ) = 4 := by norm_num
  have e3 : ((8 * T - 8 : ℕ) : ℝ) = 8 * (T : ℝ) - 8 := by
    rw [Nat.cast_sub h8]; push_cast; ring
  rw [e1, e2, e3]; ring

/-- **The run-total recognition cost over a full forward run** from radius `1` to `T` is exactly
`8(T - 1) • J(φ)`. The cost the engine posts to grow the whole world is `Θ(T)`, strictly
sub-extensive against the brute-force volume-times-ticks `Θ(T³)`: the compute-watch law in cost
units, integrated over the run. -/
theorem runCost_growth (T : ℕ) (hT : 1 ≤ T) :
    totalCost T - totalCost 1 = ((8 * T - 8 : ℕ) : ℝ) * Cost.Jcost Constants.phi := by
  rw [totalCost_mul T hT, totalCost_mul 1 le_rfl]
  have h4 : 4 ≤ 8 * T := by omega
  have h8 : 8 ≤ 8 * T := by omega
  have e1 : ((8 * T - 4 : ℕ) : ℝ) = 8 * (T : ℝ) - 4 := by
    rw [Nat.cast_sub h4]; push_cast; ring
  have e2 : ((8 * 1 - 4 : ℕ) : ℝ) = 4 := by norm_num
  have e3 : ((8 * T - 8 : ℕ) : ℝ) = 8 * (T : ℝ) - 8 := by
    rw [Nat.cast_sub h8]; push_cast; ring
  rw [e1, e2, e3]; ring

What this page does not claim

This does not claim that the cost formula applies to any physical system outside the framework's model. This does not claim that the cost of carried edges is zero in any other cost function. This does not claim that the growth law is derived from the physical recognition-to-linking bridge, which remains open.

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/PolarizedBirthInterfaceCost.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: