Foundation Pair Kernel Dimensioned Hamiltonian Compiler Source Density Non Id Si

The non-constant field

The theorem signedRealGreenField3_q1_exists_ne_reference is a statement about a discrete field, a finite list of numbers attached to the points of a small torus. It says that for any real number chosen as a reference, the field is not constant at that value: there is always at least one point where the field's value differs. In plainer terms, the field has shape; it is not a flat, featureless background.

The field in question is the q=1 Green field, a mathematical object built from a primitive posting pair, which is a pair of distinct points on the torus. The theorem applies only to realized primitive posting pairs, meaning the two points are genuinely different, not the same point twice. Given such a pair and any reference number, the proof constructs a point where the field deviates from that reference. This is a recognition event, a discrete record of a difference, and the theorem guarantees such a difference always exists.

This result is a lemma in a larger argument about a Hamiltonian, the matrix that encodes the energy of a one-body quantum system in this framework. The Hamiltonian's diagonal entries depend on the product of two model parameters, potentialScale and fieldNormalization, multiplied by the difference between the Green field and a reference. Because the field is never globally equal to the reference, the diagonal entries are not all zero, and the system has genuine dynamics. The theorem is proved in the machine-checked library of formal theorems, with no unproved assumptions.

The theorem does not claim that the field takes any particular value, nor that it is large or small. It does not identify the reference that makes the field zero, nor does it say the field is unique. It only establishes the existence of a difference, which is enough to ensure the Hamiltonian is not trivial. The theorem is a structural fact about the field, not a numerical prediction.

In the framework, this result supports the claim that the source-to-density coupling, the product of the two model parameters, is not selected by the S28 export and FD2 surface alone. Two different emissions with distinct positive products both preserve the semantics, and the corresponding Hamiltonians differ on the diagonal. The existence of the non-constant field is a necessary condition for this non-identifiability result.

/-- The q=1 Green field is never globally equal to a chosen reference. -/
theorem signedRealGreenField3_q1_exists_ne_reference
    (event : PostingPair3 3)
    (hevent : event ∈ realizedPrimitivePostingPairs3 3)
    (zeroReference : ℝ) :
    ∃ i : Fin (TorusCard3 3),
      signedRealGreenField3 1 event i ≠ zeroReference := by
  classical
  by_contra hnone
  push_neg at hnone
  have hsrc :
      ScaledSourceEquation
        (signedRecognitionProductionGraph3 3 (Equiv.refl (Fin 3))).weight
        (dipole event.1 event.2) (1 / 2)
        (signedRealGreenField3 1 event) :=
    signedRealGreenField3_scaledSourceEquation
      (by norm_num : 2 ≤ 3) (Equiv.refl (Fin 3)) (1 : ℝ) event
  have hlap := hsrc event.1
  have hne := realizedPrimitivePostingPair3_ne event hevent
  have hdip : dipole event.1 event.2 event.1 = (1 : ℝ) := by
    simp [dipole, hne]
  have hzero :
      laplacian
          (signedRecognitionProductionGraph3 3 (Equiv.refl (Fin 3))).weight
          (signedRealGreenField3 1 event) event.1 =
        0 := by
    have hfun :
        signedRealGreenField3 1 event = fun _ => zeroReference :=
      funext hnone
    rw [hfun, laplacian_const]
  rw [hzero, hdip] at hlap
  norm_num at hlap

/-- Realized primitive pairs are loopless, so source and sink differ. -/
theorem realizedPrimitivePostingPair3_ne
    (event : PostingPair3 3)
    (hevent : event ∈ realizedPrimitivePostingPairs3 3) :
    event.1 ≠ event.2 := by
  intro heq
  have hloop :
      (event.1, event.1) ∈ realizedPrimitivePostingPairs3 3 := by
    simpa [heq] using hevent
  have hrel :
      (@encodedMinimumJRelation3 3 _) event.1 event.1 :=
    (mem_realizedPrimitivePostingPairs3_iff _).mp hloop
  unfold encodedMinimumJRelation3 at hrel
  exact
    noSelfPrimitivePostings3_of_two_le (by norm_num : 2 ≤ 3)
      ((torusSiteEquivFin 3).symm event.1) hrel

/-- The finite Hamiltonian matrix depends on the product, not the split. -/
theorem oneBodyEvolution3_depends_on_sourceDensityCoupling
    (event : PostingPair3 3)
    (kineticScale potentialScale fieldNormalization zeroReference : ℝ)
    (i j : Fin (TorusCard3 3)) :
    (oneBodyEvolution3 kineticScale potentialScale
        (q1AtomicModelPotential3 event fieldNormalization zeroReference)).hamiltonian
      i j =
      kineticScale * oneBodyKineticEntry3 i j +
        if i = j then
          -sourceDensityCoupling potentialScale fieldNormalization *
            (signedRealGreenField3 1 event i - zeroReference)
        else
          0 := by
  simp only [oneBodyEvolution3]
  by_cases hij : i = j
  · subst j
    simp only [↓reduceIte, q1AtomicModelPotential3_product]
  · simp only [hij, ↓reduceIte]

What this page does not claim

The theorem does not identify the specific reference value that makes the field zero. The theorem does not claim the field is unique or that it takes any particular numerical value. The theorem does not establish the source-to-density coupling value; it only shows the field is non-constant.

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