Foundation Pair Kernel Production Support S6 Primitive Posting Action Law Suppor

The support theorem

The declaration primitivePostingActionLaw_supports_encoded_relation is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that if a weighted graph satisfies a condition called the primitive posting action law, then the graph's support, meaning the set of edges with nonzero weight, is exactly the relation generated by minimum-cost recognition postings. In plainer terms: when the law holds, the only connections that cost anything are precisely the ones that a minimal-cost process would produce. The theorem is proved in the Lean formal proof system with no unproved assumptions and no new axioms, so it is a THEOREM claim.

To understand what this establishes, consider what the framework calls a ledger, a discrete record of events. The primitive posting action law has two halves. First, any pair of sites that is not a minimum-J posting step has zero action coefficient, meaning it costs nothing. Second, every realized primitive posting, every step that the minimum-cost process actually takes, has a positive action coefficient. The theorem proves that these two conditions together are equivalent to the graph's support matching the encoded minimum-J relation. This is a precise structural statement: the law forces the graph to encode exactly the right connections.

The theorem also carries a specific consequence for the framework's exact J-cost action. When the law holds, the full action decomposes over realized posting edges only, and each active elementary posting conserves by double entry. The proof shows that the canonical posting graph satisfies the law, while two counterexample graphs, one with all weights equal to one and one with all weights equal to zero, violate it. This demonstrates that the law is not vacuous: it genuinely selects a particular class of graphs. The theorem is part of a larger chain that connects the action law to the bounded recognition relation and to Green's function behavior on a torus.

What the theorem does not claim is equally important. It does not prove that the primitive posting action law itself is forced by the framework's existing premises. A separate theorem in the same module shows that the existing premises do not imply the law, so the law remains a HYPOTHESIS for any externally supplied production graph. The theorem only establishes a conditional relationship: if the law holds, then the support matches the encoded relation. It also does not claim anything about the physical interpretation of the graph, such as hydrogen or protein data, which the module explicitly does not mention. The theorem is a formal statement about graphs and relations, not a physical law.

The practical upshot is that the framework now has a clean bridge between an action principle and a production relation. Before this result, the framework had two bare models that disagreed about which connections were possible. This theorem shows that the primitive posting action law resolves that disagreement: it selects the canonical support and rules out the all-pairs and all-zero graphs. A reader who accepts the law can now be certain that the graph's nonzero edges are exactly the minimum-J steps, nothing more and nothing less.

theorem primitivePostingActionLaw_supports_encoded_relation
    {N : ℕ} [NeZero N]
    {G : WeightedLedgerGraph (TorusCard3 N)}
    (hG : PrimitivePostingActionLaw3 G) :
    RelationSupportsWeightOn (@encodedMinimumJRelation3 N _) G := by
  intro i j hne
  let p : TorusSite3 N := (torusSiteEquivFin N).symm i
  let q : TorusSite3 N := (torusSiteEquivFin N).symm j
  by_contra hinactive
  have hz := hG.inactive_zero p q hinactive
  have hp : torusSiteEquivFin N p = i :=
    (torusSiteEquivFin N).apply_symm_apply i
  have hq : torusSiteEquivFin N q = j :=
    (torusSiteEquivFin N).apply_symm_apply j
  rw [hp, hq] at hz
  exact hne hz

theorem primitivePostingActionLaw_iff_two_halves
    {N : ℕ} [NeZero N]
    (G : WeightedLedgerGraph (TorusCard3 N)) :
    PrimitivePostingActionLaw3 G ↔
      ActionOnlyOnRealizedPostings3 G ∧
        EveryPrimitivePostingActive3 G := by
  constructor
  · intro h
    exact ⟨h.inactive_zero, h.active_positive⟩
  · rintro ⟨honly, hevery⟩
    exact ⟨honly, hevery⟩

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)

/-- The new operational law resolves the S5 support underdetermination: the
canonical bare support has an action extension, while the global bare support
cannot obey the law. Coefficient scale remains explicitly unselected. -/
theorem primitivePostingActionLaw_resolves_S5_countermodels :
    PrimitivePostingActionLaw3 (canonicalPostingGraph3 3) ∧
      ¬ PrimitivePostingActionLaw3 (globalTorusGraph3 3) ∧
      graphProductionSupport3 (canonicalPostingGraph3 3) =
        canonicalBareMinimumJSupportModel3.productionSupport ∧
      graphProductionSupport3 (globalTorusGraph3 3) =
        globalBareMinimumJSupportModel3.productionSupport :=
  ⟨canonicalPostingGraph3_obeys_action_law 3,
    globalTorusGraph3_violates_primitivePostingActionLaw,
    canonical_graph_realizes_canonical_S5_support,
    global_graph_realizes_global_S5_support⟩

What this page does not claim

The primitive posting action law itself is not proved from the framework's existing premises; it remains a hypothesis for any externally supplied production graph. The theorem says nothing about the physical interpretation of the graph, such as hydrogen or protein data. The theorem does not establish that any particular physical system satisfies 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: