module module

`IndisputableMonolith.Gravity.SevenGaps.EdgeTensorSector`

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.SevenGaps.CampaignLedger module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.TensorShearSector module_import

declarations in this module (57)

def conformalStrainLinearMap L101
theorem conformalStrainLinearMap_apply L114
theorem isConformalEdgePerturbation_iff_mem_range L120
theorem finrank_vertexPotential L133
theorem finrank_edgePerturbation L138
theorem conformalRange_finrank_le_nV L145
def periodicEdge5EquivProd L153
theorem periodicTorus5_nV_eq L160
theorem periodicTorus5_nE_eq L168
theorem finrank_encodedEdgePerturbation5 L174
theorem periodicTorus5_conformalRange_finrank_le L180
theorem periodicTorus5_conformalRange_finrank_lt_finrank_edgeSpace L188
theorem periodicTorus5_conformalRange_ne_top L197
theorem periodicTorus5_exists_not_mem_conformalRange L206
theorem periodicTorus5_exists_nonconformal L217
theorem periodicConformalLogSubspace5_endpoint_form L228
theorem periodicConformalLogSubspace5_iff_encodedConformal L240
def faceVertexA L260
def faceVertexB L263
def faceVertexC L266
def faceVertexD L269
def faceEdgeAB L272
def faceEdgeDC L275
def faceEdgeBC L278
def faceEdgeAD L281
theorem faceEdgeAB_endpoints L283
theorem faceEdgeDC_endpoints L286
theorem faceEdgeBC_endpoints L289
theorem faceEdgeAD_endpoints L292
def rectangleShearFace5 L298
theorem rectangleShearFace5_apply_AB L305
theorem rectangleShearFace5_apply_DC L308
theorem rectangleShearFace5_apply_BC L312
theorem rectangleShearFace5_apply_AD L317
theorem rectangleShearFace5_apply_of_ne L323
theorem faceEdgeAB_not_mem_rest L329
theorem faceEdgeDC_not_mem_rest L333
theorem faceEdgeBC_not_mem_rest L337
theorem periodicEdgeInnerProduct5_rectangleShearFace5_left L343
theorem rectangleShearFace5_inner_conformal_eq_zero L376
theorem rectangleShearFace5_inner_self_eq_four L392
theorem rectangleShearFace5_ne_zero L399
theorem rectangleShearFace5_nonzero_in_orthogonal_complement L410
theorem rectangleShearFace5_not_conformal_typed L418
def rectangleShearFace5Encoded L426
theorem rectangleShearFace5Encoded_not_conformal L431
theorem periodicTorus5_exists_nonconformal_constructive L440
def xUniformStrain5 L449
theorem xUniformStrain5_apply_AB L452
theorem xUniformStrain5_apply_DC L456
theorem xUniformStrain5_apply_BC L460
theorem xUniformStrain5_apply_AD L464
theorem xUniformStrain5_not_conformal_typed L471
theorem xUniformStrain5Encoded_not_conformal L496
theorem rectangleShearFace5_inner_xUniformStrain5 L506
theorem xUniformStrain5_nonzero_orthogonal_component L516
theorem periodicTorus5_edge_tensor_sector_beyond_conformal L532