Masses Mass Genesis T10 Counting Bridge Obstruction Gap One Load Not Block Combi

/-- **B-1, gap-one (THEOREM).** The anchor load `phi^42 / 4` is not a finite
integer combination of block energies, with any multiplicities, signed or
unsigned. The would-be representation forces `4 ∣ F_41`, and
`F_41 = 165580141 ≡ 1 (mod 4)`. -/
theorem gapOneLoad_not_block_combination (s : Finset ℕ) (c : ℕ → ℤ) :
    (∑ n ∈ s, (c n : ℝ) * ((Constants.phi : ℝ)⁻¹) ^ n) ≠
      (Constants.phi : ℝ) ^ 42 / 4 := by
  obtain ⟨A, B, hAB⟩ := combo_reduce s c
  intro h
  rw [hAB] at h
  have h4 : 4 * (((A : ℝ)) * Constants.phi + ((B : ℝ))) =
      (Constants.phi : ℝ) ^ 42 := by linear_combination 4 * h
  rw [phi_pow_fib] at h4
  have key : (((4 * A - (Nat.fib 42 : ℤ)) : ℤ) : ℝ) * Constants.phi +
      (((4 * B - ((Nat.fib 43 : ℤ) - (Nat.fib 42 : ℤ))) : ℤ) : ℝ) = 0 := by
    push_cast
    linear_combination h4
  obtain ⟨-, h2⟩ := int_combination_eq_zero key
  have hf43 : (Nat.fib 43 : ℤ) - (Nat.fib 42 : ℤ) = (Nat.fib 41 : ℤ) := by
    rw [Nat.fib_add_two (n := 41)]
    push_cast
    ring
  rw [hf43] at h2
  have hval : Nat.fib 41 = 165580141 := by decide
  rw [hval] at h2
  omega

/-- **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

/-- **`{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⟩