Gravity Analysis Regge Bloch All Orbit Symbol4 D Factorized Bloch Fold Orbit T11

The t11 orbit fold

In lattice gravity, spacetime is chopped into flat pieces, and the curvature is concentrated along their shared edges, the hinges. The Recognition Science framework studies a four-dimensional Regge calculus, a discrete approximation to general relativity where the geometry is carried by edge lengths and deficit angles. The declaration factorizedBlochFoldOrbit_t11_eq concerns one particular symmetry class of hinges, labeled t11, and what happens when you sum a certain product of area and deficit terms over all 240 possible hinge slots in that class.

The central result is an orbit-count identity: the number of slots belonging to the t11 orbit equals the number of slots that satisfy the predicate isT11. This is a proved theorem, not a definitional choice. It is a counting statement about the combinatorial structure of the hinge types. The declaration also proves that at zero momentum, the fold for the t11 orbit reduces to a simple quadratic form, and that the fold is an even function of the momentum scale parameter. These are the concrete, checkable facts the declaration establishes.

In Recognition Science, the framework's library proves these identities as part of a larger project: building a discrete analog of the Bloch symbol, the momentum-space object that encodes how a wave propagates through a periodic lattice. The framework models the all-orbit fold as a sum over the six hinge orbit types, and the t11 orbit is one of them. The evenness result means the fold depends only on the magnitude of the momentum, not its sign, which is a symmetry property that any reasonable lattice propagator should satisfy.

What the declaration does not claim is just as important. It does not prove that this discrete model recovers the continuum Einstein-Hilbert action in any limit. That recovery remains an open target. It does not claim that the one-orbit symbol alone matches the continuum target; in fact, the library explicitly marks a decoy theorem showing that the one-orbit m² moment for the axis configuration is -3, which is not the continuum value. The declaration also does not flip the status flag for gap_action_recovery, meaning the gap between the discrete and continuum actions is not closed by this result.

The practical consequence is a precise, machine-checked accounting of one symmetry class in the discrete gravity model. This is the kind of foundational bookkeeping that must be correct before any larger claim about recovering general relativity can be attempted. The framework's library provides that bookkeeping, and it is honest about what remains open.

theorem isOrbit_t11_iff_isT11 (s : Fin 24) (t : Fin 10) :
    isOrbit .t11 s t ↔ isT11 s t := by
  simp [isOrbit, isT11]

/-- Consistency gate: each orbit fold at zero momentum recovers the
committed `orbitZeroMomQuadratic`. -/
theorem factorizedBlochFoldOrbit_zeroMomentum (ty : HingeOrbitType)
    (H : Mat4) :
    factorizedBlochFoldOrbit ty H (fun _ => (0 : ℝ)) =
      orbitZeroMomQuadratic ty H := by
  unfold factorizedBlochFoldOrbit orbitZeroMomQuadratic
  have hterm : ∀ s t,
      factorizedOrbitSlotTerm ty H (fun _ => (0 : ℝ)) s t =
        (if isOrbit ty s t then (1 : ℝ) else 0) *
          (classDot (orbitAreaCov ty) H *
            classDot (orbitDeficitKernel ty) H) := by
    intro s t
    unfold factorizedOrbitSlotTerm
    by_cases h : isOrbit ty s t <;> simp [h, phasedClassDot_zeroMomentum]
  simp_rw [hterm]
  rw [show
      (∑ s : Fin 24, ∑ t : Fin 10,
          (if isOrbit ty s t then (1 : ℝ) else 0) *
            (classDot (orbitAreaCov ty) H *
              classDot (orbitDeficitKernel ty) H)) =
        (∑ s : Fin 24, ∑ t : Fin 10, (if isOrbit ty s t then (1 : ℝ) else 0)) *
          (classDot (orbitAreaCov ty) H *
            classDot (orbitDeficitKernel ty) H) by
    simp_rw [Finset.sum_mul]]
  rw [orbit_slot_count_real]
  ring

theorem foldOrbitAlong_even (ty : HingeOrbitType) (H : Mat4)
    (dir : Fin 4 → ℝ) : Function.Even (foldOrbitAlong ty H dir) :=
  fun μ => foldOrbitAlong_neg ty H dir μ

/-- DECOY: the closed one-orbit `(1,1)` m² coefficient `-3` is not the
continuum EH target; continuum recovery requires the full all-orbit symbol. -/
theorem decoy_one_orbit_m2_is_not_continuum_target :
    ReggeBlochM2Symbol4D.m2Symbol axisTTPlus = -3 ∧
      blochAllOrbitSymbol4DStatus.continuumEHClosed = false ∧
        blochAllOrbitSymbol4DStatus.oneOrbitIsNotContinuumTarget = true ∧
          blochAllOrbitSymbol4DStatus.gapActionRecovery = false := by
  refine ⟨ReggeBlochM2Symbol4D.m2Symbol_axisTTPlus, rfl, rfl, rfl⟩

What this page does not claim

This declaration does not prove continuum Einstein-Hilbert recovery. This declaration does not claim that the one-orbit symbol matches the continuum target. This declaration does not flip the gap_action_recovery status flag.

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