Encyclopedia Foundation Foundation Pair Kernel Canonical Generator Source S9 Twice Laplacian Action Norm

ARTICLE 5 claims 5 theorems

Foundation Pair Kernel Canonical Generator Source S9 Twice Laplacian Action Norm

A machine-checked theorem shows that a single unit posting in the framework's discrete ledger produces a response field whose Laplacian is exactly half the posting, fixing a canonical scale without fitting any number.

Verify this page

The normalized response

In the Recognition Science framework, a ledger is a discrete record of events, and a posting is a single elementary event that adds one unit at its source and removes one unit at its sink. The declaration twice_laplacian_actionNormalizedGreenResponse3 is a theorem about the response field generated by such a posting on a three-dimensional torus. It states that twice the Laplacian of the normalized response equals the posting itself, written in symbols as 2 * framedTorusLaplacian(response) = postingMagnitudeTorusSource. This is a precise identity: the response field, when acted on by the Laplacian, reproduces the original posting scaled by one half.

The factor of one half is not arbitrary. The framework's action, the quantity that assigns a cost to a field configuration, has a first variation equal to twice the Laplacian. Because of that convention, a posting of magnitude q solves the Green equation with right-hand coefficient q/2. For the primitive posting of magnitude 1, the canonical Green source scale is exactly 1/2. The theorem actionNormalizedGreenResponse3_solves proves that the response field satisfies the Laplacian equation, and twice_actionNormalizedGreenSource3 proves the doubling identity for the source; the main theorem combines these two results.

The result is relative to the ledger action unit. A later physical conversion may assign a dimensional magnitude to one ledger posting; that magnitude remains an explicit parameter and is divided by two by the same theorem. No hydrogen atom, no benchmark datum, and no fitted number appears in this declaration. The theorem is machine-checked: the framework's library of formal theorems contains no unfinished proofs and no new axioms for this result.

What the theorem does not claim is equally important. It does not assign a physical size to a posting, nor does it derive any measured constant. It does not say that the response field is unique; other fields may satisfy the same equation. It only establishes the exact algebraic relationship between a posting and its normalized response under the framework's action convention.

THEOREM twice_laplacian_actionNormalizedGreenResponse3 · IndisputableMonolith/Foundation/PairKernelCanonicalGeneratorSourceS9.lean
twice_laplacian_actionNormalizedGreenResponse3 · IndisputableMonolith/Foundation/PairKernelCanonicalGeneratorSourceS9.lean:400 
/-- The Green response obeys the unit-posting action equation after multiplying
the Laplacian by the action variation coefficient `2`. -/
theorem twice_laplacian_actionNormalizedGreenResponse3
    {N : ℕ} [NeZero N]
    (hN : 2 ≤ N)
    (q : ℂ) (event : PostingPair3 N)
    (σ : Equiv.Perm (Fin 3))
    (p : TorusSite3 N) :
    2 * framedTorusLaplacian σ
        (actionNormalizedGreenResponse3 q event) p =
      postingMagnitudeTorusSource3 q event p := by
  rw [actionNormalizedGreenResponse3_solves hN]
  exact twice_actionNormalizedGreenSource3 q event p
THEOREM actionNormalizedGreenResponse3_solves · twice_actionNormalizedGreenSource3 · IndisputableMonolith/Foundation/PairKernelCanonicalGeneratorSourceS9.lean
actionNormalizedGreenResponse3_solves · IndisputableMonolith/Foundation/PairKernelCanonicalGeneratorSourceS9.lean:385 
theorem actionNormalizedGreenResponse3_solves
    {N : ℕ} [NeZero N]
    (hN : 2 ≤ N)
    (q : ℂ) (event : PostingPair3 N)
    (σ : Equiv.Perm (Fin 3))
    (p : TorusSite3 N) :
    framedTorusLaplacian σ
        (actionNormalizedGreenResponse3 q event) p =
      actionNormalizedGreenSource3 q event p := by
  exact
    (recognitionConstruction_globalGreen_consumer
      hN σ (greenScaleFromPostingMagnitude q)
      (postingEventSourceSite3 event)
      (postingEventSinkSite3 event) p).2.2
twice_actionNormalizedGreenSource3 · IndisputableMonolith/Foundation/PairKernelCanonicalGeneratorSourceS9.lean:376 
theorem twice_actionNormalizedGreenSource3
    {N : ℕ} [NeZero N]
    (q : ℂ) (event : PostingPair3 N) (p : TorusSite3 N) :
    2 * actionNormalizedGreenSource3 q event p =
      postingMagnitudeTorusSource3 q event p := by
  unfold actionNormalizedGreenSource3 postingMagnitudeTorusSource3
    greenScaleFromPostingMagnitude scaledTorusDipole
  ring
THEOREM sourceScale_eq_half_postingMagnitude · IndisputableMonolith/Foundation/PairKernelCanonicalGeneratorSourceS9.lean
sourceScale_eq_half_postingMagnitude · IndisputableMonolith/Foundation/PairKernelCanonicalGeneratorSourceS9.lean:277 
/-- If the same nontrivial source field is presented with a free source
scale, action compatibility determines that scale uniquely as `q / 2`. -/
theorem sourceScale_eq_half_postingMagnitude
    {n : ℕ}
    (q sourceScale : ℝ)
    (w : Fin n → Fin n → ℝ)
    (e : Fin n → ℝ)
    (a b : Fin n)
    (hab : a ≠ b)
    (hsymm : ∀ i j, w i j = w j i)
    (haction : PostingMagnitudeActionLaw q w e a b)
    (hsource :
      ScaledSourceEquation w (dipole a b) sourceScale e) :
    sourceScale = realGreenScaleFromPostingMagnitude q := by
  unfold realGreenScaleFromPostingMagnitude
  have hhalf :=
    (postingMagnitudeActionLaw_iff_scaledSourceEquation
      q w e a b hsymm).mp haction
  have hs := hsource a
  have hh := hhalf a
  simp [dipole, hab, realGreenScaleFromPostingMagnitude] at hs hh
  exact hs.symm.trans hh
THEOREM twice_laplacian_actionNormalizedGreenResponse3 · IndisputableMonolith/Foundation/PairKernelCanonicalGeneratorSourceS9.lean
twice_laplacian_actionNormalizedGreenResponse3 · IndisputableMonolith/Foundation/PairKernelCanonicalGeneratorSourceS9.lean:400 
/-- The Green response obeys the unit-posting action equation after multiplying
the Laplacian by the action variation coefficient `2`. -/
theorem twice_laplacian_actionNormalizedGreenResponse3
    {N : ℕ} [NeZero N]
    (hN : 2 ≤ N)
    (q : ℂ) (event : PostingPair3 N)
    (σ : Equiv.Perm (Fin 3))
    (p : TorusSite3 N) :
    2 * framedTorusLaplacian σ
        (actionNormalizedGreenResponse3 q event) p =
      postingMagnitudeTorusSource3 q event p := by
  rw [actionNormalizedGreenResponse3_solves hN]
  exact twice_actionNormalizedGreenSource3 q event p
THEOREM twice_laplacian_actionNormalizedGreenResponse3 · IndisputableMonolith/Foundation/PairKernelCanonicalGeneratorSourceS9.lean
twice_laplacian_actionNormalizedGreenResponse3 · IndisputableMonolith/Foundation/PairKernelCanonicalGeneratorSourceS9.lean:400 
/-- The Green response obeys the unit-posting action equation after multiplying
the Laplacian by the action variation coefficient `2`. -/
theorem twice_laplacian_actionNormalizedGreenResponse3
    {N : ℕ} [NeZero N]
    (hN : 2 ≤ N)
    (q : ℂ) (event : PostingPair3 N)
    (σ : Equiv.Perm (Fin 3))
    (p : TorusSite3 N) :
    2 * framedTorusLaplacian σ
        (actionNormalizedGreenResponse3 q event) p =
      postingMagnitudeTorusSource3 q event p := by
  rw [actionNormalizedGreenResponse3_solves hN]
  exact twice_actionNormalizedGreenSource3 q event p

What this page does not claim

The theorem assigns no physical size to a posting. The theorem does not derive any measured constant such as the fine-structure constant. The response field is not claimed to be unique. The theorem does not imply that the Laplacian operator itself is the framework's action.

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