Foundation Pair Kernel Zero Fit One Body Atomic Checkpoint Fd2 One Body Kinetic

The symmetric kinetic entry

A kinetic energy matrix describes how a particle's state changes from one moment to the next. In quantum mechanics, this matrix must be symmetric: the influence of point i on point j must equal the influence of point j on point i. This property, called Hermiticity in the complex case, guarantees that probabilities stay well-defined and energy values come out real. The declaration oneBodyKineticEntry3_symmetric proves exactly this symmetry for a specific finite matrix built from the framework's S28 signed generator.

The matrix in question lives on a small three-by-three torus, a discrete grid where opposite edges connect. The framework defines the kinetic entry as a graph Laplacian: diagonal entries sum the connection weights from a point, off-diagonal entries are the negative weights. The theorem states that for any two points i and j on this grid, the entry at row i, column j equals the entry at row j, column i. The proof is short and mechanical, using the symmetry of the underlying generator weights.

This symmetry is a necessary ingredient for the larger project: attaching a real potential to this kinetic term to form a Hamiltonian. The framework proves separately that the resulting Hamiltonian is Hermitian and generates a unitary evolution, meaning probability is conserved. But the symmetry theorem itself does not claim that this matrix represents any physical system. It is a structural fact about a finite mathematical object.

In Recognition Science, this is a checkpoint on the road to a zero-fit atomic model. The framework's library of machine-checked theorems aims to show that quantum structure emerges from a discrete recognition ledger. This theorem is one small rung: it confirms that the kinetic piece has the right algebraic shape. It does not, however, identify the potential as an electron field, fix the coupling strength, or connect the framework's alpha constant to the measured fine-structure constant. Those remain explicit open targets, not consequences of this symmetry.

theorem oneBodyKineticEntry3_symmetric
    (i j : Fin (TorusCard3 3)) :
    oneBodyKineticEntry3 i j = oneBodyKineticEntry3 j i := by
  by_cases h : i = j
  · subst j
    rfl
  · have h' : j ≠ i := Ne.symm h
    simp only [oneBodyKineticEntry3, if_neg h, if_neg h']
    unfold oneBodyGeneratorWeights3
    rw [(signedRecognitionProductionGraph3
      3 (Equiv.refl (Fin 3))).weight_symm]

What this page does not claim

The theorem does not claim the kinetic matrix represents any physical system. It does not identify the q=1 Green potential as an electron potential. It does not select the kinetic-to-field coupling ratio or SI units.

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: