Gravity Recognition Ledger Boundary Cost Symmetric

The boundary cost symmetry

In the Recognition Science framework, a ledger, a discrete record of comparison costs between cells, can be split into two parts. The boundary cost is the total cost of comparing every cell on one side with every cell on the other side. The theorem boundaryCost_symmetric states that this total is unchanged if you swap the two sides: the cost of comparing the inside to the outside equals the cost of comparing the outside to the inside.

The proof is a direct consequence of the ledger's defining symmetry property, which says the cost of comparing cell i with cell j equals the cost of comparing j with i. The theorem formalizes that the sum over all cross-boundary pairs is the same regardless of summation order. It is a structural result about the bookkeeping, not a claim about any particular physical system.

In Recognition Science, this symmetry is one of the plain conditions that force the unique cost function J(x) = (x + 1/x)/2 - 1, proved in the machine-checked library of formal theorems. The boundary cost symmetry is a derived consequence of that foundation, and it supports the framework's later use of boundary costs in gravitational action and entropy calculations.

What the theorem does not claim: it does not say anything about the magnitude of the boundary cost, only that it is symmetric. It does not assert that the boundary cost is zero, or that it is minimized by any particular partition. It also does not claim that the boundary cost itself is a physical observable; that identification is a separate modeling step within the framework.

/-- Boundary cost is symmetric: exchanging interior and exterior gives
the same boundary cost. -/
theorem boundaryCost_symmetric {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
    (L : RecognitionLedger Λ) (P : SubstrateBipartition Λ) :
    boundaryCost L P =
    ∑ j ∈ P.exterior, ∑ i ∈ P.interior, L.cost j i := by
  unfold boundaryCost
  rw [Finset.sum_comm]
  congr 1; ext j
  congr 1; ext i
  exact L.symmetric i j

theorem rclGate_symmetric (u v : ℝ) : rclGate u v = rclGate v u := by
  unfold rclGate; ring

What this page does not claim

The theorem does not claim that the boundary cost is zero or has any particular value. It does not claim that the boundary cost is a physical observable. It does not claim that the boundary cost is minimized by any particular partition.

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/Gravity/RecognitionLedger.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: