Foundation Pair Kernel Delta Spatial Bridge S5 J Minimal Posting Step Unique Acc

The unique account axis

The declaration jMinimalPostingStep_unique_account_axis is a theorem in the framework's machine-checked library of formal theorems. It states that any posting step which achieves the minimum possible recognition cost changes the parity, the on or off state, of exactly one account out of three. The theorem then proves that this account is unique: there is no ambiguity about which account changed. This is the foundational step that connects the abstract ledger, a discrete record of events, to a concrete geometric picture.

The result is not about a specific posting. It is a universal statement: for any two ledger states A and B, if the step from A to B is a minimum-cost posting, then there exists a unique index k among the three accounts such that the parity of A and B differ at k, and only at k. The proof follows directly from a prior theorem, jMinimalPostingStep_oneBitDiff, which establishes that a minimum-cost step changes exactly one bit. The uniqueness part is the new content: it rules out the possibility that two different accounts could both be the changed one.

This uniqueness is what allows the framework to build a spatial operator. Because each minimal posting picks out a single account axis, the framework can define a move along that axis on a three-dimensional torus, a grid with wrapped edges. The theorem jMinimalPostingStep_induces_unique_axis_generator shows that, for any chosen frame, a minimal posting induces a unique translation generator along one of the three spatial axes. This is the bridge from the abstract account structure to the geometry of space.

In Recognition Science, this is a key step in deriving three-dimensional space from the cost of recognition. The framework models each account as a coordinate, and the unique axis theorem ensures that a minimal step moves along exactly one coordinate. This is why the resulting spatial operator is isotropic: it does not depend on how the three axes are labelled or permuted. The theorem framedTorusLaplacian_eq_torusLaplacian confirms that the operator built from these framed steps is exactly the standard torus Laplacian, independent of the frame choice.

The theorem does not claim that any particular labelling of the three axes is preferred. There is no theorem selecting a canonical order for the accounts. The uniqueness is about the account that changes, not about the names of the axes. The framework explicitly notes that every permutation of the three account axes gives the same isotropic six-neighbor torus operator. The axis labels are quotiented by frame invariance, meaning the physics is unchanged by relabelling the three directions.

/-- Minimum J gives a unique account coordinate. -/
theorem jMinimalPostingStep_unique_account_axis
    {A B : LedgerPostingAdjacency.LedgerState 3}
    (h : JMinimalPostingStep A B) :
    ∃! k : Fin 3, parity 3 A k ≠ parity 3 B k :=
  jMinimalPostingStep_oneBitDiff h

/-- Minimum J gives a unique account coordinate. -/
theorem jMinimalPostingStep_unique_account_axis
    {A B : LedgerPostingAdjacency.LedgerState 3}
    (h : JMinimalPostingStep A B) :
    ∃! k : Fin 3, parity 3 A k ≠ parity 3 B k :=
  jMinimalPostingStep_oneBitDiff h

/-- A minimum-J posting selects one member of the frame-independent
translation family at every base site. Absolute position is intentionally
free: homogeneity makes the posting specify a displacement generator, not a
preferred origin. -/
theorem jMinimalPostingStep_induces_unique_axis_generator {N : ℕ}
    (σ : Equiv.Perm (Fin 3))
    {A B : LedgerPostingAdjacency.LedgerState 3}
    (h : JMinimalPostingStep A B)
    (p : TorusSite3 N) :
    ∃! a : Fin 3,
      FramedPostingAxis σ A B a ∧
        FramedAxisStep σ p (torusShift p a 1) := by
  rcases jMinimalPostingStep_unique_framed_axis σ h with
    ⟨a, ha, huniq⟩
  refine ⟨a, ⟨ha, ?_⟩, ?_⟩
  · rcases ha with ⟨k, rfl, hk⟩
    exact ⟨k, Or.inl rfl⟩
  · intro b hb
    exact huniq b hb.1

/-- **S5 operator bridge.** Every account-axis frame gives exactly the same
operator, namely the canonical periodic D=3 six-neighbor Laplacian. Thus no
preferred account-to-axis MODEL identification survives in the operator. -/
theorem framedTorusLaplacian_eq_torusLaplacian {N : ℕ}
    (σ : Equiv.Perm (Fin 3))
    (ψ : TorusSite3 N → ℂ) (p : TorusSite3 N) :
    framedTorusLaplacian σ ψ p = torusLaplacian ψ p := by
  unfold framedTorusLaplacian torusLaplacian framedForward framedBackward
  exact Equiv.sum_comp σ
    (fun i : Fin 3 =>
      (2 : ℂ) * ψ p -
        ψ (torusShift p i 1) -
        ψ (torusShift p i (-1)))

What this page does not claim

The theorem does not select a preferred labelling or ordering of the three spatial axes. The theorem does not claim that the minimum-cost posting is unique, only that the changed account is unique. The theorem does not establish the physical recognition-to-linking bridge; that remains open.

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