Encyclopedia Foundation Foundation Pair Kernel Signed Posting Transport S11 Signed Posting Source Attach

ARTICLE 4 claims 3 theorems 1 model

Foundation Pair Kernel Signed Posting Transport S11 Signed Posting Source Attach

A machine-checked theorem ties a posting's magnitude to a scaled source equation, repairing a collision that would otherwise lose events.

Verify this page

The signed posting source

In the Recognition Science framework, a ledger is a discrete record of events. This theorem concerns a specific kind of event: a posting, which is a transfer between two accounts on a torus, a finite grid with wrap-around edges. The framework's recognition cost, the price of recording an event, forces a particular structure. The theorem, named signedPostingSourceAttachment3_iff_scaledSourceEquation, establishes an equivalence: attaching a posting's magnitude to a field on the graph is exactly the same as that field satisfying a scaled source equation.

The scaled source equation, written in symbols as ScaledSourceEquation(weight, dipole, q/2, field), states that the graph Laplacian of the field equals a source term. The source term is a dipole, a pair of equal and opposite unit charges at the two posting sites, scaled by half the posting magnitude q. The theorem proves this equivalence for any posting magnitude q and any nondegenerate period, meaning the torus has at least two sites in each direction. The weight function in the equation comes from a signed graph that counts every forward and backward posting occurrence, even when periodicity makes their targets coincide.

The theorem's importance lies in what it repairs. An earlier construction, the S8 relation-set graph, stored realized ordered pairs as a set. At period two, forward and backward events on one axis land on the same ordered pair, so the set forgets one occurrence. The signed graph, built by the signedRecognitionProductionGraph3 definition, keeps both occurrences as a multiset. The theorem shows that this multiplicity-preserving graph satisfies the same scaled source equation as the framed six-neighbor operator, with no collision-free hypothesis needed. The pulledBackSignedPostingLaplacian3_eq_framed theorem confirms the graph Laplacian equals the framed operator exactly.

In Recognition Science, this result is a step in the forcing chain that derives physical structure from the cost of recognition. The theorem is proved in the machine-checked library of formal theorems, with no unproved assumptions. It shows that the signed posting source attachment is consistent: for every posting magnitude and every nondegenerate period, the real Green field, the canonical response to a source, satisfies the attachment condition. The theorem does not claim that the signed graph's support differs from the S8 graph's support; the signedGraph_support_eq_recognitionGraph_support theorem states they have identical support, only collision multiplicity differs.

The practical consequence is that the framework's ledger can carry posting events without losing information at period two. The signed graph preserves the minimum-J support, the set of sites where the recognition cost is minimal, while refining the multiplicity. This closes the real posting-source attachment for every posting magnitude and every nondegenerate period, as the signedPostingSourceAttachment3_realGreen theorem confirms. The result is a formal guarantee that the source equation and the posting attachment are two views of the same condition, not separate assumptions.

THEOREM signedPostingSourceAttachment3_iff_scaledSourceEquation · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean
signedPostingSourceAttachment3_iff_scaledSourceEquation · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean:405 
theorem signedPostingSourceAttachment3_iff_scaledSourceEquation
    {N : ℕ} [NeZero N]
    (q : ℝ)
    (event : PostingPair3 N)
    (σ : Equiv.Perm (Fin 3))
    (hevent : event ∈ realizedPrimitivePostingPairs3 N)
    (field : Fin (TorusCard3 N) → ℝ) :
    SignedPostingSourceAttachment3 q event σ field ↔
      ScaledSourceEquation
        (signedRecognitionProductionGraph3 N σ).weight
        (dipole event.1 event.2) (q / 2) field := by
  unfold SignedPostingSourceAttachment3
  rw [and_iff_right hevent]
  simpa [realGreenScaleFromPostingMagnitude] using
    postingMagnitudeActionLaw_iff_scaledSourceEquation
      q (signedRecognitionProductionGraph3 N σ).weight
      field event.1 event.2
      (signedRecognitionProductionGraph3 N σ).weight_symm
MODEL signedRecognitionProductionGraph3 · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean
signedRecognitionProductionGraph3 · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean:154 
/-- Weighted graph obtained from the signed posting-event multiset. -/
def signedRecognitionProductionGraph3
    (N : ℕ) [NeZero N]
    (σ : Equiv.Perm (Fin 3)) :
    WeightedLedgerGraph (TorusCard3 N) where
  weight i j :=
    signedPostingWeight3 σ
      ((torusSiteEquivFin N).symm i)
      ((torusSiteEquivFin N).symm j)
  weight_nonneg i j :=
    signedPostingWeight3_nonneg σ _ _
  weight_symm i j :=
    signedPostingWeight3_symm σ _ _
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 signedGraph_support_eq_recognitionGraph_support · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean
signedGraph_support_eq_recognitionGraph_support · IndisputableMonolith/Foundation/PairKernelSignedPostingTransportS11.lean:220 
/-- The refined signed graph and S8 relation-set graph have identical support
at every period. Only collision multiplicity differs. -/
theorem signedGraph_support_eq_recognitionGraph_support
    {N : ℕ} [NeZero N]
    (σ : Equiv.Perm (Fin 3))
    (i j : Fin (TorusCard3 N)) :
    (signedRecognitionProductionGraph3 N σ).weight i j ≠ 0 ↔
      (recognitionProductionGraph3 N).weight i j ≠ 0 := by
  rw [signedRecognitionProductionGraph3_support_iff]
  constructor
  · intro hrel
    have hmem :
        (i, j) ∈ realizedPrimitivePostingPairs3 N := by
      simpa using hrel
    rw [recognitionProductionGraph3_weight_of_mem hmem]
    norm_num
  · intro hweight
    by_contra hrel
    have hnot :
        (i, j) ∉ realizedPrimitivePostingPairs3 N := by
      simpa using hrel
    rw [recognitionProductionGraph3_weight_of_not_mem hnot] at hweight
    exact hweight rfl

What this page does not claim

The theorem does not claim that the signed graph has a different support than the S8 graph. The theorem does not claim that the posting magnitude q is derived from the framework. The theorem does not claim that the signed graph's Laplacian differs from the framed 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/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