module module

`IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.Analysis.ReggeTTAlgebraicCloser module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeTTBlochConventionAudit module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridgeCore module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode module_import

declarations in this module (13)

theorem edgeMidpointPhase_grounded L111
theorem coreWeight_eq_raw L127
theorem corePolEdgeCoeff_eq L134
theorem slotDispCore_eq L142
def bucketKeyOf L151
def rawMomentSupport L157
def rawPhaseQuadratic L163
def rawTripleWeight L168
def rawBucketAmplitude L176
theorem reggeTTMoment_eq_rawTripleSum L185
theorem tripleTerm_ident L204
theorem rawMoment_eq_committedSpikeLHS L222
theorem gateB_convention_bridge L241