module module

`IndisputableMonolith.Gravity.EchoReflectionCoefficient`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (29)

structure at L38
theorem phi_energy_partition L57
def reflectedFraction L69
def transmittedFraction L72
theorem partition_complete L75
theorem reflectedFraction_pos L82
theorem transmittedFraction_pos L85
theorem reflectedFraction_lt_one L89
theorem transmittedFraction_lt_one L93
def reflectionAmplitude L102
theorem reflectionAmplitude_sq L105
def echoDampingFactor L113
theorem echoDampingFactor_eq_reflectionAmplitude L116
def echoAmplitude L120
theorem echoAmplitude_zero L122
theorem echoAmplitude_succ L125
theorem echo_ratio_constant L132
theorem echo_geometric L140
def phasePerRung L152
theorem phasePerRung_pos L155
def echoPhaseSeparation L163
theorem echoPhaseSeparation_succ L166
structure PhiSelfSimilarBarrier L177
def singleRungBarrier L185
theorem barrier_total_reflection L192
theorem echo_reflection_coefficient_forced L206
structure EchoReflectionCoefficientCert L220
def echoReflectionCoefficientCert L229
theorem echoReflectionCoefficientCert_inhabited L240