Foundation Pair Kernel Finite Heisenberg Weyl Event Operator Finite Heisenberg W

The 27-site certificate

The declaration finiteHeisenbergWeylEventOperator_cert27 is a certificate: a machine-checked bundle of proofs that a specific finite model is internally consistent. The model lives on a torus of 27 sites, where each site is an address with three coordinates, and each coordinate takes one of three values. This is the smallest nontrivial setting where a quantum clock and a quantum shift can coexist on three independent axes.

The certificate proves four things about this model. First, the carrier really has 27 sites. Second, on every axis, the clock and shift obey the Weyl relation: shifting then clocking equals clocking then shifting, up to a fixed cubic phase factor. Third, the model's primary action, a sum of squared shift mismatches and clock-weighted squared amplitudes, is never negative. Fourth, the source response and the operator entries are defined as derivatives of that same primary action, not as separate inputs. The certificate bundles these four proofs into one theorem, with no unproved assumptions and no empirical constants.

The certificate is honest about its scope. It does not claim that this 27-site action is the one Recognition Science forces. The equal weighting of shift and clock terms, the choice of this action as the molecular action, the clock center as a realized posting endpoint, and any dimensioned continuum radius all remain open. The certificate establishes only that this particular model is coherent: it has the right size, the right commutation law, and a nonnegative action, all derived from a single chosen action rather than from separate postulated channels.

What the certificate changes is the status of the model. Before it, the 27-site Weyl action was a proposal. After it, the proposal is a checked object: any further work can rely on its structural facts without re-verifying them. The certificate does not make the model true of the physical world; it makes the model safe to use as a defined starting point for later questions about whether Recognition Science forces this structure or another.

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 _))

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 operator_from_source_response27
    (center : WeylEventSite27)
    (i j : WeylEventSite27) :
    finiteWeylEventOperatorEntry27 center i j =
      (1 / 2 : ℝ) *
        deriv
          (fun t : ℝ =>
            finiteWeylEventSourceResponse27 center
              (fun site => t * weylSiteBasis27 j site)
              (weylSiteBasis27 i))
          0 := rfl

theorem finiteHeisenbergWeylEventOperator_cert27
    (center : WeylEventSite27) :
    FiniteHeisenbergWeylEventOperatorCert27 center where
  site_count := weylEventSite27_card
  axis_weyl := axis_weyl_relation27
  action_nonnegative := finiteWeylEventAction27_nonneg center
  source_from_action := sourceResponse_from_primary_action27 center
  operator_from_source := operator_from_source_response27 center

What this page does not claim

The certificate does not claim the 27-site action is the one Recognition Science forces. The certificate does not claim the equal shift/clock weight is derived rather than chosen. The certificate does not claim the model describes any empirical physical system.

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: