Foundation Pair Kernel Delta Spatial Bridge S5

The spatial bridge

The module called foundation pair kernel delta spatial bridge s5, in the Recognition Science framework, closes a gap between two earlier results. One result says that the cheapest possible recognition event, the minimum-J posting, changes exactly one account in a three-account ledger. Another result says that three spatial dimensions are forced. What was missing was a bridge: a proof that a minimum-J posting, which lives in the abstract space of ledger accounts, actually produces the familiar spatial operator on a three-dimensional lattice, the discrete Laplacian, and that this operator does not depend on how the three axes are named or ordered.

The bridge works by treating the three ledger accounts as three spatial axes. A minimum-J posting changes one account, so it moves a point on the lattice along exactly one axis. The module proves that for any choice of axis labelling, a permutation of the three axes, the posting induces a unique axis generator: a unique direction in which the point moves. Opposite moves along that axis are inverses, and moves along different axes commute. The sum over all three paired axes, the operator that averages a function over the six neighbors of a lattice site, is exactly the canonical torus Laplacian, and it is independent of the chosen axis frame. This is the central theorem, ledger, a discrete record of recognition events, to spatial geometry.

The module also records a subtlety about the eight-tick cycle. The canonical Gray clock, a fixed cycle through eight of the twelve edges of the three-dimensional cube, does not exhaust the adjacency structure. A valid minimum-J posting can traverse a cube edge that is absent from that fixed cycle. The clock shift alone therefore does not generate the isotropic spatial operator. The operator comes from the complete family of one-coordinate postings, with axis labels quotiented by frame invariance. This is a theorem, not a design choice: the module proves that the two candidate support models, the global one that allows any transition and the canonical one that selects only minimum-J steps, disagree.

In Recognition Science, this bridge is what makes the step from abstract ledger to observable space explicit. The module is target-blind: its definitions mention neither finite range, Green behavior, protein data, nor the coupling obligation. The bridge is a structural fact about the minimum-J posting and the three-account ledger, proved in the framework's machine-checked library of formal theorems with no sorry and no new axiom.

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

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

What this page does not claim

This module does not prove that space is three-dimensional; that is a separate theorem in the forcing chain. This module does not derive the fine-structure constant or any specific physical coupling. The bridge does not claim that the Gray clock is the only structure; it proves the clock alone is insufficient.

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: