Gravity Analysis Regge Ttgate Bbridge Edge Midpoint Phase Grounded

The midpoint phase identity

In the Recognition Science framework's analysis of a discretized gravity model, the declaration edgeMidpointPhase_grounded establishes a precise identity about a quantity called the midpoint Bloch phase. This phase is a number attached to the midpoint of an edge in a periodic cell, and it encodes how a wave-like state changes as you move from one cell to the next. The theorem states that for any momentum vector and any choice of edge, this midpoint phase is exactly equal to a sum involving the slot displacement table, a preregistered list of offsets. In plain terms, it proves that a table used in the calculation is not an arbitrary choice but is exactly what the geometry dictates.

The identity is stated for the smallest non-trivial periodic torus, with a side length of four cells. The theorem's importance is that it connects a literal table of numbers, the slotMidTwice table, to the actual physical setup. This is a grounding step: it ensures that the table is not a transcription error or a convenient fiction, but is derived from the real geometry of the cell. The proof is a machine-checked theorem, meaning it has been verified by a computer program that checks every logical step, with no gaps and no unproven assumptions beyond the standard logical axioms.

This grounding is part of a larger effort to verify a complex calculation in the framework's gravity analysis. The calculation involves summing contributions from 216 different configurations within a single cell. The edgeMidpointPhase_grounded theorem is a key step in showing that a particular way of organizing these contributions, called the bucket fold, is equivalent to a direct sum over all configurations. This equivalence is itself a proved theorem, and it is a necessary component for the final result that the raw stencil's moment matches a previously committed expression.

What the theorem does not claim is also important. It does not, by itself, establish the final equality between the raw stencil moment and the committed spike expression; that is a separate, larger theorem that chains together several results. It also does not invoke or depend on the seven transverse-traceless (TT) hypotheses that are part of the broader framework. The identity holds unconditionally, for all values of the input parameters, which is a stronger statement than one that would require those hypotheses. Finally, it does not claim anything about the physical interpretation of the midpoint phase beyond its mathematical definition within the model.

/-- GROUNDING (THEOREM): the literal doubled-midpoint table reproduces
the ACTUAL preregistered midpoint Bloch phase of the periodic geometry:
for every momentum `k` and slot, the midpoint phase of the local edge at
the base cell is `sum_i k_i * (slotMidTwice t f i) / 2` (stated at the
smallest campaign torus `N = 4` with the base cell; the offsets are
cell-relative by construction). -/
theorem edgeMidpointPhase_grounded (k : Fin 3 → ℝ) (t f : Fin 6) :
    edgeMidpointPhase 4 k
        (localEdgeOf (((0 : Fin 4), (0 : Fin 4), (0 : Fin 4)) :
          Vertex 4 4 4) t f) =
      ∑ i : Fin 3, k i * (((slotMidTwice t f i : ℤ) : ℝ) / 2) := by
  fin_cases t <;> fin_cases f <;>
    · simp only [edgeMidpointPhase, Fin.sum_univ_three, vertCoord,
        localEdgeOf, addVertexBits, addBits, addBit, bit, vertexBits,
        cubeEdgeBase, cubeEdgeDisp,
        Geometry.FreudenthalCubeTriangulation.localEdgeOf,
        FreudenthalStencilPreflight.dispReal, slotMidTwice]
      push_cast
      norm_num

What this page does not claim

This theorem does not establish the final equality between the raw stencil moment and the committed spike expression. This theorem does not invoke the seven TT hypotheses. This theorem does not make any claim about the physical interpretation of the midpoint phase beyond its mathematical definition.

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/Gravity/Analysis/ReggeTTGateBBridge.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: