structure definition def or abbrev

`Bands`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 106structure Bands where
 107  κ_ppn : ℝ
 108  κ_lensing : ℝ
 109  κ_gw : ℝ
 110  h_ppn : 0 ≤ κ_ppn
 111  h_lensing : 0 ≤ κ_lensing
 112  h_gw : 0 ≤ κ_gw
 113
 114/-- Map ILG parameters to a bands schema (toy: proportional to |C_lag·α|). -/

used by (1)

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

bandsFromParams in IndisputableMonolith.Relativity.ILG.Action decl_use

depends on (2)

Lean names referenced from this declaration's body.

C_lag in IndisputableMonolith.Gravity.EightTickResonance decl_use
Map in IndisputableMonolith.Measurement decl_use