pith. machine review for the scientific record. sign in
def definition def or abbrev high

SignFlipFalsifier

show as:
view Lean formalization →

The declaration encodes the sign-reversal requirement for the induced gravitomagnetic field under negation of the applied field B_0. Researchers examining Ning Li's coherent gravitomagnetism hypothesis within Recognition Science would cite it to enforce vector-field consistency. The definition consists of a direct equality on the induced field function.

claimThe induced gravitomagnetic field satisfies $B_g(-B_0) = -B_g(B_0)$, where $B_g$ is the function that maps applied field strength to the induced gravitomagnetic component.

background

In the Recognition Science framework the Li module formalizes Ning Li's 1991 claim that a superconductor produces an internal gravitomagnetic field $B_g(z)$ coupled to the external magnetic field $B_0$ through a coherence factor involving the mass-to-charge ratio. The module treats this coupling as a coherence-gated source term that restores an underlying gravitomagnetic interaction normally cancelled by random phase walk in the Cooper-pair condensate. The upstream result from Flight.Falsifiers supplies the analogous sign-flip condition for thrust under an external handedness reversal.

proof idea

This is a one-line definition that directly asserts the functional equality induced_Bg(-B_0) = -induced_Bg(B_0).

why it matters in Recognition Science

The definition supplies the concrete falsifier condition for the Li candidate inside the Gravity.Candidates hierarchy. It is referenced by Flight.Falsifiers.SignFlipFalsifier and by the display-level FlightReport summary. The property aligns with the RS reading of Li's formula as a coherence-gated restoration, consistent with the eight-tick octave and the recognition composition law that governs sign behavior under field reversal.

scope and limits

formal statement (Lean)

  63def SignFlipFalsifier (B_0 : ℝ) (induced_Bg : ℝ → ℝ) : Prop :=

proof body

Definition body.

  64  induced_Bg (-B_0) = -induced_Bg B_0
  65
  66end Li
  67end Candidates
  68end Gravity
  69end IndisputableMonolith

used by (2)

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

depends on (1)

Lean names referenced from this declaration's body.