Foundation Pair Kernel Delta Spatial Bridge S5 J Minimal Generated Step Iff Fram

The framed step equivalence

In the Recognition Science framework, a ledger (a discrete record of events) changes state through postings. A minimum-J posting is the cheapest possible such change, the one that minimizes the framework's forced cost function. The theorem jMinimalGeneratedStep_iff_framedAxisStep states that these minimal postings are exactly the moves that step along a single one of three spatial axes, once those axes have been labeled or "framed" by a permutation. In plainer terms: the cheapest possible change to the ledger is always a move along exactly one of the three perpendicular directions of space, never a diagonal or a jump.

The equivalence has a precise consequence for how space is generated. The framework's dimension forcing already supplies three spatial axes. This theorem shows that a minimal posting, when transported onto a three-dimensional torus (a space that wraps around like a video game screen), corresponds to a unit step along one axis, forward or backward. The direction is unique for that posting, and the choice of which axis is called "first," "second," or "third" does not matter: any relabeling of the axes gives the same set of allowed steps. The sum over all three paired directions produces the standard torus Laplacian, the operator that appears in diffusion and wave equations.

The theorem also separates the minimal postings from a simpler candidate. A "Gray clock" is a fixed cycle through eight of the twelve edges of the cube that represents the three-bit states of the ledger. The theorem shows that a minimal posting can traverse an edge that is not on that fixed cycle. So the clock alone does not generate the full spatial operator; the complete family of one-coordinate postings is needed, with the axis labels quotiented out by frame invariance.

What the theorem does not claim is equally important. It does not select a preferred labeling of the three axes; any permutation works. It does not say that every pair of points on the torus is connected by a minimal step, only that each minimal step is a single-axis move. It does not assert that the physical recognition-to-linking bridge to real three-dimensional space is complete; that bridge remains an open target. The theorem is a statement about the formal structure of minimal ledger changes, not about which axis is "x" or why space has three dimensions in the first place.

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

/-- Minimum-J generated support is frame independent. -/
theorem jMinimalGeneratedStep_frame_independent {N : ℕ}
    (σ τ : Equiv.Perm (Fin 3))
    (p q : TorusSite3 N) :
    JMinimalGeneratedStep σ p q ↔ JMinimalGeneratedStep τ p q := by
  rw [jMinimalGeneratedStep_iff_framedAxisStep,
    jMinimalGeneratedStep_iff_framedAxisStep]
  exact framedAxisStep_frame_independent σ τ p q

/-- A concrete minimum-J posting exists on an edge omitted by the fixed Gray
clock. This is the ledger-level separator, not merely a graph observation. -/
theorem jMinimalPosting_can_escape_grayClock :
    ∃ A B : LedgerPostingAdjacency.LedgerState 3,
      JMinimalPostingStep A B ∧
        parity 3 A = zeroPattern3 ∧
        parity 3 B = axisOnePattern3 ∧
        ¬ GrayClockEdge (parity 3 A) (parity 3 B) := by
  let A : LedgerPostingAdjacency.LedgerState 3 :=
    { debit := fun _ => 0
      credit := fun _ => 0 }
  let k : Fin 3 := 1
  let B : LedgerPostingAdjacency.LedgerState 3 := post A k Side.debit
  have hpost : PostingStep A B := ⟨k, Side.debit, rfl⟩
  have hneq : A ≠ B := by
    intro h
    have hk := congrArg
      (fun S : LedgerPostingAdjacency.LedgerState 3 => S.debit k) h
    simp [A, B, post] at hk
  have hmin : JMinimalPostingStep A B :=
    postingStep_is_jMinimal hpost hneq
  have hA : parity 3 A = zeroPattern3 := by
    funext i
    simp [A, zeroPattern3, parity, parityPattern, phiVec, Recognition.phi]
  have hB : parity 3 B = axisOnePattern3 := by
    funext i
    by_cases hi : i = k
    · subst i
      simp [A, B, k, post, axisOnePattern3, parity, parityPattern,
        phiVec, Recognition.phi]
    · simp [A, B, k, post, axisOnePattern3, parity, parityPattern,
        phiVec, Recognition.phi, hi]
  refine ⟨A, B, hmin, hA, hB, ?_⟩
  rw [hA, hB]
  exact zero_axisOne_not_grayClockEdge

/-- **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 prove that space must have three dimensions; that is a separate result. The theorem does not claim that every pair of points on the torus is connected by a minimal step. The theorem does not identify which physical axis is 'x', 'y', or 'z'.

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: