Foundation Pair Kernel Zero Fit One Body Atomic Checkpoint Fd2 Fd2 Continuum Gre

The continuum Green shape

The declaration fd2_continuum_green_shape establishes a specific mathematical fact: in three spatial dimensions, the continuum Green's function for the inverse Laplacian operator is exactly 1/(4πr). This is the standard Newtonian potential kernel, the same function that describes gravitational and electrostatic fields spreading from a point source. This shape is stated as NewtonianFourierTarget, a named target within the framework's machine-checked library.

In plain terms, the declaration pins down the "shape" of a field that solves a particular differential equation. When you have a point source, the field it produces falls off as one over the distance, with a specific numerical factor. The declaration proves this is the correct continuum form, and it does so with a proof that has been verified by a computer, with no gaps or unproven assumptions in the logical chain.

What the declaration does not do is equally important. It does not claim that this mathematical field is actually the potential experienced by an electron in a hydrogen atom. That physical identification is a separate step, stated as a predicate called RecognitionOneBodyQuantumAttachment3. The framework explicitly marks this as an "exact missing semantic arrow": no statement asserts that the mathematical Green's function corresponds to a real physical electron potential. The declaration also does not select the coupling ratio between kinetic and potential energy, does not identify the framework's internal constant with the physical fine-structure constant, and does not choose SI units.

In Recognition Science, this declaration is a checkpoint in a larger construction. It provides a rigorous mathematical foundation, a theorem-backed shape, on which a physical model could later be built. But the bridge from mathematics to physics, from the Green's function to the electron, remains open. The framework is explicit about this gap, presenting it not as a failure but as a clearly marked target for future work.

/-- The continuum inverse-Laplacian shape used by the MODEL attachment is
the theorem-backed `1 / (4*pi*r)` Newtonian Green kernel in D=3. -/
theorem fd2_continuum_green_shape :
    NewtonianFourierTarget :=
  newtonian_fourier_target

/-- The continuum inverse-Laplacian shape used by the MODEL attachment is
the theorem-backed `1 / (4*pi*r)` Newtonian Green kernel in D=3. -/
theorem fd2_continuum_green_shape :
    NewtonianFourierTarget :=
  newtonian_fourier_target

/-- Exact missing semantic arrow.  A committed physical one-body Hamiltonian
would have to be identified with the S28 generator and q=1 Green potential,
with positive scales selected independently of hydrogen. -/
def RecognitionOneBodyQuantumAttachment3
    (physicalHamiltonian : DiscreteEvolution (TorusCard3 3)) : Prop :=
  ∃ event : PostingPair3 3,
    event ∈ realizedPrimitivePostingPairs3 3 ∧
      ∃ kineticScale potentialScale fieldNormalization zeroReference : ℝ,
        0 < kineticScale ∧
          0 < potentialScale ∧
          0 < fieldNormalization ∧
          physicalHamiltonian =
            oneBodyEvolution3 kineticScale potentialScale
              (q1AtomicModelPotential3
                event fieldNormalization zeroReference)

What this page does not claim

The declaration does not claim the Green's function is the actual electron potential in hydrogen. It does not select the kinetic-to-field coupling ratio or identify the framework's alpha with the physical fine-structure constant. It does not choose SI units or provide any empirical normalization.

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