Foundation Pair Kernel Green3 Same Green Coeff Different Source Potential

The source-scale ambiguity

The declaration same_greenCoeff_different_source_potential (a theorem in the framework's machine-checked library) establishes a precise ambiguity: two different source strengths can produce two different potential coefficients while sharing the same Green function coefficient. In plain terms, knowing the far-field shape of a potential does not tell you how strong the source is. The theorem constructs the example explicitly: source strengths 1 and 2 both yield the same Green coefficient 1/(4π), yet their potential coefficients differ, since the coefficient is sourceScale/(4π).

The Green function here is the standard mathematical object: a function describing how a field responds to a point source, with r·G(r) converging to a constant C at large radius. The framework defines this asymptotic coefficient precisely and sets a target: for the three-dimensional recognition lattice, the coefficient should equal 1/(4π). That target is stated as a predicate, not proved. The proved theorem instead shows why the target alone cannot determine a Newton-type coupling: a free source scale survives, and the same coefficient is compatible with many source strengths.

In Recognition Science, this is a deliberate decoy gate. The framework models a normalization package that keeps the Green readout and source strength separate, and it proves that distinct source strengths give distinct potential coefficients. The package type is inhabited without asserting the hard target, using a dummy readout that carries no claim of being a lattice Green function. The theorem establishes what the target cannot do, not what it can.

What the declaration does not claim is equally important. It does not prove that the cubic recognition lattice has coefficient 1/(4π); that hard theorem remains open. It does not identify the source or coupling scale from the Green coefficient alone. It contains no gravity, Planck, SI, or Newton-coupling module. The couplingScale field in the readout structure is explicitly uninterpreted and is not Newton's constant. The theorem is a boundary marker, not a destination.

/-- The same Green coefficient can accompany distinct source-scaled
potential coefficients. -/
theorem same_greenCoeff_different_source_potential :
    ∃ S₁ S₂ : ℝ,
      S₁ ≠ S₂ ∧
      greenCoeff3 = greenCoeff3 ∧
      sourceScaledPotentialCoeff S₁ ≠ sourceScaledPotentialCoeff S₂ := by
  exact
    ⟨1, 2, by norm_num, rfl,
      source_scale_changes_potentialCoeff⟩

theorem sourceScaledPotentialCoeff_eq (sourceScale : ℝ) :
    sourceScaledPotentialCoeff sourceScale =
      sourceScale / (4 * Real.pi) := rfl

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

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

What this page does not claim

The theorem does not prove that the cubic recognition lattice has coefficient 1/(4π). The theorem does not identify the source or coupling scale from the Green coefficient alone. The couplingScale field is uninterpreted and is not Newton's constant.

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: