Masses Mass Genesis T10 Counting Bridge Obstruction Phi Pow Div Two Pow Not Bloc

/-- **B-1, general (THEOREM).** No pure ladder power with a power-of-two
denominator is a finite integer combination of block energies:
`phi^k / 2^j`, `j ≥ 1`, would force `2 ∣ F_k` and `2 ∣ F_{k-1}`, and
consecutive Fibonacci numbers are coprime. -/
theorem phiPow_div_twoPow_not_block_combination (s : Finset ℕ) (c : ℕ → ℤ)
    (k j : ℕ) (hj : 1 ≤ j) :
    (∑ n ∈ s, (c n : ℝ) * ((Constants.phi : ℝ)⁻¹) ^ n) ≠
      (Constants.phi : ℝ) ^ k / (2 ^ j : ℝ) := by
  obtain ⟨A, B, hAB⟩ := combo_reduce s c
  intro h
  rw [hAB] at h
  have hj0 : (2 : ℝ) ^ j ≠ 0 := by positivity
  have h2j : (2 ^ j : ℝ) * (((A : ℝ)) * Constants.phi + ((B : ℝ))) =
      (Constants.phi : ℝ) ^ k := by
    field_simp at h
    linear_combination h
  rw [phi_pow_fib] at h2j
  have key : ((((2 : ℤ) ^ j * A - (Nat.fib k : ℤ)) : ℤ) : ℝ) * Constants.phi +
      ((((2 : ℤ) ^ j * B - ((Nat.fib (k + 1) : ℤ) - (Nat.fib k : ℤ))) : ℤ) : ℝ)
      = 0 := by
    push_cast
    linear_combination h2j
  obtain ⟨h1, h2⟩ := int_combination_eq_zero key
  have d1 : (2 : ℤ) ^ j ∣ (Nat.fib k : ℤ) := ⟨A, by linear_combination -h1⟩
  have d2 : (2 : ℤ) ^ j ∣ ((Nat.fib (k + 1) : ℤ) - (Nat.fib k : ℤ)) :=
    ⟨B, by linear_combination -h2⟩
  have h2dvd : (2 : ℤ) ∣ (2 : ℤ) ^ j := dvd_pow_self 2 (by omega)
  have e1 : (2 : ℤ) ∣ (Nat.fib k : ℤ) := h2dvd.trans d1
  have e2 : (2 : ℤ) ∣ ((Nat.fib (k + 1) : ℤ) - (Nat.fib k : ℤ)) :=
    h2dvd.trans d2
  rcases Nat.eq_zero_or_pos k with rfl | hk
  · norm_num [Nat.fib] at e2
  · have hf : (Nat.fib (k + 1) : ℤ) - (Nat.fib k : ℤ) =
        (Nat.fib (k - 1) : ℤ) := by
      have h := Nat.fib_add_two (n := k - 1)
      rw [show k - 1 + 2 = k + 1 by omega, show k - 1 + 1 = k by omega] at h
      rw [h]
      push_cast
      ring
    rw [hf] at e2
    have e1' : 2 ∣ Nat.fib k := Int.ofNat_dvd.mp (by exact_mod_cast e1)
    have e2' : 2 ∣ Nat.fib (k - 1) := Int.ofNat_dvd.mp (by exact_mod_cast e2)
    have g : 2 ∣ Nat.gcd (Nat.fib k) (Nat.fib (k - 1)) := Nat.dvd_gcd e1' e2'
    rw [← Nat.fib_gcd] at g
    have hcop : Nat.gcd k (k - 1) = 1 := by
      have hd1 : Nat.gcd k (k - 1) ∣ k := Nat.gcd_dvd_left _ _
      have hd2 : Nat.gcd k (k - 1) ∣ (k - 1) := Nat.gcd_dvd_right _ _
      have hd3 : Nat.gcd k (k - 1) ∣ (k - (k - 1)) := Nat.dvd_sub hd1 hd2
      have hkk : k - (k - 1) = 1 := by omega
      rw [hkk] at hd3
      exact Nat.dvd_one.mp hd3
    rw [hcop] at g
    norm_num at g

/-- **Every finite block combination has integer coefficients:** a sum of
signed multiples of block energies is `A * phi + B` with `A, B` integers. -/
theorem combo_reduce (s : Finset ℕ) (c : ℕ → ℤ) :
    ∃ A B : ℤ, (∑ n ∈ s, (c n : ℝ) * ((Constants.phi : ℝ)⁻¹) ^ n) =
      ((A : ℝ)) * Constants.phi + ((B : ℝ)) := by
  classical
  refine s.induction_on ⟨0, 0, by simp⟩ ?_
  intro n s hn ih
  obtain ⟨A, B, hAB⟩ := ih
  refine ⟨A - (c n) * (-1) ^ n * (Nat.fib n : ℤ),
    B + (c n) * (-1) ^ n * (Nat.fib (n + 1) : ℤ), ?_⟩
  rw [Finset.sum_insert hn, hAB, phiInv_pow]
  push_cast
  ring

theorem irrational_phi : Irrational Constants.phi := by
  rintro ⟨q, hq⟩
  have h5 : Real.sqrt 5 = (((2 * q - 1 : ℚ)) : ℝ) := by
    have h1 : Constants.phi = (1 + Real.sqrt 5) / 2 := rfl
    rw [h1] at hq
    have h2 : Real.sqrt 5 = 2 * (q : ℝ) - 1 := by linear_combination -2 * hq
    rw [h2]
    push_cast
    ring
  exact irrational_sqrt5 ⟨2 * q - 1, h5.symm⟩

/-- **`{1, phi}` is rationally independent** (integer form). -/
theorem int_combination_eq_zero {a b : ℤ}
    (h : ((a : ℝ)) * Constants.phi + ((b : ℝ)) = 0) : a = 0 ∧ b = 0 := by
  by_cases ha : a = 0
  · subst ha
    simp at h
    exact ⟨rfl, by exact_mod_cast h⟩
  · exfalso
    have hane : (a : ℝ) ≠ 0 := by exact_mod_cast ha
    have hphi : Constants.phi = (((-(b : ℚ) / (a : ℚ)) : ℚ) : ℝ) := by
      push_cast
      field_simp
      linear_combination h
    exact irrational_phi ⟨-(b : ℚ) / (a : ℚ), hphi.symm⟩