superconductor_effective_source

formal source

 130/-- The effective gravitational source of a superconductor depends on its state.
 131    Below T_c: coherent → N × amplitude.
 132    Above T_c: incoherent → √N × amplitude. -/
 133def superconductor_effective_source (sc : Superconductor) (coherent : Bool) : ℝ :=
 134  if coherent then coherent_effective_source sc.cooper_pairs
 135  else incoherent_effective_source sc.cooper_pairs
 136
 137/-- COHERENCE GATE: Cooling below T_c enhances effective source by √N.
 138    This is the "Coherence Gate" from the RS Antigravity Whitepaper. -/
 139theorem coherence_gate (sc : Superconductor) (hN : 2 ≤ sc.cooper_pairs.N) :
 140    incoherent_effective_source sc.cooper_pairs <
 141    superconductor_effective_source sc true := by
 142  simp only [superconductor_effective_source, ite_true]
 143  exact coherent_exceeds_incoherent sc.cooper_pairs hN
 144
 145/-! ## 6. Certificate -/
 146
 147structure CoherenceGainCert where
 148  gain_is_sqrt_N : ∀ ens : Ensemble, coherence_gain ens = Real.sqrt ens.N
 149  coherent_beats_incoherent : ∀ ens : Ensemble, 2 ≤ ens.N →
 150    incoherent_effective_source ens < coherent_effective_source ens
 151  superconductor_gate : ∀ sc : Superconductor, 2 ≤ sc.cooper_pairs.N →
 152    incoherent_effective_source sc.cooper_pairs < superconductor_effective_source sc true
 153
 154theorem coherence_gain_certified : CoherenceGainCert where
 155  gain_is_sqrt_N := coherence_gain_eq_sqrt_N
 156  coherent_beats_incoherent := coherent_exceeds_incoherent
 157  superconductor_gate := fun sc hN => coherence_gate sc hN
 158
 159end IndisputableMonolith.Gravity.CoherenceGain