Foundation Pair Kernel Green3 Source Scaled Potential Coeff Ne Of Ne

Distinct sources, distinct coefficients

In the Recognition Science framework's machine-checked library of formal theorems, a ledger (a discrete record of events) is used to model physical structure. One route to a three-dimensional theory starts with a Green function, a mathematical object that describes how a field spreads from a point source. The declaration sourceScaledPotentialCoeff_ne_of_ne is a theorem about that setup, and it establishes a simple, exact fact: if you have two different source strengths, then the potential coefficients they produce are also different.

Formally, the theorem states that if S₁ and S₂ are real numbers and S₁ ≠ S₂, then sourceScaledPotentialCoeff S₁ ≠ sourceScaledPotentialCoeff S₂. The potential coefficient is defined as the source strength divided by 4π, the same factor that appears in the Coulomb and Newtonian potentials in three dimensions. The argument is a short algebraic one: it multiplies both sides of the assumed equality by 4π, uses the fact that 4π is not zero, and concludes the source strengths must be equal, contradicting the hypothesis. A corollary shows that source strengths 1 and 2 give different coefficients.

The theorem is a statement about the definition of the potential coefficient, not about the physical world. It does not establish that any particular Green function exists, nor that the coefficient for a recognition lattice is actually 1/(4π). That harder target, named GreenCoefficientTarget3, is stated but not proved in the same module. The theorem's role is to separate a mathematical identity from a physical claim: it shows that the definition is injective, meaning different sources map to different coefficients, but it says nothing about which source scale is the right one.

The significance is a negative one, and it is deliberate. The framework's developers call this a "decoy gate": it demonstrates that knowing the Green coefficient alone cannot identify the source strength or the coupling scale. A separate theorem, greenCoeff_alone_does_not_identify_source_or_coupling, shows two different readouts can share the same coefficient while having different source and coupling scales. The theorem being asked about here is the simpler piece of that argument: it confirms that the mapping from source to coefficient is one-to-one, so any ambiguity must come from the physics, not from the definition.

In plain terms, the declaration is a guardrail. It tells a reader that within this formal system, a potential coefficient uniquely determines its source strength, and vice versa. It does not tell a reader which source strength nature chose, and it does not claim to have derived Newton's constant or any other physical coupling. Those remain open targets, and the theorem's honesty about its own limits is part of what makes the framework's larger claims credible.

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

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

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

This theorem does not claim that the potential coefficient for any real system is 1/(4π). This theorem does not claim to derive Newton's gravitational constant or any other physical coupling. This theorem does not claim that a Green function for the recognition lattice exists.

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: