import CubicPathwidth.T3Spec
import CubicPathwidth.T2.FcubicBounds

/-!
# Elementary facts about the Theorem 3 edge-correlation floors

Values and bounds for `rFloor i j = sech (¼ ln ((i-1)(j-1)))` and for the
cubic constant `Fcubic`, used by the degree-5 proof. No new hypotheses.
-/

namespace CubicPathwidth
namespace T3

/-- For `i, j ≥ 3` the argument `¼ ln ((i-1)(j-1))` of `cosh` is positive. -/
private theorem rFloor_arg_pos {i j : ℕ} (hi : 3 ≤ i) (hj : 3 ≤ j) :
    0 < Real.log (((i : ℝ) - 1) * ((j : ℝ) - 1)) / 4 := by
  have hi' : (3 : ℝ) ≤ (i : ℝ) := by exact_mod_cast hi
  have hj' : (3 : ℝ) ≤ (j : ℝ) := by exact_mod_cast hj
  have h4 : (1 : ℝ) < ((i : ℝ) - 1) * ((j : ℝ) - 1) := by
    nlinarith [mul_nonneg (sub_nonneg.2 hi') (sub_nonneg.2 hj')]
  have := Real.log_pos h4
  linarith

/-- For `i, j ≥ 3` the cosine-hyperbolic argument is nonzero, so `cosh > 1`. -/
private theorem one_lt_cosh_arg {i j : ℕ} (hi : 3 ≤ i) (hj : 3 ≤ j) :
    1 < Real.cosh (Real.log (((i : ℝ) - 1) * ((j : ℝ) - 1)) / 4) := by
  have hx := rFloor_arg_pos hi hj
  set x := Real.log (((i : ℝ) - 1) * ((j : ℝ) - 1)) / 4 with hxdef
  have ht : 1 < Real.exp x := Real.one_lt_exp_iff.2 hx
  have hmul : Real.exp x * Real.exp (-x) = 1 := by
    rw [← Real.exp_add]; simp
  have hs_pos : 0 < Real.exp (-x) := Real.exp_pos _
  have hs1 : Real.exp (-x) < 1 := by
    nlinarith [mul_pos (sub_pos.2 ht) hs_pos]
  rw [Real.cosh_eq]
  nlinarith [mul_pos (sub_pos.2 ht) (sub_pos.2 hs1)]

theorem rFloor_pos {i j : ℕ} (hi : 3 ≤ i) (hj : 3 ≤ j) : 0 < rFloor i j := by
  unfold rFloor
  exact div_pos one_pos (Real.cosh_pos _)

theorem rFloor_lt_one {i j : ℕ} (hi : 3 ≤ i) (hj : 3 ≤ j) : rFloor i j < 1 := by
  unfold rFloor
  rw [div_lt_one (Real.cosh_pos _)]
  exact one_lt_cosh_arg hi hj

theorem rFloor_34 : rFloor 3 4 = T2.r34 := by
  have h : (((3 : ℕ) : ℝ) - 1) * (((4 : ℕ) : ℝ) - 1) = 6 := by norm_num
  unfold rFloor T2.r34
  rw [h]

theorem rFloor_43 : rFloor 4 3 = T2.r34 := by
  have h : (((4 : ℕ) : ℝ) - 1) * (((3 : ℕ) : ℝ) - 1) = 6 := by norm_num
  unfold rFloor T2.r34
  rw [h]

theorem rFloor_33 : rFloor 3 3 = T2.r33 := by
  have hA : (((3 : ℕ) : ℝ) - 1) * (((3 : ℕ) : ℝ) - 1) = 4 := by norm_num
  have h4 : Real.log 4 = 2 * Real.log 2 := by
    rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]
    push_cast
    ring
  have harg : Real.log 4 / 4 = Real.log 2 / 2 := by
    rw [h4]
    ring
  have hs : Real.exp (Real.log 2 / 2) = Real.sqrt 2 := by
    rw [Real.exp_half, Real.exp_log (by norm_num)]
  have hsq : Real.sqrt 2 * Real.sqrt 2 = 2 := Real.mul_self_sqrt (by norm_num)
  have hpos : 0 < Real.sqrt 2 := by positivity
  have hinv : (Real.sqrt 2)⁻¹ = Real.sqrt 2 / 2 := by
    field_simp
    linarith [hsq]
  unfold rFloor T2.r33
  rw [hA, harg, Real.cosh_eq, Real.exp_neg, hs, hinv]
  field_simp
  nlinarith [hsq, hpos]

theorem rFloor_44 : rFloor 4 4 = T2.r44 := by
  have hA : (((4 : ℕ) : ℝ) - 1) * (((4 : ℕ) : ℝ) - 1) = 9 := by norm_num
  have h9 : Real.log 9 = 2 * Real.log 3 := by
    rw [show (9 : ℝ) = 3 ^ 2 by norm_num, Real.log_pow]
    push_cast
    ring
  have harg : Real.log 9 / 4 = Real.log 3 / 2 := by
    rw [h9]
    ring
  have hs : Real.exp (Real.log 3 / 2) = Real.sqrt 3 := by
    rw [Real.exp_half, Real.exp_log (by norm_num)]
  have hsq : Real.sqrt 3 * Real.sqrt 3 = 3 := Real.mul_self_sqrt (by norm_num)
  have hpos : 0 < Real.sqrt 3 := by positivity
  have hinv : (Real.sqrt 3)⁻¹ = Real.sqrt 3 / 3 := by
    field_simp
    linarith [hsq]
  unfold rFloor T2.r44
  rw [hA, harg, Real.cosh_eq, Real.exp_neg, hs, hinv]
  field_simp
  nlinarith [hsq, hpos]

theorem Fcubic_nonneg : 0 ≤ T2.Fcubic :=
  le_trans (by norm_num) T2.Fcubic_ge

theorem triple_P_mono : T2.Fcubic ≤ 103 / 400 ∧ (103 / 400 : ℝ) ≤ 3667 / 10000 :=
  ⟨T2.Fcubic_le, by norm_num⟩

end T3
end CubicPathwidth

#print axioms CubicPathwidth.T3.rFloor_33
#print axioms CubicPathwidth.T3.rFloor_lt_one