Foundation Pair Kernel Finite Heisenberg Weyl Event Operator Weyl Event Site27 C

The 27-site carrier

A site is a single address in a discrete model. The declaration weylEventSite27_card proves that the carrier, a function from three axes each holding three phases, has exactly 27 distinct addresses. The proof is a short chain: the number of functions from a set of size 3 to a set of size 3 is 3^3, which is 27.

This is a theorem in the machine-checked library of formal theorems, meaning the count is derived from the definitions with no unproved assumptions. The carrier is not a physical space; it is a finite collection of points used to build a model of recognition events, where each event is a change in the state at one of these addresses.

The theorem itself is narrow. It does not establish that this carrier is the only possible one, nor that it represents physical space. It does not define the dynamics on the sites, nor does it claim that the number 27 has any special meaning beyond being the product of three axes with three phases each. The count is a foundation, not a conclusion.

In the framework, this finite grid is the stage for a recognition event, a discrete record of a change. The theorem guarantees the stage has the right number of seats. What happens on those seats, the rules of the event, is a separate model choice, not a consequence of the count.

The practical consequence is that any later construction on this carrier can rely on the exact number 27 in its proofs. The count is not an approximation or a convention; it is a proved fact about the defined object. This lets the framework build further results on a solid, finite base.

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

What this page does not claim

This theorem does not claim that the 27-site carrier is the only possible model. This theorem does not claim that the carrier represents physical three-dimensional space. This theorem does not define the dynamics or rules for events on the sites.

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: