Encyclopedia Cosmology Cosmology Polarized Birth Interface Cost Interface Cost Card

ARTICLE 5 claims 5 theorems

Cosmology Polarized Birth Interface Cost Interface Cost Card

In a polarized birth field, carrying the bulk is free; only the boundary between charge regions is paid for.

Verify this page

The interface cost

The declaration interfaceCost_card establishes a precise accounting rule for a discrete spatial structure called a polarized birth field. The field assigns each cell a charge of +1, 0, or -1, and the framework's ledger, a discrete record of recognition events, posts a cost for every adjacency between two cells. The cost is not arbitrary: it is the forced function J(x) = (x + x⁻¹)/2 - 1, evaluated at the golden ratio φ raised to the difference in charges between the two cells.

Two facts make the accounting simple. A carried edge connects cells of equal charge, so the charge difference is zero, and J(φ⁰) = J(1) = 0 exactly. The bulk is carried for literally zero recognition cost. An interface edge connects a cell on the x = 0 spine to a cell at x = ±1, so the charges differ by exactly ±1, and the cost is J(φ) = (√5 - 2)/2 > 0, a genuine positive number. The theorem proves that the total cost of the entire field equals the interface cost alone, with the carried cost exactly zero.

In two dimensions, the diamond lattice at time step t has total cost (8t - 4) · J(φ). In three dimensions, the octahedron lattice has total cost (8t² - 8t + 4) · J(φ). The cost scales with the number of interface edges, which grows with the boundary area, not with the bulk volume. The framework reads this as a literal cost-unit statement of a compute-watch law: recognition activity is paid at the codimension-1 interface, while the interior is carried coarse for free.

THEOREM Jpow_zero · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCost.lean
Jpow_zero · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCost.lean:51 
/-- 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]
THEOREM Jpow_of_abs_one · Jcost_phi_pos · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCost.lean
Jpow_of_abs_one · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCost.lean:65 
/-- Either a single rung up or a single rung down costs exactly `J(φ)`: the recognition cost of a
forced interface distinction. -/
lemma Jpow_of_abs_one {d : ℤ} (h : d = 1 ∨ d = -1) : Jpow d = Cost.Jcost Constants.phi := by
  rcases h with h | h <;> subst h
  · exact Jpow_one
  · exact Jpow_neg_one
Jcost_phi_pos · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCost.lean:72 
/-- `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
THEOREM totalCost_eq_interfaceCost · totalCost_eq_interfaceCost · carriedCost_eq_zero · carriedCost_eq_zero · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCost.lean
totalCost_eq_interfaceCost · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCost.lean:143 
/-- **The total cost equals the interface cost**, because the carried bulk contributes nothing. -/
theorem totalCost_eq_interfaceCost (t : ℕ) : totalCost t = interfaceCost t := by
  have hsplit := Finset.sum_filter_add_sum_filter_not (E t)
    (fun p => polarized t p.1 ≠ polarized t p.2) (edgeCost t)
  have hBeq : (E t).filter (fun p => polarized t p.1 ≠ polarized t p.2) = B t := by
    rw [E, B, Finset.filter_filter]
  have hMeq : (E t).filter (fun p => ¬ (polarized t p.1 ≠ polarized t p.2)) = carried t := by
    rw [carried]
    apply Finset.filter_congr
    intro p _
    simp
  rw [hBeq, hMeq] at hsplit
  have hzero : ∑ p ∈ carried t, edgeCost t p = 0 := by
    apply Finset.sum_eq_zero
    intro p hp
    exact edgeCost_carried_zero t p hp
  rw [hzero, add_zero] at hsplit
  simp only [totalCost, interfaceCost]
  exact hsplit.symm
carriedCost_eq_zero · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCost.lean:130 
/-- **Carried cost is exactly zero.** The whole bulk the engine carries coarse costs no recognition. -/
theorem carriedCost_eq_zero (t : ℕ) : carriedCost t = 0 := by
  simp only [carriedCost]
  apply Finset.sum_eq_zero
  intro p hp
  exact edgeCost_carried_zero t p hp
THEOREM totalCost_card · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCost.lean
totalCost_card · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCost.lean:168 
/-- **The total recognition cost of the polarized diamond field is `(8t - 4) • J(φ)`** (`t ≥ 1`):
the carried bulk is free, and the whole cost sits on the `8t - 4` interface edges. -/
theorem totalCost_card (t : ℕ) (ht : 1 ≤ t) :
    totalCost t = (8 * t - 4) • Cost.Jcost Constants.phi := by
  rw [totalCost_eq_interfaceCost, interfaceCost_card t ht]
THEOREM totalCost_card · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCost.lean
totalCost_card · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCost.lean:168 
/-- **The total recognition cost of the polarized diamond field is `(8t - 4) • J(φ)`** (`t ≥ 1`):
the carried bulk is free, and the whole cost sits on the `8t - 4` interface edges. -/
theorem totalCost_card (t : ℕ) (ht : 1 ≤ t) :
    totalCost t = (8 * t - 4) • Cost.Jcost Constants.phi := by
  rw [totalCost_eq_interfaceCost, interfaceCost_card t ht]

What this page does not claim

The declaration does not claim that the polarized birth field is the actual physical universe. It does not claim that the cost function J is derived from the interface structure; J is a separate theorem. It does not claim that the bulk is physically free, only that its recognition cost is zero within this model.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND