Foundation Pair Kernel Exact Jsource First Event Operator Exact Jsource First Ev

The source-first operator

In classical physics, a system is usually described by a Hamiltonian: a chosen expression for energy that already separates kinetic terms, potential terms, and sources. The Recognition Science framework inverts that order. It begins with a ledger, a discrete record of recognition events, and defines a single cost function J(x) = (x + 1/x)/2 - 1 on that ledger. The declaration exactJSourceFirstEventOperator_cert establishes that from this one cost function, two derivatives produce the two central objects of a physical theory: the source response and the fluctuation generator. No Hamiltonian is chosen first; both objects fall out of the same action.

The construction works on a finite three-site carrier. The framework defines an event background, a realized posting on that carrier, and evaluates the exact J-cost action at that background. The first variation of this action with respect to a field variation is the source response. The theorem proves this response is exactly the derivative of the action, and identifies it with a nonlinear Gauss source: a sum over sites of the variation times a nonlinear Laplacian of the background. The factor two in that sum is not inserted by hand; it is forced by differentiating J itself.

The second derivative of the same action, read on a site basis, gives a symmetric matrix: the Hessian. The framework complexifies this Hessian to form a dimensionless fluctuation operator, then multiplies by a single common scale, the native action per tick, to obtain a physical evolution operator. The certificate proves this operator is Hermitian and satisfies the Stone generator condition, the mathematical property that makes it a valid generator of unitary time evolution. A decoy normalization, one that omits the ordered-edge factor two, is proved not to be the derivative of exact J even on the smallest nontrivial carrier.

What the certificate does not claim is equally precise. The docstring states plainly that the physical interpretation of this fluctuation operator as a molecular one-body Hamiltonian is a MODEL, not a theorem. The construction has no separate attractive potential and no selected molecular coupling ratio. It therefore does not close the dimensioned compiler or produce the Planck source-scale atom. The certificate proves the variational and operator properties; the leap to molecular physics remains open.

theorem sourceResponse_is_action_derivative
    (op : ExactJSourceFirstEventOperator3) (variation : EventField3) :
    HasDerivAt
      (fun t : ℝ =>
        eventExactJAction3
          (fun i => op.background i + t * variation i))
      (op.sourceResponse variation) 0 := by
  exact
    exactJCostAction_hasDerivAt_line
      (signedRecognitionProductionGraph3 3 (Equiv.refl (Fin 3)))
      op.background variation

/-- The intrinsic response is exactly the nonlinear Gauss source paired with
the variation.  The ordered-edge factor two is fixed by differentiating J. -/
theorem sourceResponse_eq_nonlinear_gauss
    (op : ExactJSourceFirstEventOperator3) (variation : EventField3) :
    op.sourceResponse variation =
      2 * ∑ i, variation i *
        exactJNonlinearLaplacian
          (signedRecognitionProductionGraph3 3 (Equiv.refl (Fin 3)))
          op.background i := by
  exact
    exactJFirstVariationPairing_eq_two_sum_mul_laplacian
      (signedRecognitionProductionGraph3 3 (Equiv.refl (Fin 3)))
      op.background variation

theorem hessianEntry_symmetric
    (op : ExactJSourceFirstEventOperator3)
    (i j : Fin (TorusCard3 3)) :
    op.hessianEntry i j = op.hessianEntry j i := by
  unfold ExactJSourceFirstEventOperator3.hessianEntry
  rw [exactJHessianPairing_comm]

theorem source_first_event_operator_stone
    (op : ExactJSourceFirstEventOperator3) :
    StoneGeneratorCert (TorusCard3 3) op.evolution :=
  stoneGeneratorCert op.evolution

/-- The response normalization is discriminating: omitting the
ordered-edge factor two is not the derivative of exact J even on the smallest
nontrivial carrier. -/
theorem missing_factor_two_decoy_rejected :
    ¬ HasDerivAt
      (fun t : ℝ =>
        exactJCostAction twoSiteUnitLedgerGraph
          (fun i => PairKernelSourceCoupling.twoSiteField 2 i +
            t * PairKernelSourceCoupling.twoSiteField 2 i))
      (Real.sinh 1) 0 :=
  missingFactorTwo_not_exactJDerivative

What this page does not claim

The fluctuation operator is not proved to be the molecular one-body Hamiltonian. The construction has no separate attractive potential and no selected molecular coupling ratio. The certificate does not close the dimensioned compiler or produce the Planck source-scale atom.

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