ExactPadding.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.one_finset_denominators_ge_two line 12

Source documentation

A nontrivial distinct expansion of one cannot contain denominator one.

theorem one_finset_denominators_ge_two (s : Finset ℕ)
    (hcard : 2 ≤ s.card) (hpos : ∀ b ∈ s, 1 ≤ b)
    (hsum : (∑ b ∈ s, (1 : ℚ) / b) = 1) :
    ∀ b ∈ s, 2 ≤ b := by
…

def OAI.Problem337.PrimePaddingObstruction line 38
Source documentation
Algebraic interface needed to rule out the two exceptional splits at a prime.
```
def PrimePaddingObstruction : Prop :=
…
```

theorem OAI.Problem337.exists_marker_split_of_obstruction line 45

Source documentation

Choose an unmarked denominator with a collision-free two-term split.

theorem exists_marker_split_of_obstruction (hprime : PrimePaddingObstruction)
    (s : Finset ℕ) (hcard : 3 ≤ s.card) (hpos : ∀ x ∈ s, 1 ≤ x)
    (hsum : (∑ x ∈ s, (1 : ℚ) / x) = 1) (m : ℕ) (hm : m ∈ s) :
    ∃ b u v : ℕ, b ∈ s ∧ b ≠ m ∧ 1 ≤ u ∧ 1 ≤ v ∧ u ≠ v ∧
      u ∉ s ∧ v ∉ s ∧
      (1 : ℚ) / b = 1 / u + 1 / v := by
…

Mentions: OAI.Problem337.PrimePaddingObstruction, OAI.Problem337.v

theorem OAI.Problem337.prime_padding_obstruction line 109
Source documentation
The prime obstruction follows by clearing rational denominators.
```
theorem prime_padding_obstruction : PrimePaddingObstruction := by
…
```
Mentions: OAI.Problem337.PrimePaddingObstruction

theorem OAI.Problem337.exact_marker_padding_proof line 124

Source documentation

Exact marker padding, without analytic or counting hypotheses.

theorem exact_marker_padding_proof :
    ∀ r : ℕ, 3 ≤ r → ∀ n : Fin r → ℕ, IsOneExpansion n →
    ∀ m : ℕ, (∃ i : Fin r, n i = m) →
    ∃ n' : Fin (r + 1) → ℕ,
      IsOneExpansion n' ∧ ∃ i : Fin (r + 1), n' i = m := by
…

Mentions: OAI.Problem337.IsOneExpansion