Encyclopedia Foundation Foundation Pair Kernel Signed Posting Transport S11 Pulled Back Signed Posting L

ARTICLE 4 claims 4 theorems

Foundation Pair Kernel Signed Posting Transport S11 Pulled Back Signed Posting L

A machine-checked theorem shows that a graph which counts every event, even when events collide, produces exactly the same Laplacian operator as the ideal six-neighbor picture.

Verify this page

The collision repair

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition event is one unit of that record. The framework's core model places these events on a torus, a finite grid with wrap-around edges. The question at hand is how to build a graph, a set of points and connections, from these events. A naive graph might record only whether a connection exists, not how many events created it. That naive graph has a flaw: when two events land on the same connection, the graph forgets that there were two.

The declaration pulledBackSignedPostingLaplacian3_eq_framed proves that a refined graph, one that counts every event, repairs this flaw. The theorem states that the Laplacian, a standard operator that measures how a value at a point differs from its neighbors, computed on this refined graph is exactly equal to the ideal six-neighbor operator, which is defined without any reference to collisions. This holds for every nonempty period, including the problematic period two where collisions first occur. The proof is machine-checked: it is a theorem in the framework's library, with no unproven assumptions and no missing steps.

The key to the repair is the signed weight function. For each pair of sites, this function counts one forward and one backward event for each of the three axes, even when periodicity makes those events land on the same site. The theorem signedPostingWeight3_nonneg shows this count is never negative, and signedPostingWeight3_symm shows it is symmetric. The support of this weight, the set of connections it makes nonzero, is exactly the minimum-J support, the set of connections the framework's cost function forces. The refined graph therefore preserves the correct set of connections while also recording the correct multiplicities.

This result is a collision repair because it fixes the S8 relation-set graph, which forgets one occurrence when two events collide. The S10 countermodel, which shows the unrefined graph fails, remains valid. The refined graph, by contrast, closes the source equation for every posting magnitude and every nondegenerate period, as shown by signedPostingSourceAttachment3_realGreen. The practical consequence is that the framework can use the simpler six-neighbor operator without worrying about collisions, because the refined graph reproduces it exactly.

In Recognition Science, this theorem is a step in the forcing chain that derives three spatial dimensions. It shows that a discrete ledger of events, when counted properly, yields the same smooth operator as the ideal picture. The theorem does not claim that the physical world is a torus, nor that the refined graph is the only way to repair collisions. It establishes a formal equivalence between two mathematical objects within the framework's model.

THEOREM pulledBackSignedPostingLaplacian3_eq_framed · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean
pulledBackSignedPostingLaplacian3_eq_framed · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean:255 
/-- The multiplicity-preserving graph fold is exactly the framed six-neighbor
operator. No collision-free hypothesis is needed. -/
theorem pulledBackSignedPostingLaplacian3_eq_framed
    {N : ℕ} [NeZero N]
    (σ : Equiv.Perm (Fin 3))
    (field : TorusSite3 N → ℝ)
    (p : TorusSite3 N) :
    (pulledBackSignedPostingLaplacian3 σ field p : ℂ) =
      framedTorusLaplacian σ
        (fun x => (field x : ℂ)) p := by
  have hreal :
      pulledBackSignedPostingLaplacian3 σ field p =
        ∑ k : Fin 3,
          ((2 : ℝ) * field p -
            field (framedForward σ p k) -
            field (framedBackward σ p k)) := by
    unfold pulledBackSignedPostingLaplacian3 laplacian
      signedRecognitionProductionGraph3
    rw [← Equiv.sum_comp (torusSiteEquivFin N)]
    simp only [Equiv.symm_apply_apply, Equiv.apply_symm_apply]
    unfold signedPostingWeight3
    calc
      ∑ q : TorusSite3 N,
          (∑ k : Fin 3,
            ((if q = framedForward σ p k then (1 : ℝ) else 0) +
              (if q = framedBackward σ p k then 1 else 0))) *
            (field p - field q) =
          ∑ q : TorusSite3 N, ∑ k : Fin 3,
            (((if q = framedForward σ p k then (1 : ℝ) else 0) +
              (if q = framedBackward σ p k then 1 else 0)) *
                (field p - field q)) := by
                  apply Finset.sum_congr rfl
                  intro q _
                  rw [Finset.sum_mul]
      _ = ∑ k : Fin 3, ∑ q : TorusSite3 N,
            (((if q = framedForward σ p k then (1 : ℝ) else 0) +
              (if q = framedBackward σ p k then 1 else 0)) *
                (field p - field q)) := Finset.sum_comm
      _ = ∑ k : Fin 3,
            ((field p - field (framedForward σ p k)) +
              (field p - field (framedBackward σ p k))) := by
                apply Finset.sum_congr rfl
                intro k _
                simp only [add_mul, Finset.sum_add_distrib]
                simp
      _ = ∑ k : Fin 3,
            ((2 : ℝ) * field p -
              field (framedForward σ p k) -
              field (framedBackward σ p k)) := by
                apply Finset.sum_congr rfl
                intro k _
                ring
  rw [hreal]
  unfold framedTorusLaplacian
  push_cast
  rfl
