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

CoherenceGateFalsifier

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  53def CoherenceGateFalsifier (T Tc : ℝ) (measured_coupling : ℝ) : Prop :=

proof body

Definition body.

  54  if T > Tc then
  55    measured_coupling ≈ 0
  56  else
  57    measured_coupling > 0
  58
  59/-- RS Falsifier: Sign Flip.
  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). -/

depends on (9)

Lean names referenced from this declaration's body.