Foundation Pair Kernel Production Support S6 Existing Premises Do Not Force Prim

A boundary result

The Recognition Science framework models reality as a ledger, a discrete record of events, where each possible event has a weight. A central question is which events actually occur. The earlier stage of the framework, called S5, left this open: it assumed that the realized events are exactly those with minimal cost, but it did not connect that assumption to the weights that define the ledger's action.

That gap is now closed in a precise, limited way. The machine-checked library of formal theorems proves existing_premises_do_not_force_primitivePostingActionLaw. In plain language: the assumptions available before this stage do not, by themselves, force the rule that only minimal-cost postings have nonzero weight. The theorem exhibits a specific counterexample, a graph where every pair of sites is connected with weight 1, that satisfies all the earlier premises but violates the proposed law. This is a formal independence result, not a gap in reasoning.

The proposed law itself, PrimitivePostingActionLaw3, has two halves: an inactive pair, one not realized by a minimal-cost posting, must have zero weight; and an active primitive posting must have positive weight. The library proves that the canonical graph satisfies both halves, and that the law is equivalent to the conjunction of these two conditions. It also proves that the exact cost action decomposes over realized posting edges only, and that active elementary postings conserve by double entry.

In Recognition Science, this result does not claim that the law is true. It remains an honest hypothesis for an externally supplied production graph. The theorem only establishes that the earlier premises are insufficient; it does not prove the law itself, nor does it say which graph is the correct one.

theorem existing_premises_do_not_force_primitivePostingActionLaw :
    ¬ (∀ G : WeightedLedgerGraph (TorusCard3 3),
      ExistingActionLedgerPremises3 G →
        PrimitivePostingActionLaw3 G) := by
  intro hforce
  exact globalTorusGraph3_violates_primitivePostingActionLaw
    (hforce (globalTorusGraph3 3)
      globalTorusGraph3_satisfies_existing_premises)

theorem globalTorusGraph3_violates_primitivePostingActionLaw :
    ¬ PrimitivePostingActionLaw3 (globalTorusGraph3 3) := by
  intro hLaw
  exact globalTorusGraph3_violates_actionOnlyOnRealized
    hLaw.inactive_zero

theorem globalTorusGraph3_satisfies_existing_premises :
    ExistingActionLedgerPremises3 (globalTorusGraph3 3) :=
  existingActionLedgerPremises_all_graphs (globalTorusGraph3 3)

/-- **S6 operational factorization of the missing arrow (HYPOTHESIS for an
externally supplied graph).**

An action coefficient records a primitive realized posting: unrealized pairs
contribute zero and realized primitive pairs contribute positively. The law
does not choose a coefficient scale; the committed source-coupling
countermodel already proves that posting integrality does not fix that scale. -/
structure PrimitivePostingActionLaw3
    {N : ℕ} [NeZero N]
    (G : WeightedLedgerGraph (TorusCard3 N)) : Prop where
  inactive_zero :
    ∀ p q : TorusSite3 N,
      ¬ JMinimalGeneratedStep (Equiv.refl (Fin 3)) p q →
        G.weight (torusSiteEquivFin N p) (torusSiteEquivFin N q) = 0
  active_positive :
    ∀ p q : TorusSite3 N,
      JMinimalGeneratedStep (Equiv.refl (Fin 3)) p q →
        0 < G.weight (torusSiteEquivFin N p) (torusSiteEquivFin N q)

theorem canonicalPostingGraph3_obeys_action_law
    (N : ℕ) [NeZero N] :
    PrimitivePostingActionLaw3 (canonicalPostingGraph3 N) := by
  constructor
  · intro p q h
    simp [canonicalPostingGraph3, h]
  · intro p q h
    simp [canonicalPostingGraph3, h]

/-- **S6 operational factorization of the missing arrow (HYPOTHESIS for an
externally supplied graph).**

An action coefficient records a primitive realized posting: unrealized pairs
contribute zero and realized primitive pairs contribute positively. The law
does not choose a coefficient scale; the committed source-coupling
countermodel already proves that posting integrality does not fix that scale. -/
structure PrimitivePostingActionLaw3
    {N : ℕ} [NeZero N]
    (G : WeightedLedgerGraph (TorusCard3 N)) : Prop where
  inactive_zero :
    ∀ p q : TorusSite3 N,
      ¬ JMinimalGeneratedStep (Equiv.refl (Fin 3)) p q →
        G.weight (torusSiteEquivFin N p) (torusSiteEquivFin N q) = 0
  active_positive :
    ∀ p q : TorusSite3 N,
      JMinimalGeneratedStep (Equiv.refl (Fin 3)) p q →
        0 < G.weight (torusSiteEquivFin N p) (torusSiteEquivFin N q)

What this page does not claim

The primitive posting action law is true for all graphs. The earlier premises are inconsistent or contradictory. The canonical graph is the only graph satisfying the law.

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