Foundation Pair Kernel Delta Spatial Bridge S5 Canonical Bare Minimum Jsupport M

The canonical spatial bridge

The declaration canonicalBareMinimumJSupportModel3_selected is a theorem in the framework's machine-checked library of formal theorems. It proves that a specific construction, called the canonical bare minimum J support model, is the unique rule for generating spatial steps that respects the framework's core principle: a minimal recognition event, a single discrete change in a ledger of account states, must correspond to exactly one step along one of three spatial axes.

The theorem states that this canonical rule is equivalent to the relation JMinimalGeneratedStep with the identity frame. In plain terms, the rule is: a spatial step is allowed if and only if it is generated by a minimal recognition event, and that event changes exactly one account coordinate. The proof is direct, by reflexivity, and the declaration also records that this canonical rule is distinct from a trivial global rule that would allow every possible step. This distinction matters because it shows the framework does not merely assert a spatial structure; it derives it from the minimal-cost condition on recognition events.

In Recognition Science, the framework models physical space as a three-dimensional torus, a grid of sites where each site has six neighbors, two along each of three axes. The canonical rule selects, among all possible ways to define a spatial step, the one that is generated by a minimal posting. The theorem jMinimalPostingStep_unique_account_axis proves that each minimal posting changes exactly one account coordinate, and jMinimalPostingStep_induces_unique_axis_generator proves that this change induces a unique axis generator under any frame permutation. The canonical rule combines these facts: it is the unique rule that uses only minimal postings and respects the frame independence of the axes.

The theorem also establishes a key property of the resulting spatial operator. The sum over all three paired axes of the framed Laplacian is independent of the chosen frame and equals the standard torus Laplacian, as proved by framedTorusLaplacian_eq_torusLaplacian. This means the canonical rule produces the familiar discrete Laplacian on a three-dimensional grid, the operator that appears in the framework's Green function analysis. The canonical rule is therefore not an arbitrary choice; it is the one that yields the standard spatial structure from the minimal-cost principle.

What the theorem does not claim is equally important. It does not claim that the canonical rule is the only model of spatial support; the library explicitly proves that a global rule, which allows all steps, is a different model. It does not claim that the canonical rule is derived from the physical recognition-to-linking bridge, which remains an open target. It also does not claim that the canonical rule selects a preferred labelling of the three axes; the theorem jMinimalGeneratedStep_frame_independent proves that the rule is invariant under any permutation of the axes. The theorem is a precise, machine-checked statement about the structure of the framework's spatial model, not a claim about the physical origin of that structure.

theorem canonicalBareMinimumJSupportModel3_selected :
    ProductionSelectsMinimumJSupport3
      canonicalBareMinimumJSupportModel3.productionSupport := by
  intro p q
  rfl

/-- **Exact S5 hard-fork countermodels.** Two models carry the same connected
minimum-J posting fact but have distinct production supports. One satisfies
the support-selection arrow and the other does not. This is the precise
underdetermination licensed by the current declaration boundary. -/
theorem bareMinimumJSupportModels_disagree :
    globalBareMinimumJSupportModel3.productionSupport ≠
      canonicalBareMinimumJSupportModel3.productionSupport := by
  intro heq
  have hselected := canonicalBareMinimumJSupportModel3_selected
  rw [← heq] at hselected
  exact globalProductionSupport3_not_selected hselected

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

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

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

What this page does not claim

The theorem does not claim that the canonical rule is the only model of spatial support. The theorem does not claim that the canonical rule is derived from the physical recognition-to-linking bridge. The theorem does not claim that the canonical rule selects a preferred labelling of the three spatial axes.

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: