module module

`IndisputableMonolith.Gravity.EightTickResonance`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (24)

def interpolation_cost L32
theorem interpolation_cost_nonneg L35
theorem interpolation_cost_le_half L39
theorem interpolation_cost_zero_at_integer L46
def C_lag L54
theorem C_lag_pos L56
def w_resonant L64
theorem w_resonant_ge_one L67
theorem w_at_resonance L72
theorem w_off_resonance L77
theorem weight_reduction_at_resonance L84
def resonant_frequency L94
theorem resonant_frequency_pos L97
theorem resonant_frequency_decreasing L104
structure EightTickResonanceCert L121
theorem eight_tick_resonance_certified L127
theorem C_lag_eq_cLagLock_inv L146
theorem w_resonant_bounded_above L151
theorem eight_tick_period L159
def w_total L187
theorem w_total_at_resonance L191
theorem w_total_exceeds_secular L196
theorem resonance_weight_reduction_ratio L205
theorem shared_coupling L214