THEOREM signedPostingWeight3 · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean
signedPostingWeight3 · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean:38 
/-- Signed generator-event multiplicity between two torus sites. Each axis has
one forward and one backward occurrence, even when periodicity makes their
targets coincide. -/
def signedPostingWeight3
    {N : ℕ}
    (σ : Equiv.Perm (Fin 3))
    (p q : TorusSite3 N) : ℝ :=
  ∑ k : Fin 3,
    ((if q = framedForward σ p k then 1 else 0) +
      (if q = framedBackward σ p k then 1 else 0))
THEOREM signedPostingWeight3_ne_zero_iff · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean
signedPostingWeight3_ne_zero_iff · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean:90 
/-- Signed multiplicity is nonzero exactly on the minimum-J axis-step support.
Collisions change multiplicity, not support. -/
theorem signedPostingWeight3_ne_zero_iff
    {N : ℕ}
    (σ : Equiv.Perm (Fin 3))
    (p q : TorusSite3 N) :
    signedPostingWeight3 σ p q ≠ 0 ↔
      FramedAxisStep σ p q := by
  constructor
  · intro hne
    by_contra hstep
    have hfwd :
        ∀ k : Fin 3, q ≠ framedForward σ p k := by
      intro k h
      exact hstep ⟨k, Or.inl h⟩
    have hbwd :
        ∀ k : Fin 3, q ≠ framedBackward σ p k := by
      intro k h
      exact hstep ⟨k, Or.inr h⟩
    simp [signedPostingWeight3, hfwd, hbwd] at hne
  · rintro ⟨k, hk | hk⟩
    · apply ne_of_gt
      unfold signedPostingWeight3
      refine Finset.sum_pos'
        (fun i _ => by split_ifs <;> norm_num) ?_
      refine ⟨k, Finset.mem_univ k, ?_⟩
      simp [hk]
      split_ifs <;> norm_num
    · apply ne_of_gt
      unfold signedPostingWeight3
      refine Finset.sum_pos'
        (fun i _ => by split_ifs <;> norm_num) ?_
      refine ⟨k, Finset.mem_univ k, ?_⟩
      simp [hk]
      split_ifs <;> norm_num
THEOREM signedPostingSourceAttachment3_realGreen · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean
signedPostingSourceAttachment3_realGreen · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean:424 
/-- The multiplicity-preserving constructor closes the real posting-source
attachment for every posting magnitude and every nondegenerate period. -/
theorem signedPostingSourceAttachment3_realGreen
    {N : ℕ} [NeZero N]
    (hN : 2 ≤ N)
    (q : ℝ)
    (event : PostingPair3 N)
    (hevent : event ∈ realizedPrimitivePostingPairs3 N)
    (σ : Equiv.Perm (Fin 3)) :
    SignedPostingSourceAttachment3 q event σ
      (signedRealGreenField3 q event) := by
  rw [signedPostingSourceAttachment3_iff_scaledSourceEquation
    q event σ hevent]
  exact signedRealGreenField3_scaledSourceEquation hN σ q event

What this page does not claim

This theorem does not claim that the physical universe is a torus. It does not claim that the refined graph is the only way to repair collisions. It does not claim that the framework's derivation of three spatial dimensions is complete.

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