module module

`IndisputableMonolith.Gravity.Analysis.ReggeTTBlochAssembly`

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.ReggeTTContinuumLimit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.BlochCellSum module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode module_import

declarations in this module (26)

def vertexNatCoord L36
def cubeVertexBit L42
def slotBaseBit L48
def cubeDispBit L53
def slotDispBit L59
def slotMidTwice L65
def slotWrapCount L71
def slotWrapTurns L76
def slotPhase L81
def rawCosineEvaluator L87
def bucketKeyOf L95
def rawCosineSupport L101
def rawTripleWeight L105
def rawBucketAmplitude L112
theorem addBit_val_real L116
theorem vertCoord_addVertexBits L134
theorem slotMidTwice_eq_geometry L146
theorem localEdge_phase_decomposition L161
theorem cos_localEdge_eq_cell_slot L196
theorem rawCosineEvaluator_bucketKeyOf L211
theorem neg_rawCellStencilTerm_eq L232
theorem rawCosineFold_eq_rawTripleSum L249
theorem rawTriple_cellSum L267
theorem rawCellStencil_eq_rawCosineBlochFold L300
theorem canonicalFiniteH_eq_rawCosineBlochFold L387
theorem eventually_canonicalFiniteH_eq_rawCosineBlochFold L399