{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiBasePoints.lean",
  "offset": 481,
  "limit": 14
}

{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiBasePoints.lean",
    "content": "    have hsq : (5.3248 : \u211d) ^ 2 \u2264 C0hat (Real.sqrt 80000 + 1) ^ 2 :=\n      pow_le_pow_left\u2080 (by norm_num) hC0lo 2\n    linarith [hsq, hlogT2ge]\n  -- e\u2074 \u2265 54.5978\n  have he4 : (54.5978 : \u211d) \u2264 Real.exp 4 := by\n    rw [exp_four]\n    exact le_trans (by norm_num) (exp_one_pow_ge 4)\n  -- assemble\n  simp only [Bn]\n  -- Z\u2082 T \u2265 6.06 (0.6\u00b75.6 + 0 + 2.7; log log \u2265 0; the corrected count, D-071)\n  have hZ2lo : (6.06 : \u211d) \u2264 Z2hat (Real.sqrt 80000 + 1) := by\n    unfold Z2hat\n    linarith [hlogT2ge, hloglogT2nn]\n  have hbrlo : (110.84 : \u211d) \u2264 (2 / 3 : \u211d) * Z2hat (Real.sqrt 80000 + 1) +",
    "numLines": 14,
    "startLine": 481,
    "totalLines": 701
  }
}