CoherenceGateFalsifier
plain-language theorem explainer
Recognition Science treats Ning Li's gravitomagnetic coupling as coherence-gated, so the effect must disappear once the superconductor loses its condensate above Tc. CoherenceGateFalsifier encodes this requirement as a predicate on real numbers: measured coupling is forced to zero (approximately) when T exceeds Tc and required to be positive below Tc. Experimental tests of the Li-Torr claim would invoke this predicate to check consistency with the RS interpretation. The definition is a direct conditional with no lemmas or reductions.
Claim. The coherence gate falsifier asserts that if temperature $T$ exceeds critical temperature $T_c$, then measured coupling strength is approximately zero; otherwise the measured coupling is strictly positive.
background
The module formalizes Ning Li and D.G. Torr's 1991 claim inside Recognition Science by recasting the gravitomagnetic field inside a superconductor as a coherence-gated source term. The applied field $B_0$ couples to an induced gravitomagnetic component $B_g$ only while the Cooper-pair condensate maintains recognition coherence; above the transition this coupling is cancelled by phase decoherence. The definition therefore supplies the minimal predicate that any RS-consistent model of the effect must satisfy.
proof idea
The declaration is a primitive definition whose body is a direct if-then-else on the comparison $T > T_c$, returning the Prop that measured_coupling is approximately zero or strictly positive accordingly. No upstream lemmas are invoked; the construction relies only on the real-number ordering and the approximation relation already present in the ambient Mathlib import.
why it matters
This definition supplies the explicit falsification criterion for the RS hypothesis on Li-Torr coherent gravitomagnetism stated in the module header. It isolates the coherence-gating condition that distinguishes the RS reading from ordinary electromagnetism and prepares the ground for later integration with the eight-tick octave and J-cost machinery. With zero downstream uses recorded, it functions as a standing hypothesis interface whose discharge would require either an empirical counter-example or a theorem linking the predicate to the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.