Foundation Pair Kernel Production Support S6 Active Primitive Posting Positive A

Active postings and their ledger

In the Recognition Science framework, reality is modeled as maintaining a ledger, a discrete record of events. Each event is a posting between two sites, and the framework's central cost function J assigns a price to every possible posting. The declaration active_primitive_posting_positive_and_conserved is a theorem about a specific kind of posting: a primitive posting, one that is generated by a minimal-cost step. The theorem states two things about such an active posting. First, its action coefficient, the weight the framework assigns to it, is strictly positive. Second, the posting conserves by double entry: the sum of its effects across all sites in the ledger is exactly zero.

The theorem is proved for any weighted ledger graph that satisfies the PrimitivePostingActionLaw3. This law itself is a conjunction of two halves. The first half, ActionOnlyOnRealizedPostings3, says that a pair of sites not connected by a minimal-cost step has a zero action coefficient. The second half, EveryPrimitivePostingActive3, says that every pair connected by such a step has a strictly positive coefficient. The theorem active_primitive_posting_positive_and_conserved takes the second half as its hypothesis and derives the positivity, and it takes the conservation of elementary postings as a separate premise to derive the double-entry balance. The machine-checked library proves these results for the canonical posting graph, which satisfies the full law.

The declaration also resolves a gap left by an earlier stage of the framework. Previous premises did not force the law: a graph where every pair of sites is connected, and a graph where no pair is connected, both satisfied the old premises, yet neither obeys the new law. The new law selects the canonical graph as the one that realizes the intended production support, and it proves that the exact J-cost action decomposes over realized posting edges only. This means the framework's action, its measure of total cost, is built only from postings that actually happen, not from all possible ones.

What the declaration does not claim is just as important. It does not claim that the law holds for any externally supplied production graph; that remains an open hypothesis. It does not mention any specific physical system, such as hydrogen or a protein, nor does it involve a range predicate or Green's function behavior. The theorem is a structural result about the ledger, not a statement about any particular material. It establishes the consistency of a model where active postings are both costly and balanced, a combination that is not forced by the framework's earlier axioms alone.

/-- Combined active-edge readout. Positivity is the completeness half of the
new hypothesis. Conservation is an independent pre-existing Gauss theorem,
included here to show that selected active edges retain double-entry
semantics. -/
theorem active_primitive_posting_positive_and_conserved
    {N : ℕ} [NeZero N]
    {G : WeightedLedgerGraph (TorusCard3 N)}
    (hG : PrimitivePostingActionLaw3 G)
    (p q : TorusSite3 N)
    (hactive :
      JMinimalGeneratedStep (Equiv.refl (Fin 3)) p q) :
    0 < G.weight (torusSiteEquivFin N p) (torusSiteEquivFin N q) ∧
      ∑ i : Fin (TorusCard3 N),
        divF
          (elementaryPosting
            (torusSiteEquivFin N p)
            (torusSiteEquivFin N q)) i = 0 :=
  ⟨hG.active_positive p q hactive,
    elementaryPosting_sum_div_zero
      (torusSiteEquivFin N p) (torusSiteEquivFin N q)⟩

/-- No action coefficient lies on a pair that is not realized by a
minimum-J posting. This is the support-soundness half of the S5 arrow. -/
def ActionOnlyOnRealizedPostings3
    {N : ℕ} [NeZero N]
    (G : WeightedLedgerGraph (TorusCard3 N)) : Prop :=
  ∀ p q : TorusSite3 N,
    ¬ JMinimalGeneratedStep (Equiv.refl (Fin 3)) p q →
      G.weight (torusSiteEquivFin N p) (torusSiteEquivFin N q) = 0

/-- Every realizable primitive minimum-J posting has a positive action
coefficient. This is the support-completeness half of the S5 arrow. -/
def EveryPrimitivePostingActive3
    {N : ℕ} [NeZero N]
    (G : WeightedLedgerGraph (TorusCard3 N)) : Prop :=
  ∀ 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]

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)

What this page does not claim

The primitive posting action law is not proved for any externally supplied production graph. The theorem does not mention hydrogen, proteins, or any other specific physical system. The declaration does not establish that all postings are active, only that active ones are positive and conserved.

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: