Foundation Pair Kernel Weyl Event Center Attachment Realized Posting Weyl Center

The posting geometry

A posting, in the Recognition Science framework, is a discrete record of a single recognition event: a pair of sites in a finite carrier, one marked as the clock center and one as the other endpoint. The declaration realizedPostingWeylCenter_respects_primitiveAxisShift27 is a theorem about the geometry of such postings when the carrier is the 27-site Weyl event carrier, a finite grid built from three axes each with three positions. The theorem proves that for every realized posting, the other endpoint differs from the clock center by exactly one primitive axis shift: a move of one step along one of the three axes, either forward or backward. In plain terms, the theorem establishes that the geometry of a single primitive event is always a unit step along one axis, never a diagonal jump, never a two-step move, and never a move that leaves the axis unchanged.

The theorem is proved in the framework's machine-checked library of formal theorems, and the proof is axiom-clean: it uses only the standard logical axioms, with no new assumptions and no empirical constants. The theorem is part of a larger certificate, weylEventCenterAttachment_cert27, which packages the posting geometry together with two other facts: the clock center is the positive endpoint of the posting, and the Fourier transform of the carrier exchanges the shift and clock occupation costs. The certificate is a single object that a consumer can use to reason about the geometry of any realized posting without re-deriving the individual facts.

The theorem does not claim that the two weights, the shift weight and the clock weight, are equal. The framework proves that equal weights are forced only conditionally, on a finite-Fourier exchange-invariance premise, and that premise is not yet supplied by existing Recognition theorems. The physical equal-weight claim therefore remains open. The theorem also does not introduce any dimensioned length: the primitive axis shift is a discrete step in the finite carrier, not a distance in physical space. The theorem is a statement about the combinatorial geometry of the carrier, not about the physical scale of the event.

What the theorem changes is the shape of the reasoning available to the framework. Before the theorem, a realized posting could in principle have any geometry; after the theorem, any posting is known to be a unit step along one axis. This is a structural fact that constrains the possible configurations of the 27-site carrier and supports the framework's larger project of deriving physical structure from the cost of recognition. The theorem is a small but load-bearing piece of the foundation: it pins down the local geometry of a single event, and it does so with a proof that can be checked by a machine.

The theorem's honesty is as important as its content. The framework does not claim that the equal-weight condition is physically realized; it names the missing premise and marks the claim as open. The theorem does not claim that the 27-site carrier is the physical space we inhabit; it is a finite combinatorial model. And the theorem does not claim that the primitive axis shift is a physical length; it is a discrete step in a finite grid. These limits are not afterthoughts; they are part of the theorem's meaning. The theorem proves what it proves, and it leaves the rest open.

/-- A realized primitive posting remains exactly one positive or negative axis
step after transport to the Weyl torus. -/
theorem realizedPostingWeylCenter_respects_primitiveAxisShift27
    (event : RealizedPostingEvent3 3) :
    ∃ axis : Fin 3,
      realizedPostingWeylOtherEndpoint27 event =
          forwardShiftSite27 axis
            (realizedPostingWeylClockCenter27 event) ∨
        realizedPostingWeylOtherEndpoint27 event =
          shiftSite27 axis
            (realizedPostingWeylClockCenter27 event) := by
  obtain ⟨axis, haxis⟩ :=
    realizedProductionEvent_has_spatialWitness event
  refine ⟨axis, ?_⟩
  simpa [ProductionSpatialEventWitness3,
    realizedPostingWeylOtherEndpoint27,
    realizedPostingWeylClockCenter27,
    productionIndexEquivWeylEventSite27,
    PairKernelDeltaSpatialBridgeS5.framedForward,
    PairKernelDeltaSpatialBridgeS5.framedBackward,
    PairKernelPeriodic3.torusShift,
    forwardShiftSite27, shiftSite27, sub_eq_add_neg] using haxis

theorem weylEventCenterAttachment_cert27
    (event : RealizedPostingEvent3 3) :
    WeylEventCenterAttachmentCert27 event where
  center_is_positive_endpoint := rfl
  primitive_axis_transport :=
    realizedPostingWeylCenter_respects_primitiveAxisShift27 event
  dft_exchange_witness :=
    finiteDFTAxis3_discriminating_exchange
  equal_weight_conditional :=
    fun _ _ => finiteFourierExchangeInvariant_forces_equal_weights

/-- A genuine finite-Fourier exchange symmetry would force equal shift and
clock weights.  The conclusion is conditional on `hinvariant`. -/
theorem finiteFourierExchangeInvariant_forces_equal_weights
    {shiftWeight clockWeight : ℝ}
    (hinvariant :
      FiniteFourierExchangeInvariantAxis3
        shiftWeight clockWeight) :
    shiftWeight = clockWeight := by
  have h := hinvariant deltaAxisAmplitude3
  rw [finiteDFTAxis3_delta] at h
  simp only [twoWeightOccupationCostAxis3,
    shiftOccupationCostAxis3_uniform,
    clockOccupationCostAxis3_uniform,
    shiftOccupationCostAxis3_delta,
    clockOccupationCostAxis3_delta,
    mul_zero, add_zero] at h
  linarith

What this page does not claim

The theorem does not claim that the shift and clock weights are equal. The theorem does not introduce any dimensioned length or physical scale. The theorem does not claim that the 27-site carrier is physical space.

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