Encyclopedia Gravity Gravity Analysis Regge Ttgate Bbridge Gate B Convention Bridge

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Ttgate Bbridge Gate B Convention Bridge

A machine-checked proof that two very different ways of computing a gravity-theory quantity agree exactly, with no hypotheses needed.

Verify this page

The convention bridge

In the Recognition Science framework's study of gravity, a central quantity is a moment, a kind of weighted average that summarizes how a geometric object responds to a small push. The framework's library computes this moment in two distinct ways. The first way starts from a raw stencil, a fixed discrete pattern of points on a small torus, and aggregates its 216 individual contributions bucket by bucket. The second way starts from a separate, hand-committed expression built from six named blocks. The declaration gateB_convention_bridge is a machine-checked theorem stating that these two computations produce exactly the same number for every possible input.

The equality is not approximate and not conditional. It holds identically for every choice of the two input functions, E and x, which encode the geometry and the direction of the push. The proof chains together three intermediate results: the bucket fold equals the plain sum over all 216 triples, each individual term in the raw sum equals the corresponding term in the committed expression, and the full 216-term sum equals the six-block expression. The final theorem then closes the panel-locked target GateBConventionTarget, which is the formal statement of the convention bridge.

A notable feature is disclosed in the proof itself: the seven hypotheses of the target proposition, called the TT equations, are introduced but never actually used. The equality holds before any of those hypotheses are applied. The theorem is therefore stronger than its stated form, and the stronger unconditional version is exported separately as rawMoment_eq_committedSpikeLHS. The spike's own certificate and its specific numerical conclusion are never invoked; only its six block terms are used as data.

All of this is finite algebra over a fixed table. The expected axiom footprint of every theorem in the file is the standard trio [propext, Classical.choice, Quot.sound], with no sorry, no admit, and no new axioms. The declaration does not claim that the TT equations hold, does not derive the spike's numerical conclusion, and does not establish any physical prediction about gravity. It establishes one thing: two different formal expressions for the same moment are identically equal.

THEOREM gateB_convention_bridge · rawMoment_eq_committedSpikeLHS · IndisputableMonolith/Gravity/Analysis/ReggeTTGateBBridge.lean
gateB_convention_bridge · IndisputableMonolith/Gravity/Analysis/ReggeTTGateBBridge.lean:232 
/-- **GATE C-B HEADLINE (THEOREM): the panel-locked Gate B target is
closed on the raw-stencil instantiation.**  `GateBConventionTarget`
(exactly the sidecar's Prop) holds for the raw-stencil support, the
midpoint-displacement phase quadratic, and the bucket-fiber-aggregated
amplitude, for every `E` and `x`.  DISCLOSURE: the seven TT antecedents
of the locked Prop are introduced but not consumed, because the bridge
equality holds identically in `(E, x)`
(`rawMoment_eq_committedSpikeLHS`); the locked statement shape is closed
a fortiori and the stronger unconditional theorem is exported above. -/
theorem gateB_convention_bridge (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ) :
    GateBConventionTarget rawMomentSupport (rawPhaseQuadratic x)
      (rawBucketAmplitude E) E x := by
  intro _ _ _ _ _ _ _
  exact rawMoment_eq_committedSpikeLHS E x
rawMoment_eq_committedSpikeLHS · IndisputableMonolith/Gravity/Analysis/ReggeTTGateBBridge.lean:215 
/-- **THE UNCONDITIONAL BRIDGE (THEOREM): the raw-stencil moment fold
equals the committed spike LHS IDENTICALLY in `(E, x)`.**  Chains the
fiber-aggregation fold, the pointwise identification, and the core
216-term identity at `s2 = sqrt 2`, `s3 = sqrt 3`, `p = pi` (the
sidecar's committed instantiation; the core identity holds for free
values).  The spike's `tt_continuum_certificate` and its `-1/4`
conclusion are never invoked: only the block data `tetBlock0..5`. -/
theorem rawMoment_eq_committedSpikeLHS (E : Fin 3 → Fin 3 → ℝ)
    (x : Fin 3 → ℝ) :
    reggeTTMoment rawMomentSupport (rawPhaseQuadratic x)
        (rawBucketAmplitude E) =
      committedSpikeLHS (spikeInput E x) := by
  rw [reggeTTMoment_eq_rawTripleSum]
  rw [Finset.sum_congr rfl fun p _ => tripleTerm_ident E x p]
  rw [coreTripleSum_eq_spikeSum E x (Real.sqrt 2) (Real.sqrt 3) Real.pi]
  rfl
THEOREM gateB_convention_bridge · IndisputableMonolith/Gravity/Analysis/ReggeTTGateBBridge.lean
gateB_convention_bridge · IndisputableMonolith/Gravity/Analysis/ReggeTTGateBBridge.lean:232 
/-- **GATE C-B HEADLINE (THEOREM): the panel-locked Gate B target is
closed on the raw-stencil instantiation.**  `GateBConventionTarget`
(exactly the sidecar's Prop) holds for the raw-stencil support, the
midpoint-displacement phase quadratic, and the bucket-fiber-aggregated
amplitude, for every `E` and `x`.  DISCLOSURE: the seven TT antecedents
of the locked Prop are introduced but not consumed, because the bridge
equality holds identically in `(E, x)`
(`rawMoment_eq_committedSpikeLHS`); the locked statement shape is closed
a fortiori and the stronger unconditional theorem is exported above. -/
theorem gateB_convention_bridge (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ) :
    GateBConventionTarget rawMomentSupport (rawPhaseQuadratic x)
      (rawBucketAmplitude E) E x := by
  intro _ _ _ _ _ _ _
  exact rawMoment_eq_committedSpikeLHS E x
THEOREM gateB_convention_bridge · IndisputableMonolith/Gravity/Analysis/ReggeTTGateBBridge.lean
gateB_convention_bridge · IndisputableMonolith/Gravity/Analysis/ReggeTTGateBBridge.lean:232 
/-- **GATE C-B HEADLINE (THEOREM): the panel-locked Gate B target is
closed on the raw-stencil instantiation.**  `GateBConventionTarget`
(exactly the sidecar's Prop) holds for the raw-stencil support, the
midpoint-displacement phase quadratic, and the bucket-fiber-aggregated
amplitude, for every `E` and `x`.  DISCLOSURE: the seven TT antecedents
of the locked Prop are introduced but not consumed, because the bridge
equality holds identically in `(E, x)`
(`rawMoment_eq_committedSpikeLHS`); the locked statement shape is closed
a fortiori and the stronger unconditional theorem is exported above. -/
theorem gateB_convention_bridge (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ) :
    GateBConventionTarget rawMomentSupport (rawPhaseQuadratic x)
      (rawBucketAmplitude E) E x := by
  intro _ _ _ _ _ _ _
  exact rawMoment_eq_committedSpikeLHS E x

What this page does not claim

The declaration does not prove that the seven TT equations hold. The declaration does not derive the spike's numerical -1/4 conclusion. The declaration does not establish any physical prediction about gravity.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND