Foundation Pair Kernel Physical Posting Attachment S10 N2 Relation Set Collapses

The two-direction collision

In the Recognition Science framework, a ledger is a discrete record of events, and a posting is one elementary entry in that record. The declaration n2_relationSet_collapses_signedDirectionMultiplicity concerns a small torus with only two sites along each axis. On such a torus, shifting one step forward and one step backward land on the same site, because the torus wraps around. The theorem establishes that a realized posting pair on this two-site torus has a posting multiplicity of 1, meaning it counts as a single relation, while its signed direction multiplicity is 2, meaning the same relation is counted twice, once for the forward direction and once for the backward direction.

The proof is direct. The declaration constructs a specific posting pair, verifies it is realized, and then shows that the two directional counts collide. The key lemma, signedDirectionMultiplicity3_eq_two_at_N2, establishes that for any permutation and any site on the two-site torus, the forward and backward neighbors coincide, so the signed multiplicity is exactly 2. The theorem then packages this with the fact that the posting pair still has multiplicity 1. This is a conditional statement: it holds for the two-site torus, not for larger ones.

What the declaration does not claim is that this collision has a physical meaning. It does not assert that a posting carries the native action quantum, nor that the source coordinate is the action dual. Those identifications are left as explicit predicates, and the library establishes neither. The numerical consequence, that a posting magnitude becomes phi^5, is a conditional theorem that depends on those identifications. The collision itself is a established fact about the two-site torus; its physical interpretation remains open.

In plain terms, the theorem establishes a structural fact: on the smallest torus, the framework's own counting rules produce a double count. This is a precise, machine-checked statement about the ledger's geometry. What it does not do is attach that double count to any physical quantity. The distinction matters because the framework's larger claims depend on making that attachment, and the library is explicit that the attachment is not yet established.

/-- Explicit N=2 countermodel: the S8 relation-set event has multiplicity one,
while the framed operator has two signed direction events landing on the same
neighbor. Any graph/operator pullback theorem must preserve this multiplicity
or assume `3 ≤ N`. -/
theorem n2_relationSet_collapses_signedDirectionMultiplicity :
    ∃ (p q : TorusSite3 2) (event : PostingPair3 2),
      event = (torusSiteEquivFin 2 p, torusSiteEquivFin 2 q) ∧
        event ∈ realizedPrimitivePostingPairs3 2 ∧
        postingPairMultiplicity3 2 event.1 event.2 = 1 ∧
        signedDirectionMultiplicity3
          (Equiv.refl (Fin 3)) p q 0 = 2 := by
  let p : TorusSite3 2 := fun _ => 0
  let q : TorusSite3 2 :=
    framedForward (Equiv.refl (Fin 3)) p 0
  let event : PostingPair3 2 :=
    (torusSiteEquivFin 2 p, torusSiteEquivFin 2 q)
  have hstep :
      FramedAxisStep (Equiv.refl (Fin 3)) p q :=
    ⟨0, Or.inl rfl⟩
  have hgenerated :
      JMinimalGeneratedStep (Equiv.refl (Fin 3)) p q :=
    (jMinimalGeneratedStep_iff_framedAxisStep
      (Equiv.refl (Fin 3)) p q).mpr hstep
  have hevent :
      event ∈ realizedPrimitivePostingPairs3 2 := by
    rw [mem_realizedPrimitivePostingPairs3_iff]
    unfold encodedMinimumJRelation3 event
    simpa using hgenerated
  refine ⟨p, q, event, rfl, hevent,
    realizedPostingPair_multiplicity_one hevent, ?_⟩
  exact
    signedDirectionMultiplicity3_eq_two_at_N2
      (Equiv.refl (Fin 3)) p 0

theorem signedDirectionMultiplicity3_eq_two_at_N2
    (σ : Equiv.Perm (Fin 3))
    (p : TorusSite3 2)
    (k : Fin 3) :
    signedDirectionMultiplicity3 σ p (framedForward σ p k) k = 2 := by
  have hcollision :
      framedForward σ p k = framedBackward σ p k := by
    unfold framedForward framedBackward
    exact torusShift_one_eq_neg_one_at_two p (σ k)
  simp [signedDirectionMultiplicity3, hcollision]

What this page does not claim

The theorem does not assert that any posting carries the native action quantum hbar. The theorem does not identify the source coordinate as the action dual. The theorem does not derive the phi^5 posting magnitude without those identifications.

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/PairKernelPhysicalPostingAttachmentS10.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: