Foundation Pair Kernel Source Normalization

Source scale freedom

In Recognition Science, a ledger, a discrete record of events and their connections, is described by a pair kernel, a function assigning a real number to every ordered pair of points. The source equation relates a field on the ledger to a source profile through a weighted graph Laplacian, a measure of how a value at a point differs from its neighbors. The equation takes the form L w e = scale * rho, where L is the Laplacian, e is the field, rho is the source profile, and scale is a normalization constant.

The module proves a homogeneity property: scaling the field by any real number c scales the Laplacian by the same factor, and scales the quadratic action, a measure of total pair energy, by c squared. From this, it derives a key consequence. If you have one solution with scale 1, you can multiply the field by any number to get a solution with that number as the scale, on the same ledger and with the same source profile. The proof is a short chain of algebraic manipulations, checked by the framework's machine-checked library of formal theorems.

This result is a mathematical no-go for this premise package. It shows that the source equation alone cannot determine a preferred normalization scale. The framework does not claim that the physical source scale is absent; rather, it proves that within this equation, any scale is as good as any other. A separate physical law, not yet derived, must break this rescaling freedom to select the actual scale seen in nature.

The module also proves an energy identity: for symmetric weights, the action equals the scale times a source-field pairing, a sum of products of field and source values. This identity holds for any scaled source equation and is used elsewhere in the framework. A final theorem, called the decoy, makes the freedom vivid: one unit-normalized solution gives both a scale 1 and a scale 2 equation on the same carrier and source profile, with 1 not equal to 2, demonstrating concretely that the equation cannot distinguish between them.

In Recognition Science, this means the source equation is a relation, not a selector. The framework's contribution is to state the freedom exactly and prove it, so that any future claim about a specific scale must come from an additional principle, not from this equation. The practical consequence is that when the framework later derives constants like hbar or G, it must do so through a mechanism that breaks this proved rescaling family.

/-- The weighted graph Laplacian is homogeneous in the field. -/
theorem laplacian_scale
    (w : ι → ι → ℝ) (e : ι → ℝ) (c : ℝ) (i : ι) :
    laplacian w (fun i => c * e i) i = c * laplacian w e i := by
  unfold laplacian
  rw [Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro j _
  ring

/-- The quadratic pair action is homogeneous of degree two in the field. -/
theorem action_scale
    (w : ι → ι → ℝ) (e : ι → ℝ) (c : ℝ) :
    action w (fun i => c * e i) = c ^ 2 * action w e := by
  unfold action
  calc
    (1 / 2 : ℝ) *
        ∑ i, ∑ j, w i j * ((c * e i) - (c * e j)) ^ 2
        = (1 / 2 : ℝ) *
            ∑ i, ∑ j, c ^ 2 * (w i j * (e i - e j) ^ 2) := by
          congr 1
          apply Finset.sum_congr rfl
          intro i _
          apply Finset.sum_congr rfl
          intro j _
          ring
    _ = (1 / 2 : ℝ) *
          (c ^ 2 * ∑ i, ∑ j, w i j * (e i - e j) ^ 2) := by
          congr 1
          rw [Finset.mul_sum]
          apply Finset.sum_congr rfl
          intro i _
          rw [Finset.mul_sum]
    _ = c ^ 2 *
          ((1 / 2 : ℝ) * ∑ i, ∑ j, w i j * (e i - e j) ^ 2) := by
          ring

/-- From an explicit unit-normalized solution, every source scale is admitted
by rescaling the field. -/
theorem every_source_scale_admitted_of_unit_solution
    (w : ι → ι → ℝ) (rho : ι → ℝ) (sourceScale : ℝ) (e : ι → ℝ)
    (hunit : ScaledSourceEquation w rho 1 e) :
    ScaledSourceEquation w rho sourceScale (fun i => sourceScale * e i) := by
  simpa using
    scaledSourceEquation_scale
      (w := w) (rho := rho) (scale := (1 : ℝ)) (c := sourceScale)
      (e := e) hunit

/-- Generic energy identity for any scaled source equation under symmetric
weights. -/
theorem action_eq_scale_sourcePairing_of_scaledSourceEquation
    (w : ι → ι → ℝ) (rho : ι → ℝ) (scale : ℝ) (e : ι → ℝ)
    (hsymm : ∀ i j, w i j = w j i)
    (hsource : ScaledSourceEquation w rho scale e) :
    action w e = scale * sourcePairing rho e := by
  rw [action_eq_sum_mul_laplacian w e hsymm]
  unfold sourcePairing
  calc
    (∑ i, e i * laplacian w e i)
        = ∑ i, e i * (scale * rho i) := by
          apply Finset.sum_congr rfl
          intro i _
          rw [hsource i]
    _ = ∑ i, scale * (e i * rho i) := by
          apply Finset.sum_congr rfl
          intro i _
          ring
    _ = scale * ∑ i, e i * rho i := by
          rw [Finset.mul_sum]

/-- Explicit normalization decoy: one unit solution gives both scale `1`
and scale `2` equations on the same carrier and source profile. -/
theorem decoy_scale_one_and_two_of_unit_solution
    (w : ι → ι → ℝ) (rho : ι → ℝ) (e : ι → ℝ)
    (hunit : ScaledSourceEquation w rho 1 e) :
    ScaledSourceEquation w rho 1 e ∧
      ScaledSourceEquation w rho 2 (fun i => (2 : ℝ) * e i) ∧
      (1 : ℝ) ≠ 2 := by
  refine ⟨hunit, ?_, by norm_num⟩
  simpa using
    every_source_scale_admitted_of_unit_solution
      (w := w) (rho := rho) (sourceScale := (2 : ℝ)) (e := e) hunit

What this page does not claim

The physical source scale is absent. A specific normalization scale is derived in this module. The source equation alone determines a preferred scale. This module proves the existence of a unit-normalized solution for any pair kernel and source profile.

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