Foundation Pair Kernel Canonical Generator Source S9 Candidate B Green Scale Eq

The half-scale source

A Green's function tells how a field responds to a point source. In the Recognition Science framework, the discrete analogue starts with a ledger, a record of elementary events, where each posting of one unit adds +1 at its source and -1 at its sink. The framework's cost, the forced price of recognition, obeys a fixed action principle whose first variation is twice the discrete Laplacian. Because of that factor of two, a posting of magnitude q produces a source term with coefficient q/2 in the Green equation.

The declaration candidateB_greenScale_eq_nativeQuantumInv_half is a theorem in the framework's machine-checked library of formal theorems. It states that for a particular candidate posting, called candidate B, the source scale equals exactly half of the native action quantum inverse. The proof is by reflection: the definition of the source magnitude and the definition of the native inverse are such that the equality holds by computation. No number is fitted, no physical datum is consulted, and no new axiom is introduced.

What the theorem does not claim is just as important. It does not assign a dimensional magnitude to a ledger posting; that magnitude remains an explicit parameter in a later physical conversion. It does not involve hydrogen or any benchmark measurement. It does not assert that candidate B is the physically realized source, only that its scale has this exact algebraic form. The theorem is a structural identity within the framework's discrete geometry, not an empirical prediction.

The consequence is that the framework's discrete Green equation has a canonical source scale for a primitive posting, and that scale is one half of the native quantum inverse. This anchors the relationship between the ledger's elementary events and the action that governs them, ready for a later step that may assign physical units.

/-- If Candidate B were attached to the posting source, the same action/Gauss
factor would give `φ⁵ / 2`; the factor of two is fixed independently of that
attachment. -/
theorem candidateB_greenScale_eq_nativeQuantumInv_half :
    realGreenScaleFromPostingMagnitude
        candidateB_sourceMagnitudeExpr.eval =
      nativeActionQuantumInv / 2 := by
  rfl

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

What this page does not claim

No dimensional magnitude is assigned to a ledger posting by this theorem. No hydrogen or benchmark datum appears in the proof. The theorem does not identify which candidate posting is physically realized.

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: