Foundation Pair Kernel Green3 Green Coeff Alone Does Not Identify Source Or Coup

The identification limit

A Green function is a mathematical tool that describes how a localized source, like a point charge or a mass, creates a field or potential throughout space. In three dimensions, the potential from a unit source falls off with distance, and the constant that sets its overall size is its Green coefficient. For the standard continuum case, that coefficient is 1/(4π), a value that appears throughout physics whenever a field spreads out symmetrically in three-dimensional space.

The Recognition Science library formalizes a target for this coefficient. Its declaration greenCoeff3 defines the number 1/(4π) as the asymptotic goal for a Green readout on a cubic recognition lattice, a discrete grid of points where the framework records events. The library also defines what it means for a readout to have this asymptotic coefficient: after multiplying the readout by the shell radius, the result must converge to that constant as the radius grows. This is the exact target the framework names for its three-dimensional route, but it is a target, not a result. The library states plainly that no declaration proves the cubic lattice actually produces this coefficient.

What the library does prove is a limit on what the coefficient alone can tell you. The theorem greenCoeff_alone_does_not_identify_source_or_coupling constructs two different readouts that share the same Green coefficient, 1/(4π), but have different source scales and different coupling scales. In plain terms: if you only know the coefficient, you cannot know whether the source is weak and close or strong and far, nor can you know the strength of the interaction that couples the source to the field. The Green function's shape fixes the coefficient, but the source strength and the coupling constant remain free parameters that this coefficient does not determine.

This is a deliberate decoy gate in the framework's research program. The library separates the Green readout from the source normalization, holding them as distinct pieces of data. It proves that distinct source strengths give distinct potential coefficients, so the source scale is not a meaningless label. Yet the same coefficient can accompany different source scales. The framework's own documentation calls this the R6 decoy gate: a checkpoint that shows why the hard theorem, proving that the cubic lattice has the exact 1/(4π) coefficient, cannot be replaced by a simple reading of the coefficient itself. The normalization package exists, but it carries the unproved target as an obligation, not as a fact.

What the theorem does not claim is just as important. It does not say that the Green coefficient is wrong, or that the 1/(4π) target is unattainable. It does not say anything about gravity, Planck's constant, SI units, or Newton's coupling constant, none of which appear in this framework. The theorem is a statement about identification: a single asymptotic number, however precisely measured, cannot single out the source strength or the coupling that produced it. The hard work of deriving the coefficient from the lattice remains open, and this theorem is the guard that keeps that open problem honest.

/-- Green normalization alone leaves the source and coupling scales
unidentified. This is the R6 decoy gate. -/
theorem greenCoeff_alone_does_not_identify_source_or_coupling :
    ∃ R₁ R₂ : GreenReadout3,
      R₁.greenCoefficient = greenCoeff3 ∧
      R₂.greenCoefficient = greenCoeff3 ∧
      R₁.greenCoefficient = R₂.greenCoefficient ∧
      R₁.sourceScale ≠ R₂.sourceScale ∧
      R₁.couplingScale ≠ R₂.couplingScale := by
  refine
    ⟨{ greenCoefficient := greenCoeff3, sourceScale := 1, couplingScale := 1 },
      { greenCoefficient := greenCoeff3, sourceScale := 2, couplingScale := 2 },
      ?_⟩
  norm_num

/-- The exact R6.1 target. This file states it and does not prove it for a
lattice Green function. -/
def GreenCoefficientTarget3 (green : ℕ → ℝ) : Prop :=
  GreenAsymptoticCoefficient3 green greenCoeff3

/-- Distinct source strengths give distinct potential coefficients. -/
theorem sourceScaledPotentialCoeff_ne_of_ne {S₁ S₂ : ℝ} (hS : S₁ ≠ S₂) :
    sourceScaledPotentialCoeff S₁ ≠ sourceScaledPotentialCoeff S₂ := by
  unfold sourceScaledPotentialCoeff
  intro h
  have hden : (4 : ℝ) * Real.pi ≠ 0 := by positivity
  have hmul := congrArg (fun x : ℝ => x * (4 * Real.pi)) h
  field_simp [hden] at hmul
  exact hS hmul

What this page does not claim

The theorem does not prove the cubic lattice has the 1/(4π) coefficient. The theorem does not involve gravity, Planck's constant, SI units, or Newton's coupling constant. The theorem does not say the Green coefficient is an insufficient description of the potential's shape.

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