Encyclopedia Foundation Foundation Pair Kernel Action Extensionality S7

ARTICLE 5 claims 5 theorems

Foundation Pair Kernel Action Extensionality S7

A weighted graph's cost action hides its self-links, yet reveals every connection between distinct points, a sharp result in the Recognition Science framework.

Verify this page

Action determines structure

The module foundation pair kernel action extensionality s7 studies a weighted graph, a collection of points with numbers on the connections between them, through the lens of a cost action, a single number that summarizes the graph's total cost. The central question is whether this action uniquely identifies the graph. The answer is sharp: two graphs with the same action for every possible input must agree on all connections between distinct points, but they may differ freely on the self-connections, the numbers a point assigns to itself.

This is the extensionality principle: the action determines the graph's structure up to its diagonal. The proof uses a family of probe inputs, each one a basis potential that is 1 at a single point and 0 elsewhere. Mixing two such probes isolates the weight of the connection between their two points, recovering it exactly as a multiple of 4 times the weight times (cosh 1 minus 1). The self-connections remain invisible because every term in the action is a difference of potentials, so a constant shift on one point cancels out.

Because the diagonal is invisible, the action cannot distinguish a graph from its diagonal pollute, the graph obtained by changing only the self-connections. Yet the action does determine the graph completely once the diagonal is fixed, for instance by requiring it to be loopless, meaning every self-connection is zero. This yields a clean equivalence: two graphs have identical actions for all inputs if and only if they agree on all off-diagonal connections.

In the Recognition Science framework, this result supports the production action identities, which assert that the action of a production graph equals a sum over primitive posting steps. The module proves that the canonical posting graph, the one with a single unit step between every pair of sites, satisfies these identities. Any loopless graph satisfying the free posting identity must be this canonical graph, while the positive scaled version allows only a global positive scale factor. The existing premises do not force these identities, as the global torus graph, the one with all connections equal, violates them.

The practical consequence is that the action, a scalar summary, carries enough information to reconstruct the graph's off-diagonal structure, and the canonical graph is the unique loopless solution to the production identity. This pins down the graph that the framework's ledger of recognition events must use, up to the harmless freedom of self-connections.

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 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_loopless_graph · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean
exactJCostAction_determines_loopless_graph · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean:261 
/-- The exact action uniquely determines a loopless weighted graph. -/
theorem exactJCostAction_determines_loopless_graph
    {n : ℕ} (G H : WeightedLedgerGraph n)
    (hG : LooplessGraph G) (hH : LooplessGraph H)
    (haction :
      ∀ ε : Fin n → ℝ,
        exactJCostAction G ε = exactJCostAction H ε) :
    G = H := by
  have hweight : G.weight = H.weight := by
    funext i j
    by_cases hij : i = j
    · subst j
      rw [hG i, hH i]
    · exact exactJCostAction_determines_offDiagonal G H haction hij
  cases G with
  | mk weightG weightG_nonneg weightG_symm =>
    cases H with
    | mk weightH weightH_nonneg weightH_symm =>
      simp only at hweight
      subst weightH
      rfl
THEOREM productionActionIdentity_unique_loopless_graph · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean
productionActionIdentity_unique_loopless_graph · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean:825 
/-- Exact-action identity plus the independently necessary loopless
normalization gives uniqueness of the full production graph. -/
theorem productionActionIdentity_unique_loopless_graph
    {N : ℕ} [NeZero N]
    {G : WeightedLedgerGraph (TorusCard3 N)}
    (hself : NoSelfPrimitivePostings3 N)
    (hloop : LooplessGraph G)
    (hidentity : ProductionActionEqualsFreePostingAction3 G) :
    G = canonicalPostingGraph3 N :=
  exactJCostAction_determines_loopless_graph G (canonicalPostingGraph3 N)
    hloop (canonicalPostingGraph3_loopless hself)
    (productionActionIdentity_eq_canonicalAction hidentity)
THEOREM globalTorusGraph3_violates_productionActionIdentity · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean
globalTorusGraph3_violates_productionActionIdentity · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean:1056 
/-- The all-pairs S6 countermodel also violates the action identity. A mixed
basis probe finds an explicit distinct pair which is not a primitive posting
but has coefficient one in the all-pairs graph. -/
theorem globalTorusGraph3_violates_productionActionIdentity :
    ¬ ProductionActionEqualsFreePostingAction3 (globalTorusGraph3 3) := by
  intro hidentity
  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 hz :=
    productionActionIdentity_inactive_distinct_zero
      hidentity p q hpq hinactive
  norm_num [globalTorusGraph3] at hz

What this page does not claim

The action determines the diagonal weights; it does not. The production action identities are forced by the existing premises; they are not, and the global torus graph is a counterexample. The module proves the physical recognition-to-linking bridge; that bridge remains open.

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