module module

`IndisputableMonolith.Gravity.RecordFluxStress`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.ClausiusEinsteinBridge module_import
IndisputableMonolith.Holography.LocalRecognitionHorizonCut module_import

declarations in this module (21)

def eventStress L38
theorem eventStress_symmetric L43
lemma sum_mul_sq L50
theorem quadContr_eventStress L75
theorem eventStress_zero_of_covector_zero L95
theorem quadContr_eventStress_zero_of_covector_zero L102
abbrev ExteriorCutChannel L109
def channelBitReadout L112
def channelDeltaZ L120
def channelDelta L127
def cutEventStress L136
theorem cutEventStress_symmetric L142
theorem quadContr_cutEventStress L148
theorem cutEventStress_zero_of_covector_zero L158
theorem eventStress_ne_zero_of_unit_channel L168
def bitDelta L177
lemma recordFlux_eq_sum_bitDelta L180
lemma exteriorRecord_as_channels L184
lemma zipWith_bitDelta_ofFn L191
lemma sum_ofFn_eq_sum L201
theorem exteriorStepHeat_eq_sum_channelDeltaZ L209