module module

`IndisputableMonolith.Gravity.Analysis.ReggeTTBlochInterfaceAudit`

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 (2)

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

IndisputableMonolith.Gravity.Analysis.ReggeTTBlochConventionAudit module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTBucketAggregation module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeTTFlatSecondVariation module_import

declarations in this module (20)

structure RawCellStencilTerm L50
abbrev PhaseVector L57
structure Bucket L62
def negPhase L69
def rationalStencilWeight L78
def canonicalFiniteH L85
def rawCellStencilTerm L94
def rawCellStencil L104
theorem a2_reduced_eq_rawCellStencil L115
def row0SmokeBucket L130
def rawJacobianCoefficient L135
theorem row0Smoke_raw_weight_eq_rational L141
theorem row0Smoke_table_value L153
def worstRadicalBucket L160
theorem worstRadical_flatAngleJacobian_value L168
theorem worstRadical_rawJacobianCoefficient_closedForm L190
def reggeTTBlochFold L202
def reggeTTAssembledSymbol L207
def reggeTTMoment L215
def stencilOnlyConstantWitnessResidual L223