Foundation Pair Kernel Canonical Generator Source S9 One Ledger Law Iff Half Sca

The half-source law

In the Recognition Science framework, a ledger is a discrete record of events, and the smallest possible event is a single posting: a unit of value that moves from one site, its source, to another, its sink. The declaration oneLedgerLaw_iff_halfScaledSourceEquation states, in the framework's formal language, that a law governing one such posting is equivalent to a scaled source equation with coefficient one half. In plain terms, the theorem proves that when the framework's action, a measure of the cost of a configuration, is paired with a posting of magnitude one, the canonical source scale is exactly one half.

The result follows from a more general theorem, postingMagnitudeActionLaw_iff_scaledSourceEquation, which handles postings of any magnitude q. That theorem shows that an action field paired with a posting of magnitude q solves the Green equation with right-hand coefficient q / 2. Setting q = 1 yields the half-source law. The proof is machine-checked, meaning it is verified by a computer program that checks every step against the rules of logic, with no gaps and no unproven assumptions beyond the standard three axioms of the underlying type theory.

The theorem is relative to the ledger action unit. That is, the framework's action is measured in units where one elementary posting has divergence plus one at its source and minus one at its sink, and the fixed pair action has first variation two times the laplacian. These two normalizations are what force the factor of one half. A later physical conversion may assign a dimensional magnitude to one ledger posting, but that magnitude remains an explicit parameter, and the same theorem divides it by two. The result does not depend on any measured data, such as the hydrogen spectrum or a benchmark value; it is a purely structural consequence of the framework's definitions.

What the declaration does not claim is just as important. It does not assert that the half-source law is the only possible law for a posting, nor does it assign a physical meaning to the unit posting. It does not say that the source scale one half is a fundamental constant of nature; rather, it is a consequence of the chosen normalization of the action. The theorem also does not address the question of whether the framework's ledger action corresponds to any physical action in the conventional sense. Those questions remain open, and the declaration itself is silent on them.

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

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

/-- 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 claim that the half-source law is the only possible law for a posting. The theorem does not claim that the unit posting has any particular physical meaning. The theorem does not claim that the source scale one half is a fundamental constant of nature. The theorem does not address whether the framework's ledger action corresponds to any conventional physical 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: