Encyclopedia Foundation Foundation Pair Kernel Action Extensionality S7 Existing Premises Do Not Force P

ARTICLE 4 claims 4 theorems

Foundation Pair Kernel Action Extensionality S7 Existing Premises Do Not Force P

A machine-checked theorem shows the framework's current assumptions leave a key production identity undecided, and names a concrete graph that escapes it.

Verify this page

What the premises do not force

In the Recognition Science framework, a ledger is a discrete record of events, and a cost is a number assigned to a transition between two ledger states. The framework's library, a machine-checked collection of formal theorems, asks which properties of a ledger graph are determined by its cost function alone. One sharp answer is already proved: the cost function determines all off-diagonal weights of a graph, those connecting distinct entries, but it cannot see the diagonal weights, the self-connections. Two graphs that differ only on their diagonal produce the same cost for every possible input, so raw graph equality is impossible without an extra normalization rule.

The declaration existing_premises_do_not_force_positiveRealizedProductionActionIdentity addresses a different question: whether the framework's current assumptions, the ExistingActionLedgerPremises3, are strong enough to force a particular production identity to hold for every graph. That identity, ProductionActionEqualsPositiveRealizedPostingAction3, says the total production cost of a graph equals a free sum over edge-wise positive realized posting weights, with independent per-edge scales. The theorem answers in the negative: it proves that these premises do not force the identity. The proof exhibits a concrete counterexample, a graph called globalTorusGraph3, which satisfies all the existing premises yet violates the identity. This is a non-trivial result, not a gap in the library; it is a proved statement about the limits of the current assumptions.

The theorem's meaning is constructive for the framework's development. It shows that if the production identity is desired as a general law, the current premises are insufficient and a new premise must be added. The theorem does not say the identity is false, only that it is not forced. It also does not say the identity is true for the canonical graph; in fact, the canonical graph does satisfy the identity, and a separate theorem proves that any loopless graph satisfying the identity must be a positive scaling of that canonical graph. The negative result therefore sharpens the search: the identity is a strong structural condition, and the existing premises do not yet single it out.

For a reader outside the framework, the takeaway is a lesson about formal systems. A set of axioms can be consistent and still underdetermine a property you care about. The framework's library does not paper over this; it records the underdetermination as a proved theorem, with a named witness. This is the opposite of a hidden assumption: it is an explicit map of where the current theory is silent, and a precise target for the next premise.

THEOREM exactJCostAction_determines_offDiagonal · diagonalPollute_exactJCostAction · 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
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 existing_premises_do_not_force_positiveRealizedProductionActionIdentity · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean
existing_premises_do_not_force_positiveRealizedProductionActionIdentity · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean:1126 
/-- The graph-independent exact-action, Gauss, source, and Pi-free premises
isolated in S6 do not force the weakest edge-wise positive realized action
identity. -/
theorem existing_premises_do_not_force_positiveRealizedProductionActionIdentity :
    ¬ (∀ G : WeightedLedgerGraph (TorusCard3 3),
      ExistingActionLedgerPremises3 G →
        ProductionActionEqualsPositiveRealizedPostingAction3 G) := by
  intro hforce
  exact globalTorusGraph3_violates_positiveRealizedProductionActionIdentity
    (hforce (globalTorusGraph3 3)
      globalTorusGraph3_satisfies_existing_premises)
THEOREM globalTorusGraph3_violates_positiveRealizedProductionActionIdentity · existing_premises_do_not_force_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
existing_premises_do_not_force_positiveRealizedProductionActionIdentity · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean:1126 
/-- The graph-independent exact-action, Gauss, source, and Pi-free premises
isolated in S6 do not force the weakest edge-wise positive realized action
identity. -/
theorem existing_premises_do_not_force_positiveRealizedProductionActionIdentity :
    ¬ (∀ G : WeightedLedgerGraph (TorusCard3 3),
      ExistingActionLedgerPremises3 G →
        ProductionActionEqualsPositiveRealizedPostingAction3 G) := by
  intro hforce
  exact globalTorusGraph3_violates_positiveRealizedProductionActionIdentity
    (hforce (globalTorusGraph3 3)
      globalTorusGraph3_satisfies_existing_premises)
THEOREM canonicalPostingGraph3_satisfies_positiveRealizedProductionActionIdentity · positiveScaledProductionActionIdentity_unique_loopless_graph · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean
canonicalPostingGraph3_satisfies_positiveRealizedProductionActionIdentity · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean:768 
/-- Canonical free posting inhabits the weakest edge-wise positive action
identity once self-postings are excluded. -/
theorem canonicalPostingGraph3_satisfies_positiveRealizedProductionActionIdentity
    {N : ℕ} [NeZero N]
    (hself : NoSelfPrimitivePostings3 N) :
    ProductionActionEqualsPositiveRealizedPostingAction3
      (canonicalPostingGraph3 N) := by
  refine ⟨(canonicalPostingGraph3 N).weight,
    canonicalPostingGraph3_positiveRealizedWeights hself, ?_⟩
  intro ε
  unfold exactJCostAction
  apply Finset.sum_congr rfl
  intro i _
  apply Finset.sum_congr rfl
  intro j _
  simp [graphOfPositiveRealizedPostingWeights3]
positiveScaledProductionActionIdentity_unique_loopless_graph · IndisputableMonolith/Foundation/PairKernelActionExtensionalityS7.lean:879 
/-- Under the independently necessary loopless normalization, the
scale-free identity uniquely recovers the full production graph up to one
common strictly positive scale. -/
theorem positiveScaledProductionActionIdentity_unique_loopless_graph
    {N : ℕ} [NeZero N]
    {G : WeightedLedgerGraph (TorusCard3 N)}
    (hself : NoSelfPrimitivePostings3 N)
    (hloop : LooplessGraph G)
    (hscaled :
      ProductionActionEqualsPositiveScaledFreePostingAction3 G) :
    ∃ κ : ℝ, ∃ hκ : 0 < κ,
      G = nonnegativeScaleGraph κ hκ.le
        (canonicalPostingGraph3 N) := by
  rcases hscaled with ⟨κ, hκ, hidentity⟩
  refine ⟨κ, hκ, ?_⟩
  exact
    exactJCostAction_determines_loopless_graph G
      (nonnegativeScaleGraph κ hκ.le (canonicalPostingGraph3 N))
      hloop
      (nonnegativeScaleGraph_loopless κ hκ.le
        (canonicalPostingGraph3_loopless hself))
      (positiveScaledProductionActionIdentity_eq_scaledCanonicalAction
        hκ hidentity)

What this page does not claim

The theorem does not claim the production identity is false; it only shows the existing premises do not force it. The theorem does not claim the framework is inconsistent; it is a proved statement within it. The theorem does not claim the cost function determines all graph structure; diagonal weights remain invisible without normalization.

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