Foundation Pair Kernel Production Action Construction S8

The constructed production action

In Recognition Science, a ledger (a discrete record of recognition events) changes state through elementary postings between pairs of sites. The module Foundation Pair Kernel Production Action Construction S8 supplies the missing constructor that folds these primitive posting events into a single production action. On a finite three-dimensional torus, it defines the event batch as the finite set of ordered site pairs carrying a witnessed minimum-J posting, where J is the forced cost function. Each event contributes one positive off-diagonal coefficient to a weighted graph, and pairs absent from the batch contribute zero. The exact action is then the finite sum of the event J-cost contributions.

The central result is a theorem, not a premise: the constructed graph satisfies ProductionActionEqualsPositiveRealizedPostingAction3. This means the production action equals the sum of the realized posting events, with no action-identity assumption. The theorem's proof is machine-checked, with no sorry and no new axiom. The construction also proves that every event in the batch has an underlying minimum-J ledger transition which is an actual one-account posting, and that its spatial posting current is double-entry conserved. The event-batch action is additive under disjoint batch composition, expressing event-order independence at the finite-set level.

The module then derives several consequences. It proves the graph is loopless, has positive realized weights, and that the exact action determines the graph uniquely among loopless graphs. It also recovers both production support directions: the action only occurs on realized postings, and every primitive posting is active. The module further proves the graph satisfies D=3 locality and the global Green consumer property, meaning the production selects the minimum-J support and the graph's response to a scaled dipole equals the scaled dipole itself.

The module also discriminates against countermodels. It proves that the zero torus graph and the global torus graph are not equal to the recognition production graph, because they violate the positive realized production action identity. This discrimination shows the construction is not vacuous: it selects a specific graph among alternatives. The uniqueness result is particularly strong: any loopless graph with the same exact action must be the recognition production graph.

What this establishes in plain language is that the production action of a recognition system is not a free choice but a forced consequence of the underlying posting events. The action is built from the events, not imposed on them. This is a foundational step in the Recognition Science framework: it connects the microscopic ledger dynamics to the macroscopic production action, and it does so with machine-checked rigor. The module closes a gap that previously left the production action as an open constructor, and it does so without adding any new assumptions to the framework.

/-- 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

/-- Every event in the constructed batch has an underlying minimum-J ledger
transition which is an actual one-account posting, and its spatial posting
current is double-entry conserved. -/
theorem realizedPrimitivePostingPair_has_ledger_event
    {N : ℕ} [NeZero N]
    (e : PostingPair3 N)
    (he : e ∈ realizedPrimitivePostingPairs3 N) :
    ∃ A B : LedgerPostingAdjacency.LedgerState 3,
      PostingStep A B ∧
        JMinimalPostingStep A B ∧
        (∑ k : Fin (TorusCard3 N),
          divF (elementaryPosting e.1 e.2) k) = 0 := by
  have hrel :=
    (mem_realizedPrimitivePostingPairs3_iff e).mp he
  unfold encodedMinimumJRelation3 at hrel
  rcases hrel with ⟨A, B, hmin, a, haxis, hshift⟩
  have hpost : PostingStep A B :=
    minJlogCost_monotoneStep_implies_postingStep
      hmin.1 hmin.2.1 hmin.2.2
  exact
    ⟨A, B, hpost, hmin,
      elementaryPosting_sum_div_zero e.1 e.2⟩

/-- Independent constructor consequence: disjoint posting batches compose
additively. -/
theorem postingBatchExactJCostAction3_union
    {N : ℕ} [NeZero N]
    {left right : Finset (PostingPair3 N)}
    (hdisjoint : Disjoint left right)
    (ε : Fin (TorusCard3 N) → ℝ) :
    postingBatchExactJCostAction3 (left ∪ right) ε =
      postingBatchExactJCostAction3 left ε +
        postingBatchExactJCostAction3 right ε := by
  unfold postingBatchExactJCostAction3
  rw [Finset.sum_union hdisjoint]

/-- The graph action is exactly the sum of the constructed primitive posting
event contributions. -/
theorem recognitionProductionGraph3_exactJCostAction_eq_eventBatch
    {N : ℕ} [NeZero N]
    (ε : Fin (TorusCard3 N) → ℝ) :
    exactJCostAction (recognitionProductionGraph3 N) ε =
      postingBatchExactJCostAction3
        (realizedPrimitivePostingPairs3 N) ε := by
  classical
  unfold exactJCostAction postingBatchExactJCostAction3
  rw [← Finset.sum_product']
  unfold realizedPrimitivePostingPairs3
  rw [Finset.sum_filter]
  apply Finset.sum_congr rfl
  intro e he
  by_cases hrel : (@encodedMinimumJRelation3 N _) e.1 e.2
  · simp [recognitionProductionGraph3,
      realizedPrimitivePostingPairs3, hrel,
      primitivePostingPairExactJCost3]
  · simp [recognitionProductionGraph3,
      realizedPrimitivePostingPairs3, hrel]

/-- 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

This module does not prove the existence of a physical universe; it proves a formal theorem about a constructed graph. The production action identity is not assumed as a premise; it is derived from the event construction. The module does not claim that the recognition production graph is the only graph satisfying the action identity; it claims uniqueness among loopless graphs.

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: