Encyclopedia Foundation Foundation Pair Kernel Delta Spatial Bridge S5 Framed Torus Laplacian Eq Torus L

ARTICLE 4 claims 4 theorems

Foundation Pair Kernel Delta Spatial Bridge S5 Framed Torus Laplacian Eq Torus L

The framework proves that its spatial operator is the standard torus Laplacian, independent of how the three axes are labeled.

Verify this page

The frame-free Laplacian

The ledger, a discrete record of recognition events, assigns each posting a cost. The framework's minimum-cost theorem forces exactly one account coordinate per posting, and its dimension forcing supplies exactly three spatial generator axes. But no theorem selects a preferred labelling of those axes, and the new result shows none is needed: every permutation of the three account axes gives the same isotropic six-neighbor torus operator.

The declaration framedTorusLaplacian_eq_torusLaplacian proves that the operator defined through a frame, a chosen ordering of the three axes, is exactly the canonical torus Laplacian. The framed operator sums, over each of the three axes, the value at a site minus the values at its two opposite neighbors. The theorem shows this sum does not depend on which axis is called first, second, or third. A permutation of the axes merely reorders the terms in the sum, so the result is identical.

This frame independence matters because the framework's bridge from postings to space is target-blind: its definitions mention neither finite range, Green behavior, nor protein data. The operator comes from the complete family of one-coordinate postings, with axis labels quotiented by frame invariance. The same operator has the already-proved global spectral Green response, meaning the Laplacian inverts the dipole source on the torus.

The theorem also records a separator. The canonical Gray clock, a fixed cycle through eight of the twelve cube edges, does not exhaust the adjacency of the three-bit cube. A valid minimum-J posting can traverse a cube edge absent from that fixed cycle, so the clock shift alone does not generate the isotropic spatial operator. The operator comes from the full family of one-coordinate postings, not from a single cycle.

In Recognition Science, this result establishes that the spatial Laplacian is canonical and frame-covariant, not an artifact of a chosen axis labelling. It does not claim that the physical recognition-to-linking bridge is complete, nor that the framework derives the fine-structure constant. The theorem is a topological and algebraic fact about the operator, not a statement about measured physics.

THEOREM framedTorusLaplacian_eq_torusLaplacian · IndisputableMonolith/Foundation/PairKernelDeltaSpatialBridgeS5.lean
framedTorusLaplacian_eq_torusLaplacian · IndisputableMonolith/Foundation/PairKernelDeltaSpatialBridgeS5.lean:369 
/-- **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)))
THEOREM framedAxisStep_frame_independent · IndisputableMonolith/Foundation/PairKernelDeltaSpatialBridgeS5.lean
framedAxisStep_frame_independent · IndisputableMonolith/Foundation/PairKernelDeltaSpatialBridgeS5.lean:330 
/-- Changing the account-axis frame does not change the operational step
relation: the frame only relabels a complete three-axis family. -/
theorem framedAxisStep_frame_independent {N : ℕ}
    (σ τ : Equiv.Perm (Fin 3))
    (p q : TorusSite3 N) :
    FramedAxisStep σ p q ↔ FramedAxisStep τ p q := by
  constructor
  · rintro ⟨k, hk | hk⟩
    · refine ⟨τ.symm (σ k), Or.inl ?_⟩
      simpa [framedForward] using hk
    · refine ⟨τ.symm (σ k), Or.inr ?_⟩
      simpa [framedBackward] using hk
  · rintro ⟨k, hk | hk⟩
    · refine ⟨σ.symm (τ k), Or.inl ?_⟩
      simpa [framedForward] using hk
    · refine ⟨σ.symm (τ k), Or.inr ?_⟩
      simpa [framedBackward] using hk
THEOREM jMinimalPosting_can_escape_grayClock · IndisputableMonolith/Foundation/PairKernelDeltaSpatialBridgeS5.lean
jMinimalPosting_can_escape_grayClock · IndisputableMonolith/Foundation/PairKernelDeltaSpatialBridgeS5.lean:141 
/-- 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
THEOREM framedRecognitionGenerator_globalGreen_consumer · IndisputableMonolith/Foundation/PairKernelDeltaSpatialBridgeS5.lean
framedRecognitionGenerator_globalGreen_consumer · IndisputableMonolith/Foundation/PairKernelDeltaSpatialBridgeS5.lean:503 
/-- **Consumer-changing S5 terminal.** The operational relation generated by
minimum-posting axis classes is bounded in its derived step distance, while
the exact same frame-independent operator has the canonical global spectral
Green response. Unlike the S4 consumer, there is no arbitrary graph `G`
decoupled from the Green operator. -/
theorem framedRecognitionGenerator_globalGreen_consumer
    {N : ℕ} [NeZero N]
    (σ : Equiv.Perm (Fin 3))
    (sourceScale : ℂ) (a b p : TorusSite3 N) :
    BoundedRecognitionRelationOn
        (@FramedAxisStep N σ) (@framedStepDistance N σ) 1 ∧
      framedTorusLaplacian σ
          (scaledDipoleGreenResponse sourceScale a b) p =
        scaledTorusDipole sourceScale a b p := by
  refine ⟨framedAxisStep_bounded σ, ?_⟩
  rw [framedTorusLaplacian_eq_torusLaplacian]
  exact
    (localGenerator_globalGreen_consumer
      (N := N) sourceScale a b p).2

What this page does not claim

The physical recognition-to-linking bridge is complete. The framework derives the fine-structure constant alpha. The Gray clock generates the full isotropic spatial operator.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND