Foundation Pair Kernel Green3

The three-dimensional target

In classical physics, the Green function for three-dimensional space carries a famous coefficient. For a point source, the potential falls off as 1/r, and the constant in front is 1/(4π). This library, foundation pair kernel green3, a machine-checked collection of formal theorems, names that exact coefficient as its target: 1 / (4 * Real.pi).

The library does not prove that the coefficient emerges from the framework's discrete recognition lattice. That theorem is open. Instead, the file sets up the precise statement to aim for. It defines a predicate, GreenAsymptoticCoefficient3, which says that a supplied function green has the right asymptotic behavior: the product r * green(r) converges to the target coefficient as r grows. The target itself, GreenCoefficientTarget3, is this predicate applied to the specific value 1/(4π).

The library's proved content is a cautionary tale about what the target alone cannot do. A structure called GreenReadout3 bundles a green coefficient, a source scale, and a coupling scale. The theorem greenCoeff_alone_does_not_identify_source_or_coupling shows that two different readouts can share the same green coefficient of 1/(4π) while having different source and coupling scales. In plain terms: knowing the 1/(4π) coefficient does not tell you the strength of the source or the coupling. A free scale survives.

The library also proves that distinct source strengths produce distinct potential coefficients. If one source has scale 1 and another scale 2, their potential coefficients differ. This is the normalization decoy, a deliberately simple result that shows why the asymptotic coefficient alone cannot pin down a Newton-type coupling. The file's docstring states this plainly: the target is a predicate on a supplied Green readout, not a proved property of the lattice.

What this establishes, in the framework's own terms, is a clean separation of concerns. The three-dimensional Green coefficient is a well-defined target. The source normalization is a separate piece of data. And the hard theorem, that the cubic recognition lattice actually produces this coefficient, remains open. The library's value is in stating the goal precisely and in proving why the goal alone is not enough.

/-- The D=3 continuum Green coefficient targeted by R6. -/
def greenCoeff3 : ℝ := 1 / (4 * Real.pi)

/-- A radial Green readout has asymptotic coefficient `C` when `r * G(r)`
converges to `C` along the natural-number shells. -/
def GreenAsymptoticCoefficient3 (green : ℕ → ℝ) (C : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ R : ℕ, ∀ r : ℕ, R ≤ r →
    |(r : ℝ) * green r - C| < ε

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

/-- 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 library does not prove that the recognition lattice has the 1/(4π) coefficient. The library does not derive Newton's gravitational constant or any coupling constant. The library does not identify the source scale or coupling scale from the Green coefficient alone.

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: