module module

`IndisputableMonolith.Measurement.C2ABridge`

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.Measurement.BornRule module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Measurement.KernelMatch module_import
IndisputableMonolith.Measurement.PathAction module_import
IndisputableMonolith.Measurement.TwoBranchGeodesic module_import

declarations in this module (6)

def pathFromRotation L28
theorem integral_cot_from_theta L48
theorem measurement_bridge_C_eq_2A L152
theorem weight_bridge L177
theorem weight_equals_born L185
theorem amplitude_modulus_bridge L196