TerminalBridge.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.Descent.UnitListAtMost.of_list line 11
Source documentation
Convert an ordinary positive list to the finite-tuple interface used by backward propagation, without changing its length or reciprocal sum.
```
theorem UnitListAtMost.of_list {x : ℚ} {B : ℕ} (l : List ℕ)
    (hlen : l.length ≤ B) (hpos : ∀ n ∈ l, 0 < n)
    (hsum : (l.map (fun n : ℕ => (1 : ℚ) / (n : ℚ))).sum = x) :
    UnitListAtMost x B := by
…
```
Mentions: OAI.Problem337.Descent.UnitListAtMost

theorem OAI.Problem337.Descent.UnitListAtMost.of_list_real line 25

Source documentation

A real-valued length budget can be rounded once at the terminal stage.

theorem UnitListAtMost.of_list_real {x : ℚ} {L : ℝ} (l : List ℕ)
    (hlen : (l.length : ℝ) ≤ L) (hpos : ∀ n ∈ l, 0 < n)
    (hsum : (l.map (fun n : ℕ => (1 : ℚ) / (n : ℚ))).sum = x) :
    UnitListAtMost x ⌈L⌉₊ := by
…

Mentions: OAI.Problem337.Descent.UnitListAtMost

theorem OAI.Problem337.Descent.UnitListAtMost.to_list line 34
Source documentation
Convert the propagated finite tuple back to the list interface in the dense-family proposition.
```
theorem UnitListAtMost.to_list {x : ℚ} {B : ℕ} (H : UnitListAtMost x B) :
    ∃ l : List ℕ, l.length ≤ B ∧ (∀ n ∈ l, 0 < n) ∧
      (l.map (fun n : ℕ => (1 : ℚ) / (n : ℚ))).sum = x := by
…
```
Mentions: OAI.Problem337.Descent.UnitListAtMost

theorem OAI.Problem337.Descent.UnitListAtMost.to_list_two line 45

Source documentation

Below one the output additionally meets the required denominator-two bound.

theorem UnitListAtMost.to_list_two {x : ℚ} {B : ℕ} (H : UnitListAtMost x B)
    (hx : x < 1) :
    ∃ l : List ℕ, l.length ≤ B ∧ (∀ n ∈ l, 2 ≤ n) ∧
      (l.map (fun n : ℕ => (1 : ℚ) / (n : ℚ))).sum = x := by
…

Mentions: OAI.Problem337.Descent.UnitListAtMost