SignFlipFalsifier
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.