RootedAnnealing.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Adjacent selected-root weights and ideal multipliers

The actual computed-root penalty satisfies the source height bound. It gives the factor-two annealing estimates for the same literal completion count used by the executed density evaluator.

def OAI.ContingencyTables.RootedAnnealing.penalty line 27
Source documentation
The selected-root penalty of an actual integer free assignment.
```
noncomputable def penalty (A : Instance I J) (R : RootedCompletion.Selection A.T)
    (z : View A → ℕ) (f : FreeIndex A.small A.T A.b) : ℝ :=
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection
theorem OAI.ContingencyTables.RootedAnnealing.penalty_bound line 36
Source documentation
The source height bound holds for the selected, computed root too.
```
theorem penalty_bound (A : Instance I J) (R : RootedCompletion.Selection A.T)
    (z : View A → ℕ) (hz : InBox (bounds A) z)
    (f : FreeIndex A.small A.T A.b) :
    0≤ penalty A R z f ∧ penalty A R z f≤ scale A := by
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedAnnealing.penalty
def OAI.ContingencyTables.RootedAnnealing.weight line 58
theorem OAI.ContingencyTables.RootedAnnealing.count_adjacent line 61
theorem OAI.ContingencyTables.RootedAnnealing.weight_positive line 98
theorem OAI.ContingencyTables.RootedAnnealing.weight_adjacent line 103
theorem OAI.ContingencyTables.RootedAnnealing.total_adjacent line 119
theorem OAI.ContingencyTables.RootedAnnealing.ideal_adjacent line 128