Cosmology Graded Rung Cost Edge Cost Interface

The interface cost

In the Recognition Science framework, a ledger is a discrete record of events, and each event carries a forced cost. The declaration edgeCost_interface is a theorem about one specific kind of event: the boundary between two adjacent regions that sit on different rungs of a phi-rung scale. A rung is a level in a discrete ladder of scales, and the theorem concerns the cost of the boundary itself, not the cost of the regions it separates.

The theorem states a precise equality. If two neighboring regions have rung numbers that differ by exactly one, and if the rung field satisfies the unit-step property (the rung changes by at most one across any adjacency), then the cost of that single boundary edge is exactly J(phi), where J is the forced cost function and phi is the golden ratio. The proof runs through the definition of edge cost as J applied to the rung difference, then uses the unit-step hypothesis to narrow the difference to either +1 or -1, and finally applies reciprocal symmetry to show both cases yield the same value. The result holds for any finite edge set and any integer rung field meeting the unit-step condition, with no fitted parameters.

The theorem does not claim that every boundary costs J(phi). It requires the unit-step property: the rung difference must be exactly one. A boundary between regions two or more rungs apart is outside the theorem's scope. Nor does it claim anything about what causes the rung difference, or about the physical meaning of the rungs themselves. Those questions belong to other parts of the framework. The theorem is a statement about the cost function's behavior under a specific structural condition, nothing more.

What the theorem changes is the accounting. It reduces the cost of any unit-step boundary to a single constant, independent of the rung values involved. This makes the total cost of a graded rung profile computable by counting boundaries, not by summing over all edges. The engine that maintains such profiles can therefore predict its own cost from the number of interfaces alone, a substantial simplification of the ledger bookkeeping.

/-- 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

/-- 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

What this page does not claim

The theorem does not apply to boundaries where the rung difference is two or more. The theorem does not explain why regions sit on different rungs in the first place. The theorem does not assign physical meaning to the rungs themselves.

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: