Foundation Pair Kernel Physical Source Covector

The physical source covector

The ledger, a discrete record of recognition events, records each elementary posting as a pair of entries: a source at one index and a sink at another. The integer Gauss source of such a posting is already known to be a unit dipole, a difference of two point masses. This construction builds the real-valued physical source covector that carries that dipole into field variations, the object that tells how a field responds to the posting.

The construction takes three steps. It takes the integer Gauss source, realifies it through the proved identification with the unit dipole, and couples it to field variations at an explicit symbolic positive scale. The result is a linear map, a covector, that acts on a field variation v by the formula sourceScale * (v a - v b). The scale parameter is left free; the Gauss law fixes the dipole shape, not the coupling magnitude.

The operational characterization of this covector is established. It is linear over the reals, vanishes on a posting with a equal to b, and has the correct support and sign structure: it reads sourceScale at the source index, -sourceScale at the sink, and zero elsewhere. It is unique among covectors realizing the Gauss source coupling law at a given scale, and the scale parameter is injective on a nontrivial posting, so different scales give different covectors.

In Recognition Science, this carrier is the bridge from a purely combinatorial integer dipole to a real physical source. The construction does not select a numerical source scale, does not derive OneLedgerLaw, and does not identify the carrier with a Noether momentum-map covector. The comparison with that momentum-map covector is recorded as an ordinary equality proposition on matching carrier types, a target for later work.

/-- Canonical realification: posting divergence equals the independently named
unit dipole. -/
theorem realifiedElementaryGaussSource_eq_unitDipole {n : ℕ}
    (a b i : Fin n) :
    realifiedElementaryGaussSource a b i = unitDipole a b i :=
  PairKernelDiscreteGauss.elementaryPosting_divF_eq_unitDipole a b i

/-- Operational evaluation as scaled potential drop. -/
theorem pairKernelPhysicalSourceCovector_apply {n : ℕ}
    (sourceScale : ℝ) (a b : Fin n) (v : Fin n → ℝ) :
    pairKernelPhysicalSourceCovector sourceScale a b v =
      sourceScale * (v a - v b) :=
  rfl

/-- Uniqueness: any covector realizing the same Gauss/source-coupling law at
the same symbolic scale equals the constructed carrier. -/
theorem pairKernelPhysicalSourceCovector_unique {n : ℕ}
    (φ : PhysicalSourceCarrier n) (sourceScale : ℝ) (a b : Fin n)
    (hφ : RealizesPairKernelGaussSourceCoupling φ sourceScale a b) :
    φ = pairKernelPhysicalSourceCovector sourceScale a b := by
  apply LinearMap.ext
  intro v
  calc
    φ v =
        sourceScale *
          ∑ i, v i *
            PairKernelDiscreteGauss.divF
              (PairKernelDiscreteGauss.elementaryPosting a b) i :=
      hφ v
    _ = pairKernelPhysicalSourceCovector sourceScale a b v :=
          (pairKernelPhysicalSourceCovector_eq_divF_pairing
            sourceScale a b v).symm

/-- Distinct symbolic scales give distinct covectors on a nontrivial posting.
This is the precise sense in which scale freedom lives in the constructor:
Gauss fixes shape; scale remains a free real parameter. -/
theorem pairKernelPhysicalSourceCovector_scale_injective {n : ℕ}
    {a b : Fin n} (hab : a ≠ b) {s₁ s₂ : ℝ}
    (h : pairKernelPhysicalSourceCovector s₁ a b =
      pairKernelPhysicalSourceCovector s₂ a b) :
    s₁ = s₂ := by
  have hs :=
    congrArg
      (fun φ : PhysicalSourceCarrier n =>
        φ (fun i => if i = a then (1 : ℝ) else 0)) h
  have h1 := pairKernelPhysicalSourceCovector_source_basis s₁ a b hab
  have h2 := pairKernelPhysicalSourceCovector_source_basis s₂ a b hab
  simp only [h1, h2] at hs
  exact hs

/-- **MODEL.** Real covector on posting/field variations for a realized
elementary posting, at an explicit symbolic source scale.

Evaluation equals `sourceScale * (v a - v b)`, equivalently the pairing of `v`
against `sourceScale · divF(elementaryPosting a b)`. -/
def pairKernelPhysicalSourceCovector {n : ℕ}
    (sourceScale : ℝ) (a b : Fin n) : PhysicalSourceCarrier n where
  toFun v := sourceScale * (v a - v b)
  map_add' v w := by
    simp only [Pi.add_apply]
    ring
  map_smul' c v := by
    simp only [Pi.smul_apply, RingHom.id_apply, smul_eq_mul]
    ring

What this page does not claim

This construction does not derive the OneLedgerLaw. This construction does not identify the carrier with a Noether momentum-map covector. This construction does not set the numerical source scale.

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/PairKernelPhysicalSourceCovector.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: