Foundation Pair Kernel Canonical Generator Source S9 Posting Magnitude Action La

The posting law

The declaration postingMagnitudeActionLaw_iff_scaledSourceEquation is a theorem in the framework's machine-checked library of formal theorems. It connects two descriptions of the same physical situation. The first description is the posting law: a rule stating that a field paired with a posting of magnitude q produces a certain action. The second description is a scaled source equation: a differential equation whose right-hand side is a source term with a scale factor. The theorem states that these two descriptions are equivalent, provided the underlying weight function is symmetric.

The content of the equivalence is a simple division. When the posting has magnitude q, the scale factor in the source equation is exactly q/2. For the primitive case where the posting has magnitude 1, the canonical source scale is exactly 1/2. The theorem proves that the action law and the scaled source equation are two ways of saying the same thing, with the factor of two arising from the normalization convention: one elementary posting has divergence +1 at its source and -1 at its sink, while the fixed pair action has first variation 2 times the Laplacian.

The result is relative to the ledger action unit. A later physical conversion may assign a dimensional magnitude to one ledger posting; that magnitude stays an explicit parameter and is divided by two by the same theorem. The theorem does not fit any number. It does not introduce a hydrogen datum, a benchmark value, or any measured constant. It is a structural statement about how posting magnitudes and source scales relate within the framework.

/-- Exact action/Gauss compatibility. A posting magnitude `q` couples to the
Laplacian with scale `q / 2` because the fixed action derivative is
`2 * laplacian`. -/
theorem postingMagnitudeActionLaw_iff_scaledSourceEquation
    {n : ℕ}
    (q : ℝ)
    (w : Fin n → Fin n → ℝ)
    (e : Fin n → ℝ)
    (a b : Fin n)
    (hsymm : ∀ i j, w i j = w j i) :
    PostingMagnitudeActionLaw q w e a b ↔
      ScaledSourceEquation w (dipole a b)
        (realGreenScaleFromPostingMagnitude q) e := by
  unfold realGreenScaleFromPostingMagnitude
  constructor
  · intro hlaw
    have hstationary :
        StationaryAtCoefficient w e (dipole a b) q := by
      intro v
      calc
        physSourcePairing w e v =
            q * ∑ i,
              v i *
                PairKernelSourceCoupling.postingDivergence
                  (PairKernelSourceCoupling.elementaryPosting a b) i :=
          hlaw v
        _ = q * ∑ i, v i * dipole a b i := by
          congr 1
          apply Finset.sum_congr rfl
          intro i _
          rw [PairKernelSourceCoupling.elementaryPosting_divergence_eq_dipole]
    have hdoubled :
        ∀ i, 2 * laplacian w e i = q * dipole a b i :=
      (stationaryAtCoefficient_iff w e (dipole a b) q hsymm).mp
        hstationary
    intro i
    have h := hdoubled i
    linarith
  · intro hsource
    have hdoubled :
        ∀ i, 2 * laplacian w e i = q * dipole a b i := by
      intro i
      have h := hsource i
      linarith
    have hstationary :
        StationaryAtCoefficient w e (dipole a b) q :=
      (stationaryAtCoefficient_iff w e (dipole a b) q hsymm).mpr
        hdoubled
    intro v
    calc
      physSourcePairing w e v =
          q * ∑ i, v i * dipole a b i :=
        hstationary v
      _ = q * ∑ i,
          v i *
            PairKernelSourceCoupling.postingDivergence
              (PairKernelSourceCoupling.elementaryPosting a b) i := by
        congr 1
        apply Finset.sum_congr rfl
        intro i _
        rw [PairKernelSourceCoupling.elementaryPosting_divergence_eq_dipole]

/-- The existing unit `OneLedgerLaw` is exactly the half-scaled source
equation. -/
theorem oneLedgerLaw_iff_halfScaledSourceEquation
    {n : ℕ}
    (w : Fin n → Fin n → ℝ)
    (e : Fin n → ℝ)
    (a b : Fin n)
    (hsymm : ∀ i j, w i j = w j i) :
    OneLedgerLaw w e a b ↔
      ScaledSourceEquation w (dipole a b) (1 / 2) e := by
  simpa [PostingMagnitudeActionLaw, OneLedgerLaw,
    realGreenScaleFromPostingMagnitude] using
    postingMagnitudeActionLaw_iff_scaledSourceEquation
      1 w e a b hsymm

What this page does not claim

The theorem does not assign a dimensional magnitude to one ledger posting. The theorem does not fit any measured constant or benchmark datum. The theorem does not by itself establish the physical recognition-to-linking bridge for three-dimensional space.

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: