MarkedCleanup.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.marked_duplicate_replacement line 12

Source documentation

Takenouchi's duplicate replacement preserves every odd divisor of the repeated denominator.

theorem marked_duplicate_replacement (m : ℕ) (hm : 3 ≤ m) :
    ∃ u v : ℕ, 1 ≤ u ∧ 1 ≤ v ∧ u < m ∧
      2 * m < u + v ∧
      (2 : ℚ) / (m : ℚ) = 1 / (u : ℚ) + 1 / (v : ℚ) ∧
      (∀ Q : ℕ, Odd Q → Q ∣ m → Q ∣ v) := by
…

Mentions: OAI.Problem337.v

theorem OAI.Problem337.odd_marker_denominator_ge_three line 44
Source documentation
An odd marker greater than one forces its denominator to be at least three.
```
theorem odd_marker_denominator_ge_three {Q n : ℕ} (hQ : Odd Q)
    (hQone : 1 < Q) (hn : 0 < n) (hdiv : Q ∣ n) : 3 ≤ n := by
…
```

theorem OAI.Problem337.marked_sum_one_denominators_ge_two line 52

Source documentation

A positive expansion of one carrying an odd marker cannot have denominator one.

theorem marked_sum_one_denominators_ge_two {ι : Type*} [Fintype ι] [DecidableEq ι]
    (n : ι → ℕ) (hn : ∀ i, 0 < n i)
    (hsum : (∑ i, (1 : ℚ) / (n i : ℚ)) = 1)
    {Q : ℕ} (hQ : Odd Q) (hQone : 1 < Q) (hmarker : ∃ i, Q ∣ n i) :
    ∀ i, 2 ≤ n i := by
…

theorem OAI.Problem337.marked_sum_one_duplicate_ge_three line 72

Source documentation

In a marked expansion of one, any repeated denominator is at least three.

theorem marked_sum_one_duplicate_ge_three {ι : Type*} [Fintype ι] [DecidableEq ι]
    (n : ι → ℕ) (hn : ∀ i, 0 < n i)
    (hsum : (∑ i, (1 : ℚ) / (n i : ℚ)) = 1)
    {Q : ℕ} (hQ : Odd Q) (hQone : 1 < Q) (hmarker : ∃ i, Q ∣ n i)
    {i j : ι} (hij : i ≠ j) (heq : n i = n j) : 3 ≤ n i := by
…

theorem OAI.Problem337.marker_update_two line 96

Source documentation

A two-coordinate update retains an odd-divisibility marker whenever removed markers are restored.

theorem marker_update_two {k Q : ℕ} (n : Fin k → ℕ) {i j : Fin k}
    (hij : i ≠ j) (a b : ℕ) (hmarker : ∃ t, Q ∣ n t)
    (hrestore : Q ∣ n i ∨ Q ∣ n j → Q ∣ a ∨ Q ∣ b) :
    ∃ t, Q ∣ Function.update (Function.update n i a) j b t := by
…

theorem OAI.Problem337.marked_cleanup_exact_length line 114

Source documentation

Exact-length cleanup at total one, retaining a denominator divisible by a specified odd integer.

theorem marked_cleanup_exact_length {k Q : ℕ} (hQ : Odd Q) (hQone : 1 < Q)
    (original : Fin k → ℕ) (hpos : ∀ i, 1 ≤ original i)
    (hsum : (∑ i, (1 : ℚ) / (original i : ℚ)) = 1)
    (hmarker : ∃ i, Q ∣ original i) :
    ∃ n : Fin k → ℕ, IsOneExpansion n ∧ ∃ i, Q ∣ n i := by
…

Mentions: OAI.Problem337.IsOneExpansion

theorem OAI.Problem337.marked_cleanup line 163

Source documentation

The at-most-length formulation used in the counting construction.

theorem marked_cleanup {k Q : ℕ} (hQ : Odd Q) (hQone : 1 < Q)
    (original : Fin k → ℕ) (hpos : ∀ i, 1 ≤ original i)
    (hsum : (∑ i, (1 : ℚ) / (original i : ℚ)) = 1)
    (hmarker : ∃ i, Q ∣ original i) :
    ∃ r : ℕ, r ≤ k ∧ ∃ n : Fin r → ℕ, IsOneExpansion n ∧ ∃ i, Q ∣ n i := by
…

Mentions: OAI.Problem337.IsOneExpansion