Encyclopedia Foundation Foundation Pair Kernel Signed Posting Transport S11

ARTICLE 5 claims 4 theorems 1 model

Foundation Pair Kernel Signed Posting Transport S11

A small fix in how events are counted lets a graph keep track of every forward and backward step, even when two steps land on the same place.

Verify this page

The collision repair

In the Recognition Science framework, a ledger is a discrete record of events. The construction named foundation pair kernel signed posting transport s11 addresses a counting problem in that ledger. When a system moves forward and then backward along the same axis, both events can land on the same ordered pair, so a simple set of pairs would record only one occurrence. This construction instead keeps a signed count of every generator event, so the ledger remembers that two distinct steps happened, not just that the pair was visited.

The core object is a weighted graph. For each pair of sites on a three-dimensional torus, the graph assigns a weight equal to the number of forward and backward generator events that connect them. The framework proves that this weight is nonnegative and symmetric, and that it is nonzero exactly on the same set of steps that the minimum-cost relation uses. Relabeling the three account axes does not change any weight, so the construction is independent of how the axes are named.

The main result is that the graph Laplacian of this weighted graph equals the framed six-neighbor operator for every nonempty period, including period two. This is the collision repair: the old relation-set graph forgot one occurrence at period two, but the signed graph does not. The framework also proves that each posting occurrence still has a unit dipole source, meaning the refinement does not change the fundamental divergence structure.

In Recognition Science, the framework models a real-valued Green field that solves the source equation on this graph at the exact scale q/2. The real part of the canonical complex Green response satisfies the equation for every posting magnitude and every nondegenerate period. This closes the posting-source attachment: the framework proves that the signed graph supports a consistent source solution.

The construction establishes that a collision in the ledger does not destroy information. By counting occurrences instead of just recording pairs, the framework keeps the full event structure and still recovers the same Laplacian operator. This is a technical repair, but it matters: without it, the graph would lose track of events at period two, and the operator would not match the framed six-neighbor form.

MODEL 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_nonneg · signedPostingWeight3_symm · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean
signedPostingWeight3_nonneg · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean:49 
theorem signedPostingWeight3_nonneg
    {N : ℕ}
    (σ : Equiv.Perm (Fin 3))
    (p q : TorusSite3 N) :
    0 ≤ signedPostingWeight3 σ p q := by
  unfold signedPostingWeight3
  exact Finset.sum_nonneg (fun k _ => by
    split_ifs <;> norm_num)
signedPostingWeight3_symm · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean:58 
theorem signedPostingWeight3_symm
    {N : ℕ}
    (σ : Equiv.Perm (Fin 3))
    (p q : TorusSite3 N) :
    signedPostingWeight3 σ p q =
      signedPostingWeight3 σ q p := by
  unfold signedPostingWeight3
  apply Finset.sum_congr rfl
  intro k _
  have hfwd :
      q = framedForward σ p k ↔
        p = framedBackward σ q k := by
    constructor
    · intro h
      subst q
      exact (framedForward_backward σ p k).symm
    · intro h
      subst p
      exact (framedBackward_forward σ q k).symm
  have hbwd :
      q = framedBackward σ p k ↔
        p = framedForward σ q k := by
    constructor
    · intro h
      subst q
      exact (framedBackward_forward σ p k).symm
    · intro h
      subst p
      exact (framedForward_backward σ q k).symm
  simp only [hfwd, hbwd]
  ring
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 signedPostingOccurrence_divergence_eq_dipole · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean
signedPostingOccurrence_divergence_eq_dipole · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean:187 
/-- Refining pair multiplicity does not change double-entry source
divergence: each oriented posting occurrence still has unit dipole source. -/
theorem signedPostingOccurrence_divergence_eq_dipole
    {N : ℕ} [NeZero N]
    (event : PostingPair3 N)
    (i : Fin (TorusCard3 N)) :
    postingDivergence
        (PairKernelSourceCoupling.elementaryPosting event.1 event.2) i =
      dipole event.1 event.2 i :=
  elementaryPosting_divergence_eq_dipole event.1 event.2 i
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 construction does not derive the cost function J(x). This construction does not prove that three spatial dimensions are forced. This construction does not claim the signed graph is the only way to repair the collision.

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