Cosmology Graded Rung Cost

The graded rung cost ledger

A ledger, a discrete record of events, can carry many kinds of entries. In Recognition Science, the cost of carrying an entry is forced by a proved theorem, not chosen. The graded rung cost result extends that outcome from a simple binary case to a general one: a field where each region carries an integer rung value, and adjacent regions may differ by at most one rung. The result proves that the total cost of such a field is exactly the number of differing adjacencies, times a fixed constant J(phi).

The single assumption is the forced minimal-distinction property: across every adjacency, the rung changes by at most one. A unit recognition step resolves at most one phi-rung, so the difference between neighboring rung values is always 0, +1, or -1. This is not a fitted parameter; it is the invariant the engine maintains as its T-3 refiner descends one rung at a time. The result proves, over the reals with zero gaps and only the three standard axioms, that a carried adjacency with equal rungs costs exactly 0, and an interface adjacency with different rungs costs exactly J(phi).

The closed form follows directly: total cost equals interface cost, which equals the count of differing adjacencies times J(phi). The same-rung bulk costs nothing. This holds for any integer rung field on any finite edge set, not just the binary birth field of the earlier phase. The polarized birth field is recovered as the special case where the rung field takes only the values +1, 0, and -1, with the unit-step property discharged by the earlier level-difference mechanism.

The practical consequence is a simple pricing rule for the engine: pay exactly J(phi) per forced unit-rung distinction, carry the entire same-rung bulk for free. The theorem is tagged THEOREM in the machine-checked library of formal theorems, with zero gaps and only the three standard axioms. It does not derive the value of J(phi) itself; that is a separate result. The result establishes the cost law at the level of generality the live engine needs, not just for the simplified birth field.

/-- A carried (equal-rung) adjacency costs exactly zero: `J(phi^0) = J(1) = 0`. -/
theorem edgeCost_carried (k : V → ℤ) {p : V × V} (h : k p.1 = k p.2) :
    edgeCost k p = 0 := by
  have hz : k p.1 - k p.2 = 0 := sub_eq_zero.mpr h
  rw [edgeCost, hz, Jpow_zero]

/-- Under the unit-step law, an interface (different-rung) adjacency costs exactly `J(phi)`: the gap
is forced to `±1` rung, and `J(phi^(±1)) = J(phi)` by reciprocal symmetry. -/
theorem edgeCost_interface (k : V → ℤ) {E : Finset (V × V)} (hk : UnitStep k E)
    {p : V × V} (hp : p ∈ E) (hne : k p.1 ≠ k p.2) :
    edgeCost k p = Cost.Jcost Constants.phi := by
  have hd : k p.1 - k p.2 = 1 ∨ k p.1 - k p.2 = -1 := by
    rcases hk p hp with h0 | h1 | hm1
    · exact absurd (sub_eq_zero.mp h0) hne
    · exact Or.inl h1
    · exact Or.inr hm1
  rw [edgeCost]
  exact Jpow_of_abs_one hd

/-- **The total recognition cost of any unit-step rung field is `(interface edge count) * J(phi)`.**
Carried bulk is free; the whole cost sits on the forced unit-rung distinctions. -/
theorem totalCost_eq_card (k : V → ℤ) (E : Finset (V × V)) (hk : UnitStep k E) :
    totalCost k E = (E.filter (fun p => k p.1 ≠ k p.2)).card • Cost.Jcost Constants.phi := by
  rw [totalCost_eq_interfaceCost, interfaceCost_eq_card k E hk]

/-- **The general law recovers the Phase-55 2D closed form.** Instantiating the graded-rung ledger at
the polarized birth field gives `totalCost = (8t - 4) * J(phi)` (`t >= 1`): Phase 55 is the binary
special case of the graded-rung cost law. -/
theorem polarized_totalCost_card (t : ℕ) (ht : 1 ≤ t) :
    totalCost (polarized t) (E t) = (8 * t - 4) • Cost.Jcost Constants.phi := by
  rw [polarized_totalCost, PolarizedBirthInterfaceCost.Diamond.totalCost_card t ht]

What this page does not claim

This module does not derive the value of J(phi) itself. This module does not prove that the unit-step property holds for all possible rung fields. This module does not describe how the T-3 refiner implements the single-rung descent.

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