recognition / Gravity / Gravity.Candidates.Li / SignFlipFalsifier

def

`SignFlipFalsifier`

definition

show as: view math explainer →

module: IndisputableMonolith.Gravity.Candidates.Li
domain: Gravity
line: 63 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gravity.Candidates.Li on GitHub at line 63.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

depends on

SignFlipFalsifier IndisputableMonolith.Flight.Falsifiers

used by

formal source

  60    Since B_0 is a vector field, reversing B_0 (or the current) must reverse
  61    the induced gravitomagnetic component.
  62    B_g_induced(-B_0) = -B_g_induced(B_0). -/
  63def SignFlipFalsifier (B_0 : ℝ) (induced_Bg : ℝ → ℝ) : Prop :=
  64  induced_Bg (-B_0) = -induced_Bg B_0
  65
  66end Li
  67end Candidates
  68end Gravity
  69end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.