Encyclopedia Foundation Foundation Pair Kernel Action Extensionality S7 Positive Realized Production Act

ARTICLE 5 claims 5 theorems

Foundation Pair Kernel Action Extensionality S7 Positive Realized Production Act

In the Recognition Science framework, a single equation about production costs determines which connections between entities are real, and which are merely artifacts of the bookkeeping.

Verify this page

The action identity

In the Recognition Science framework, a ledger (a discrete record of events) tracks connections between entities as weighted links in a graph. The framework's central cost function, J(x) = (x + 1/x)/2 - 1, assigns a recognition cost to each configuration. The question at hand is: given the total cost of a configuration, can you recover the underlying graph uniquely? The answer is no, not fully. The cost function is blind to self-connections, the diagonal entries of the graph, because every cost term involves a difference between two potentials. You can change a node's self-weight arbitrarily without changing the total cost at all.

What the cost does determine, sharply, is every off-diagonal connection. A theorem in the framework's machine-checked library of formal theorems proves that if two graphs have the same total cost for every possible potential assignment, then all their off-diagonal weights are equal. A separate theorem shows the converse: if all off-diagonal weights match, the total costs match. So the cost function pins down the entire graph except for the diagonal, which is invisible. This is the extensionality result: the action determines the loopless graph, and only the loopless graph.

The declaration named positiveRealizedProductionActionIdentity_derives_both_support_directions packages this into a production setting. It says: if a graph's production action equals a free sum over positive realized posting weights, then two support directions follow. First, the graph is loopless, meaning no self-connections. Second, the graph satisfies the primitive posting action law, a structural condition on which links are allowed. The declaration compiles these two consequences from the identity plus a loopless assumption. It is a theorem in the library, proved without axioms beyond the standard three.

What this does not claim is just as important. The identity does not force a unique graph. A graph that satisfies it is not necessarily the canonical posting graph; it could be any positive scaling of it. The declaration does not say that the production action identity holds for all graphs, or even for all graphs satisfying the existing premises. In fact, the library contains a counterexample: the global torus graph satisfies the existing premises but violates the identity. So the identity is a substantive additional condition, not a consequence of what came before.

The practical upshot is a division of labor. The cost function tells you everything about how entities interact, and nothing about how they stand alone. To recover the full graph, you need a normalization rule for the diagonal. The production identity supplies that rule in a specific form, and the framework proves what that rule buys you. The diagonal remains a modeling choice, not a derived fact.

THEOREM diagonalPollute_exactJCostAction · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean
diagonalPollute_exactJCostAction · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean:304 
/-- Diagonal pollution leaves the full exact action unchanged. -/
theorem diagonalPollute_exactJCostAction
    {n : ℕ} (G : WeightedLedgerGraph n)
    (ε : Fin n → ℝ) :
    exactJCostAction (diagonalPollute G) ε =
      exactJCostAction G ε := by
  apply exactJCostAction_eq_of_offDiagonal
  intro i j hij
  simp [diagonalPollute, hij]
THEOREM exactJCostAction_determines_offDiagonal · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean
exactJCostAction_determines_offDiagonal · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean:193 
/-- Equality of the exact action on all potentials determines every
off-diagonal coefficient. -/
theorem exactJCostAction_determines_offDiagonal
    {n : ℕ} (G H : WeightedLedgerGraph n)
    (haction :
      ∀ ε : Fin n → ℝ,
        exactJCostAction G ε = exactJCostAction H ε)
    {a b : Fin n} (hab : a ≠ b) :
    G.weight a b = H.weight a b := by
  have hG := exactJCostAction_mixed_basis_probe G a b hab
  have hH := exactJCostAction_mixed_basis_probe H a b hab
  have hprobe :
      4 * G.weight a b * (Real.cosh 1 - 1) =
        4 * H.weight a b * (Real.cosh 1 - 1) := by
    calc
      4 * G.weight a b * (Real.cosh 1 - 1) =
          exactJCostAction G (basisPotential a) +
            exactJCostAction G (basisPotential b) -
            exactJCostAction G
              (fun i => basisPotential a i + basisPotential b i) :=
        hG.symm
      _ =
          exactJCostAction H (basisPotential a) +
            exactJCostAction H (basisPotential b) -
            exactJCostAction H
              (fun i => basisPotential a i + basisPotential b i) := by
        rw [haction (basisPotential a), haction (basisPotential b),
          haction (fun i => basisPotential a i + basisPotential b i)]
      _ = 4 * H.weight a b * (Real.cosh 1 - 1) := hH
  have hcosh : 0 < Real.cosh (1 : ℝ) - 1 :=
    sub_pos.mpr (Real.one_lt_cosh.mpr (by norm_num))
  nlinarith
THEOREM exactJCostAction_eq_of_offDiagonal · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean
exactJCostAction_eq_of_offDiagonal · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean:226 
/-- Off-diagonal coefficient agreement is also sufficient for exact-action
agreement. Diagonal coefficients never contribute. -/
theorem exactJCostAction_eq_of_offDiagonal
    {n : ℕ} (G H : WeightedLedgerGraph n)
    (hweight :
      ∀ i j : Fin n, i ≠ j → G.weight i j = H.weight i j)
    (ε : Fin n → ℝ) :
    exactJCostAction G ε = exactJCostAction H ε := by
  unfold exactJCostAction
  apply Finset.sum_congr rfl
  intro i _
  apply Finset.sum_congr rfl
  intro j _
  by_cases hij : i = j
  · subst j
    simp
  · rw [hweight i j hij]
THEOREM positiveRealizedProductionActionIdentity_primitivePostingActionLaw · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean
positiveRealizedProductionActionIdentity_primitivePostingActionLaw · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean:796 
theorem positiveRealizedProductionActionIdentity_primitivePostingActionLaw
    {N : ℕ} [NeZero N]
    {G : WeightedLedgerGraph (TorusCard3 N)}
    (hN : 2 ≤ N)
    (hloop : LooplessGraph G)
    (hidentity : ProductionActionEqualsPositiveRealizedPostingAction3 G) :
    PrimitivePostingActionLaw3 G :=
  (primitivePostingActionLaw_iff_two_halves G).mpr
    (positiveRealizedProductionActionIdentity_derives_both_of_two_le
      hN hloop hidentity)
THEOREM globalTorusGraph3_violates_positiveRealizedProductionActionIdentity · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean
globalTorusGraph3_violates_positiveRealizedProductionActionIdentity · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean:1008 
/-- The all-pairs S6 countermodel violates the weakest edge-wise positive
realized action identity: a mixed basis probe recovers a nonzero inactive
coefficient. -/
theorem globalTorusGraph3_violates_positiveRealizedProductionActionIdentity :
    ¬ ProductionActionEqualsPositiveRealizedPostingAction3
      (globalTorusGraph3 3) := by
  intro hidentity
  rcases hidentity with ⟨w, hw, haction⟩
  let p : TorusSite3 3 := fun _ => 0
  let q : TorusSite3 3 :=
    fun i => if i = (0 : Fin 3) ∨ i = (1 : Fin 3) then 1 else 0
  have hpq : p ≠ q := by
    intro hpq
    have h0 := congrFun hpq (0 : Fin 3)
    norm_num [p, q] at h0
  have hinactive :
      ¬ JMinimalGeneratedStep (Equiv.refl (Fin 3)) p q := by
    rw [jMinimalGeneratedStep_iff_framedAxisStep]
    intro hstep
    rcases hstep with ⟨k, hk | hk⟩
    · fin_cases k
      all_goals
        have h0 := congrFun hk 0
        have h1 := congrFun hk 1
        simp [p, q, framedForward, torusShift] at h0 h1
    · fin_cases k
      all_goals
        have h0 := congrFun hk 0
        have h1 := congrFun hk 1
        simp [p, q, framedBackward, torusShift] at h0 h1
  have hij :
      torusSiteEquivFin 3 p ≠ torusSiteEquivFin 3 q :=
    (torusSiteEquivFin 3).injective.ne hpq
  have hcoeff :=
    exactJCostAction_determines_offDiagonal (globalTorusGraph3 3)
      (graphOfPositiveRealizedPostingWeights3 hw) haction hij
  have hinactive' :
      ¬ (@encodedMinimumJRelation3 3 _)
        (torusSiteEquivFin 3 p) (torusSiteEquivFin 3 q) := by
    simpa [encodedMinimumJRelation3,
      (torusSiteEquivFin 3).symm_apply_apply,
      (torusSiteEquivFin 3).symm_apply_apply] using hinactive
  have hz := hw.inactive_zero _ _ hinactive'
  have hzero : (1 : ℝ) = 0 := by
    simpa [globalTorusGraph3, graphOfPositiveRealizedPostingWeights3, hz]
      using hcoeff
  exact (by norm_num : (1 : ℝ) ≠ 0) hzero

What this page does not claim

The production identity does not force a unique graph; it allows any positive scaling of the canonical graph. The identity does not hold for all graphs satisfying the existing premises; the global torus graph is a counterexample. The framework does not derive the diagonal normalization from the cost function alone.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND