Foundation Pair Kernel Operational Locality S4 Global Balanced Ledger Conserves

The balanced ledger

A ledger, in the Recognition Science framework, is a discrete record of events. The declaration globalBalancedLedger_conserves concerns a particular ledger, globalBalancedLedger, which is defined so that every debit and every credit is exactly zero. The theorem proves that this ledger conserves: for any chain of transitions, the total flux across the ledger remains zero. In plain terms, if nothing is ever added or removed, nothing is ever lost or gained. The proof is a direct application of a general lemma about balanced ledgers, and it is checked by the framework's machine-checked library of formal theorems.

The significance of this result is not that a zero ledger is interesting by itself. It is that the theorem is used as a building block in a larger argument about operational locality. The framework asks: what does it mean for one event to depend on another? Its answer is that a dependency is operational if it is defined by realizable minimum-cost posting transitions, not by a range cutoff or a generator support. The balanced ledger theorem is one of several ingredients that must coexist in a candidate route for this locality property. The framework's library records exact countermodels showing that balanced conservation, along with shift-invariant cost and an eight-tick identity, can all hold while the dependency relation is still all-pairs, meaning every site depends on every other. The balanced ledger alone does not choose the spatial identification used by the translated-cell semantics.

What the declaration does not claim is therefore important. It does not claim that a balanced ledger forces locality. It does not claim that the zero ledger is the only balanced ledger, nor that conservation is a sufficient condition for the operational dependency structure. The theorem is a necessary ingredient in the framework's derivation, not a sufficient one. The framework's own documentation is explicit: the weaker candidate routes, which include balanced conservation, are exactly the routes that admit countermodels where locality fails. The positive result, tiledJMinimalDependency3_operationally_local, requires the full minimum-J posting semantics, not just balance.

For a reader coming from outside the framework, the practical lesson is about proof discipline. A machine-checked theorem that a trivial ledger conserves is a small, exact fact. Its value lies in how it is composed with other facts. The framework's library uses it as a witness that certain combinations of properties are consistent, and as a contrast case for the stronger operational locality theorem. The declaration is a precise, narrow claim: a zero ledger conserves. It is not a claim about the world, about physics, or about any nontrivial dynamics. It is a formal statement about a formal object, and the framework's honesty about its limits is part of how it earns trust.

/-- The all-pairs ledger conserves because it is balanced. Conservation places
no spatial restriction on the carrier relation. -/
theorem globalBalancedLedger_conserves (n : ℕ) :
    Conserves (globalBalancedLedger n) := by
  refine { conserve := ?_ }
  intro ch _
  exact chainFlux_zero_of_balanced
    (globalBalancedLedger n) ch (by intro u; rfl)

/-- Atomicity, balanced conservation, shift-invariant J-cost, period eight,
D=3, and a nontrivial distinction all coexist with an all-pairs dependency.
Thus none of those scalar or temporal declarations chooses spatial locality. -/
theorem committed_candidate_routes_admit_allPairs :
    Nonempty (AtomicTick (tickCarrier 8)) ∧
      Conserves (globalBalancedLedger 8) ∧
      ShiftInvariant (meanFieldLedgerCost 8) ∧
      EightTickFromDimension 3 = eight_tick ∧
      (∃ a b : Fin (2 * 2 * 2), a ≠ b) ∧
      ¬ LocalOperationalDependency3 2 1
        (allPairsDependency :
          Fin (2 * 2 * 2) → Fin (2 * 2 * 2) → Prop) := by
  refine ⟨⟨globalAtomicTick (fun _ => 0)⟩,
    globalBalancedLedger_conserves 8,
    meanFieldLedgerCost_shift_invariant 8,
    rfl, ?_, allPairsDependency_not_local3 2 (by omega)⟩
  exact ⟨0, 1, by decide⟩

/-- **S4 locality theorem.** The operational dependency induced by minimum-J
posting in translated D=3 cells satisfies `LocalOperationalDependency3`
at radius one. The theorem is exact on the account-axis MODEL identification;
production selection of that identification remains the physical hard fork. -/
theorem tiledJMinimalDependency3_operationally_local
    {L : ℕ} (hL : 2 ≤ L) :
    LocalOperationalDependency3 L 1 (TiledJMinimalDependency3 hL) := by
  intro i j hij
  rcases hij with ⟨origin, A, B, hstep, rfl, rfl⟩
  have hdist :
      dist3
        (patternAtCell hL origin (parity 3 A))
        (patternAtCell hL origin (parity 3 B)) = 1 := by
    rw [patternAtCell_dist3]
    exact oneBitDiff_patternDist3
      (jMinimalPostingStep_oneBitDiff hstep)
  simpa only [encodedDist3, Equiv.symm_apply_apply] using hdist.le

What this page does not claim

The balanced ledger theorem does not claim that conservation forces locality. The balanced ledger is not claimed to be the only balanced ledger. The theorem does not claim anything about physical conservation laws in the empirical world.

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/Foundation/PairKernelOperationalLocalityS4.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: