Foundation Pair Kernel Finite Heisenberg Weyl Event Operator Source Response Fro

The source response as a derivative

In Recognition Science, a ledger, a discrete record of events, can be assigned a numerical cost called its action. The declaration sourceResponse_from_primary_action27 establishes a precise link between this action and the system's response to a source. It defines the response as the first derivative of the action with respect to a variation in the system's state, evaluated at zero variation. In plain terms, it measures how steeply the cost changes when you nudge the state in a particular direction; that slope is the response.

The declaration is a theorem in the machine-checked library of formal theorems. It states that the defined response, finiteWeylEventSourceResponse27, equals the derivative of the action along a straight-line variation. This is proven by definitional equality, meaning the response is not an independent assumption but a packaging of the action's derivative. The theorem holds for any center point and any variation on the 27-site torus, where a site is a three-coordinate address with three phases per axis, giving 3^3 = 27 sites.

The action itself is a sum over three axes of shift mismatch and clock mismatch terms, with no free coefficients. The response and the operator are both derived from this action through derivatives. The framework proves the carrier has 27 sites, the Weyl relation holds on each axis, and the action is nonnegative. These are the theorems; the choice of this particular action as the primary object is a model, not a forced result.

What the declaration does not claim is equally important. It does not claim that the equal weighting of shift and clock terms is forced by existing Recognition theory, nor that this action is the unique molecular action, nor that its clock center corresponds to a realized posting endpoint. It also does not claim a dimensioned continuum radius. The honest status is a MODEL primary action with THEOREM carrier, Weyl relation, and nonnegativity. The response and operator are derivative-defined packaging of that model.

theorem sourceResponse_from_primary_action27
    (center : WeylEventSite27)
    (ψ variation : WeylEventAmplitude27) :
    finiteWeylEventSourceResponse27 center ψ variation =
      deriv
        (fun t : ℝ =>
          finiteWeylEventAction27 center
            (fun site => ψ site + t * variation site))
        0 := rfl

theorem sourceResponse_from_primary_action27
    (center : WeylEventSite27)
    (ψ variation : WeylEventAmplitude27) :
    finiteWeylEventSourceResponse27 center ψ variation =
      deriv
        (fun t : ℝ =>
          finiteWeylEventAction27 center
            (fun site => ψ site + t * variation site))
        0 := rfl

theorem weylEventSite27_card :
    Nat.card WeylEventSite27 = 27 := by
  change Nat.card (Fin 3 → ZMod 3) = 27
  rw [Nat.card_fun, Nat.card_zmod, Nat.card_fin]
  norm_num

/-- Exact finite Weyl relation on every production-torus axis. -/
theorem axis_weyl_relation27
    (ψ : WeylEventSite27 → ℂ)
    (axis : Fin 3)
    (site : WeylEventSite27) :
    clockAxis27 (shiftAxis27 ψ axis) axis site =
      omega3 * shiftAxis27 (clockAxis27 ψ axis) axis site := by
  have hval :
      ∀ j : ZMod 3,
        j.val = (j - 1).val + 1 ∨
          (j.val = 0 ∧ (j - 1).val = 2) := by
    decide
  have e :
      omega3 ^ (site axis).val =
        omega3 ^ ((site axis - 1).val + 1) := by
    rcases hval (site axis) with h | ⟨h0, h2⟩
    · rw [h]
    · rw [h0, h2, pow_zero]
      exact omega3_pow_three.symm
  simp only [clockAxis27, shiftAxis27, shiftSite27]
  simp only [Function.update_self]
  rw [e]
  simp [pow_succ, mul_comm, mul_assoc, mul_left_comm]

theorem finiteWeylEventAction27_nonneg
    (center : WeylEventSite27)
    (ψ : WeylEventAmplitude27) :
    0 ≤ finiteWeylEventAction27 center ψ := by
  unfold finiteWeylEventAction27
  apply Finset.sum_nonneg
  intro axis _
  apply Finset.sum_nonneg
  intro site _
  exact add_nonneg (sq_nonneg _)
    (mul_nonneg (Complex.normSq_nonneg _) (sq_nonneg _))

/-- Coefficient-free self-dual Weyl action. -/
def finiteWeylEventAction27
    (center : WeylEventSite27)
    (ψ : WeylEventAmplitude27) : ℝ :=
  Finset.univ.sum fun axis : Fin 3 =>
    Finset.univ.sum fun site : WeylEventSite27 =>
      (ψ (shiftSite27 axis site) - ψ site) ^ 2 +
        clockDisplacement27 center axis site * (ψ site) ^ 2

What this page does not claim

The equal shift and clock weight is not forced by existing theory. This action is not claimed to be the unique molecular action. The clock center is not claimed to be a realized posting endpoint.

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