Construction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The unconditional construction with the prime chosen last

The only inputs are the proposed scale, a positive rank, and a positive entropy budget. The prime, robust directions, contraction partitions, separated real matrix, positive and signed approximation lists, and actual convex body are all constructed by the preceding theorems.

theorem OAI.MetricEntropyDuality.exists_entropy_pair_with_budget line 23
Source documentation
Construct actual full-dimensional bodies and their strict entropy bound. There is no matrix, compression, geometric, or entropy premise.
```
theorem exists_entropy_pair_with_budget (a : ℝ) (ha : 1 ≤ a)
    (r : ℕ) (hr : 1 ≤ r) (B : ℝ) (hB : 0 < B) :
    Nonempty (EntropyPair a r B) := by
…
```
Mentions: OAI.MetricEntropyDuality.EntropyPair