Foundation Pair Kernel Coherence Scaled Event Operator Coherence Born Source Res

The source response identity

In quantum mechanics, the Born rule is the link between a wavefunction and the probabilities of measurement outcomes: the chance of finding a particle at a location is the squared magnitude of the wavefunction there. The declaration coherenceBornSourceResponse3_apply states a compact version of this idea for a finite, discrete system. It says that the response of the system's energy to a small change in the potential, evaluated along a given quantum state, equals the sum over all locations of the potential change multiplied by the probability density of the state at that location. In symbols, for a state ψ and a potential variation δV, the response is Σᵢ δV(i) · |ψ(i)|². This is the standard first-order perturbation formula, written as an exact identity rather than an approximation.

The identity is a theorem in the framework's machine-checked library of formal theorems, meaning its proof is verified by a computer and rests on no unproven assumptions. It is a definitional unfolding: the response is defined to be this sum, so the theorem holds by rewriting. The same library also proves that this response is linear in the potential change, that the energy itself is the response evaluated at the full potential, and that the scaled version used in the framework's operator carries the same structure with an overall energy scale factor. These are structural facts about how the framework models a single quantum particle on a torus of three sites.

In Recognition Science, this identity is one piece of a larger construction called the coherence-scaled event operator. The framework models a physical event as a discrete posting on a small graph, and builds a Hamiltonian from a signed graph Laplacian plus a potential derived from the Green's function of that posting. The source response identity is the bridge between the potential and the probability distribution: it says the energy shift caused by changing the potential is exactly the overlap of that change with the state's density. This is what makes the potential and the response two views of the same object, a duality the framework exploits.

The theorem does not claim that this operator is the Hamiltonian of any real molecule. The framework explicitly states that this is a model carrier with theorem properties: the structure is chosen, not derived from first principles, and its dimensionless coupling ratio is fixed to one by definition. The declaration does not prove that the emitted spectrum matches atomic measurements, nor does it establish the remaining physical equalities that would tie this operator to hydrogen or other elements. It also does not claim that the potential variation is physical or that the response identity holds for arbitrary potentials; it holds for the finite torus model as defined.

What the identity does establish is a clean, checkable foundation: given the model's definitions, the response formula is exact and machine-verified. This matters because it separates the parts of the framework that are proved from the parts that are chosen. The response identity is a proved structural fact; the choice of the operator itself is a modeling decision awaiting empirical test. A reader can rely on the former while holding the latter open.

theorem coherenceBornSourceResponse3_apply
    (ψ : OneBodyHilbert3) (variation : PotentialVariation3) :
    coherenceBornSourceResponse3 ψ variation =
      eventGeneratorEnergyScale *
        ∑ i, variation i * Complex.normSq (ψ i) := by
  simp [coherenceBornSourceResponse3, bornSourceResponse3_apply]

theorem coherenceBornSourceResponse3_apply
    (ψ : OneBodyHilbert3) (variation : PotentialVariation3) :
    coherenceBornSourceResponse3 ψ variation =
      eventGeneratorEnergyScale *
        ∑ i, variation i * Complex.normSq (ψ i) := by
  simp [coherenceBornSourceResponse3, bornSourceResponse3_apply]

/-- Exact scaled line response. The source-to-density response and the
Hamiltonian generator carry the same single native event scale. -/
theorem coherenceBornPotentialEnergy3_line
    (potential variation : PotentialVariation3)
    (ψ : OneBodyHilbert3) (t : ℝ) :
    eventGeneratorEnergyScale *
        bornPotentialEnergy3
          (fun i => potential i + t * variation i) ψ =
      eventGeneratorEnergyScale *
          bornPotentialEnergy3 potential ψ +
        t * coherenceBornSourceResponse3 ψ variation := by
  rw [bornPotentialEnergy3_line]
  simp [coherenceBornSourceResponse3]
  ring

What this page does not claim

The coherence-scaled event operator is the Hamiltonian of any real molecule. The emitted spectrum of this operator matches atomic measurements. The potential variation used in the model is a physical or measurable quantity.

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