Foundation Pair Kernel Action Extensionality S7 Diagonal Polluted Canonical Sati

The diagonal test

The declaration diagonalPollutedCanonical_satisfies_positiveScaledProductionActionIdentity is not present in the grounding pack. The pack contains a closely related theorem, diagonalPollute_exactJCostAction, which states that adding self-connections (a diagonal pollute) to a weighted ledger graph leaves its exact J-cost action unchanged. This is a ledger, a discrete record of events with weighted connections, and the action is a real-valued function of the graph's weights and a potential field. The theorem proves that for any graph G and any potential ε, the action of the diagonally polluted graph equals the action of the original graph.

This invariance is sharp. A companion theorem, exactJCostAction_determines_loopless_graph, shows that the action does determine the graph uniquely when the graph has no self-connections. The two results together mean that the action can recover all off-diagonal weights, but diagonal weights are invisible to it. The action has a unique loopless representative, while raw graph equality is impossible without a diagonal normalization. In plain terms, the action cannot see self-connections, so any two graphs that differ only in their diagonal weights are indistinguishable by the action.

The pack also proves that the canonical posting graph satisfies the production action identity, which equates its action to a free sum over edge-wise positive realized posting weights. A separate theorem, diagonalPollutedCanonical_violates_actionOnly, shows that the diagonally polluted canonical graph violates a stricter condition called ActionOnlyOnRealizedPostings3. This means the polluted graph does not satisfy the stronger property that the action depends only on realized postings, even though its action equals the original graph's action.

In the framework, the diagonal pollution test demonstrates a precise boundary: the action is blind to self-connections, yet the graph structure itself is not. The theorem establishes that adding self-connections preserves the action, but it does not claim that the polluted graph is identical to the original, nor that it satisfies any stronger structural property. The distinction between action equality and graph equality is the core lesson.

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

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

/-- For a nontrivial carrier, the diagonal-polluted graph violates the
soundness half. Thus action equality alone cannot remove self-loops; the
loopless normalization is logically necessary. -/
theorem diagonalPollutedCanonical_violates_actionOnly
    {N : ℕ} [NeZero N] (hN : 2 ≤ N) :
    ¬ ActionOnlyOnRealizedPostings3
      (diagonalPollute (canonicalPostingGraph3 N)) := by
  intro honly
  let p : TorusSite3 N := fun _ => 0
  have hself := noSelfPrimitivePostings3_of_two_le hN p
  have hz := honly p p hself
  have hcanonical :=
    canonicalPostingGraph3_loopless
      (noSelfPrimitivePostings3_of_two_le hN)
      (torusSiteEquivFin N p)
  simp [diagonalPollute, hcanonical] at hz

What this page does not claim

The declaration diagonalPollutedCanonical_satisfies_positiveScaledProductionActionIdentity itself is not in the grounding pack. The diagonally polluted graph is not claimed to be identical to the original graph, only action-equivalent. The action's blindness to diagonal weights is not claimed to imply that diagonal weights are physically irrelevant.

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: