RootedPhysicalCompletion.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Literal residual completion for the executed root convention

The row and column small views remain distinct. The explicit selected roots determine which incidence equations are enforced; the resulting integral completion is exactly the selected-cut affine formula.

def OAI.ContingencyTables.RootedPhysicalCompletion.solved line 21
def OAI.ContingencyTables.RootedPhysicalCompletion.completed line 26
lemma OAI.ContingencyTables.RootedPhysicalCompletion.solved_supported line 30
lemma OAI.ContingencyTables.RootedPhysicalCompletion.row_pointwise line 34
lemma OAI.ContingencyTables.RootedPhysicalCompletion.column_pointwise line 43
lemma OAI.ContingencyTables.RootedPhysicalCompletion.row_completed_sum line 52
lemma OAI.ContingencyTables.RootedPhysicalCompletion.column_completed_sum line 62
theorem OAI.ContingencyTables.RootedPhysicalCompletion.solved_eq_affine line 74
Source documentation
The cut-defined coefficients evaluate the actual integral solution for this root convention, including every unbalanced small profile.
```
theorem solved_eq_affine (A : Instance I J) (S : Selection A.T) (t : TreeCell A.T)
    (x q free : I → J → ℤ) :
    (solved A S x q free t.val.1 t.val.2:ℝ)=
      affineTree A S t (fun i j => (x i j:ℝ)) (fun i j => (q i j:ℝ))
        (fun a => (free a.1 a.2:ℝ)) := by
…
```
Mentions: OAI.ContingencyTables.RootedPhysicalCompletion.solved