Foundation Pair Kernel Production Action Construction S8 Realized Primitive Post

The positive cost of a posting

In the Recognition Science framework, a ledger, a discrete record of events, changes through postings: moves that add a positive amount to one account and subtract the same amount from another. The declaration realizedPrimitivePostingPair_exactJCost_positive proves a plain fact about such a posting: if the posting changes the potential difference between its two accounts, then its cost, measured by the framework's exact J-cost function, is strictly greater than zero. The cost function is J(x) = (x + 1/x)/2 - 1, and for a posting between accounts with potentials ε₁ and ε₂, the cost contribution is cosh(ε₁ - ε₂) - 1, which is zero only when the potentials are equal.

The proof runs inside a machine-checked library of formal theorems and is grounded in a construction, not an assumption. The framework first collects every ordered pair of sites on a finite three-dimensional torus that carries a witnessed minimum-J posting into a finite event batch. Each event in that batch contributes one positive coefficient to a weighted graph, and pairs absent from the batch contribute zero. The declaration then shows that for any event in the batch with a nonzero potential drop, the product of its graph weight (which is 1) and its exact J-cost contribution is strictly positive. The argument reduces to the classical fact that cosh(x) > 1 for x ≠ 0.

This positivity result is a building block, not a standalone claim. It feeds into a larger theorem, recognitionConstruction_productionActionIdentity, which proves that the graph built from the event batch satisfies the identity ProductionActionEqualsPositiveRealizedPostingAction3. That identity, in turn, recovers both support directions: the action lives only on realized postings, and every primitive posting is active. The graph is also loopless and unique: it is the only loopless graph carrying its exact action. The framework's library proves these consequences by theorem, not by an action-identity premise.

What the declaration does not claim is just as important. It does not say that every posting has positive cost; a posting with zero potential drop has zero cost. It does not assert that the event batch is nonempty, only that if an event is in the batch and has a nonzero drop, its cost is positive. And it does not claim that the framework's J-cost function is the only possible cost function; that uniqueness is a separate theorem about the function's form, not about this construction. The declaration is a precise, conditional statement about the cost of a realized posting event, and the framework's library proves it without sorry and without new axioms.

/-- A present event has a strictly positive action coefficient. If its
potential drop is nonzero, its exact nonlinear J-cost contribution is also
strictly positive. -/
theorem realizedPrimitivePostingPair_exactJCost_positive
    {N : ℕ} [NeZero N]
    {e : PostingPair3 N}
    (he : e ∈ realizedPrimitivePostingPairs3 N)
    (ε : Fin (TorusCard3 N) → ℝ)
    (hdrop : ε e.1 - ε e.2 ≠ 0) :
    0 <
      (recognitionProductionGraph3 N).weight e.1 e.2 *
        primitivePostingPairExactJCost3 e ε := by
  rw [recognitionProductionGraph3_weight_of_mem he, one_mul]
  unfold primitivePostingPairExactJCost3
  exact sub_pos.mpr (Real.one_lt_cosh.mpr hdrop)

/-- The live S7 obligation is discharged for the graph built by the
Recognition posting-event constructor. -/
theorem recognitionConstruction_productionActionIdentity
    {N : ℕ} [NeZero N] (hN : 2 ≤ N) :
    ProductionActionEqualsPositiveRealizedPostingAction3
      (recognitionProductionGraph3 N) := by
  let hw :=
    recognitionProductionGraph3_positiveRealizedWeights hN
  refine
    ⟨(recognitionProductionGraph3 N).weight, hw, ?_⟩
  intro ε
  unfold exactJCostAction graphOfPositiveRealizedPostingWeights3
  rfl

/-- Independent uniqueness consequence: the event-fold graph is the unique
loopless graph carrying its exact action. -/
theorem recognitionProductionGraph3_unique_loopless_action_representation
    {N : ℕ} [NeZero N] (hN : 2 ≤ N)
    (G : WeightedLedgerGraph (TorusCard3 N))
    (hloop : LooplessGraph G)
    (haction :
      ∀ ε : Fin (TorusCard3 N) → ℝ,
        exactJCostAction G ε =
          exactJCostAction (recognitionProductionGraph3 N) ε) :
    G = recognitionProductionGraph3 N :=
  exactJCostAction_determines_loopless_graph
    G (recognitionProductionGraph3 N)
    hloop (recognitionProductionGraph3_loopless hN) haction

What this page does not claim

The declaration does not claim that every posting has positive cost, only those with a nonzero potential drop. The declaration does not assert that the event batch is nonempty. The declaration does not prove that the J-cost function is the only possible cost function.

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