124theorem cooper_pairing_yields_persistent 125 (x : ℝ) (hx : 0 < x) : 126 ∃ e : RecognitionEvent, IsPersistent e := by
proof body
Tactic-mode proof.
127 refine ⟨{ 128 state := x * x⁻¹, 129 state_pos := by 130 rw [mul_inv_cancel₀ (ne_of_gt hx)]; norm_num 131 }, ?_⟩ 132 show Cost.Jcost (x * x⁻¹) = 0 133 exact cooper_pair_cost_zero x hx 134 135/-! ## §5. The Observer -/ 136 137/-- An observer is a coherent recognition structure equipped with a 138 persistent reference event. The observer integrates multiple 139 distinguishable recognition events against a single fixed 140 identity-tick reference. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.