Foundation Pair Kernel Green3 Green Readout3

The Green readout

In physics, a Green's function describes how a field responds to a point source. In three dimensions, the familiar Coulomb or Newton potential falls off as the inverse distance, and the coefficient 1/(4π) appears in the standard normalization. The Recognition Science framework's declaration GreenReadout3 is a small data structure that holds three real numbers: a greenCoefficient, a sourceScale, and a couplingScale. It is not a theorem about any actual lattice; it is a named container for the pieces that a future derivation would need to relate.

The framework's machine-checked library of formal theorems defines the exact asymptotic target: a radial Green readout has coefficient C when r times G(r) converges to C along the natural-number shells. The target coefficient is set to 1/(4π), the three-dimensional continuum value. But the file states this target as a predicate on a supplied readout; it does not prove that the cubic recognition lattice achieves it. The docstring is explicit: the hard theorem remains open, and no declaration below proves the coefficient for the lattice.

The proved content is a decoy that shows why the target alone cannot determine a Newton-type coupling. The library proves that distinct source strengths give distinct potential coefficients, and that a free source scale survives. A theorem constructs two readouts with the same greenCoefficient but different sourceScale and couplingScale values. The same Green coefficient can accompany different source-scaled potential coefficients. This is the R6 decoy gate: normalization alone leaves the source and coupling scales unidentified.

In Recognition Science, this declaration models the separation between the asymptotic target and the source normalization. The framework proves the separation is real: knowing the 1/(4π) coefficient does not fix the source strength. What the declaration does not claim is that the cubic lattice actually produces this coefficient, or that the couplingScale is Newton's constant. Those remain targets for future work, not results in hand.

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

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

/-- 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 cubic recognition lattice has asymptotic coefficient 1/(4π). The couplingScale in GreenReadout3 is Newton's constant. The declaration proves the existence of a lattice Green function with the target coefficient.

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: