ComputedCompanionInstance.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A literal companion instance from binary bounded margins

All operational data are read from the executed endpoint, flow, and maximum-forest programs. The existential endpoint witnesses are used only in the terminal-mass proof, never to define an executed output.

def OAI.ContingencyTables.ComputedCompanionInstance.baseline line 21
lemma OAI.ContingencyTables.ComputedCompanionInstance.baseline_properties line 25
def OAI.ContingencyTables.ComputedCompanionInstance.instanceData line 40
Source documentation
The package consumed by the proved factorial, terminal, and oracle lemmas. Its forest and baseline are decoded executed values.
```
noncomputable def instanceData (hEK : PublishedEdmondsKarp.EdmondsKarp1972Theorem1)
    (r : Fin m→ℕ) (c : Fin n→ℕ) (b : Fin m→Fin n→ℕ)
    (hne : ∃ X,TableTightening.Feasible r c b X) (W : ℕ) (hW : 2≤W) :
    Instance (Fin m) (Fin n) where
…
```
Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.EdmondsKarp1972Theorem1, OAI.ContingencyTables.TableTightening.Feasible
theorem OAI.ContingencyTables.ComputedCompanionInstance.original_count line 77
Source documentation
Tightening preserves the count consumed by the terminal estimator.
```
theorem original_count (hEK : PublishedEdmondsKarp.EdmondsKarp1972Theorem1)
    (r : Fin m→ℕ) (c : Fin n→ℕ) (b : Fin m→Fin n→ℕ)
    (hne : ∃ X,TableTightening.Feasible r c b X) (W : ℕ) (hW : 2≤W) :
    CompanionTerminalMass.tableCount (instanceData hEK r c b hne W hW)=
      (Fintype.card (BoundedTable r c b):ℝ) := by
…
```
Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.EdmondsKarp1972Theorem1, OAI.ContingencyTables.TableTightening.Feasible, OAI.ContingencyTables.CompanionTerminalMass.tableCount, OAI.ContingencyTables.ComputedCompanionInstance.instanceData, OAI.ContingencyTables.BoundedTable
def OAI.ContingencyTables.ComputedCompanionInstance.endpoints line 93
Source documentation
The endpoint assumption in the terminal proof follows from the executed searches. The witnesses here are mathematical proof data.
```
noncomputable def endpoints (hEK : PublishedEdmondsKarp.EdmondsKarp1972Theorem1)
    (r : Fin m→ℕ) (c : Fin n→ℕ) (b : Fin m→Fin n→ℕ)
    (hne : ∃ X,TableTightening.Feasible r c b X) (W : ℕ) (hW : 2≤W) :
    CompanionTerminalMass.Endpoints (instanceData hEK r c b hne W hW) := by
…
```
Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.EdmondsKarp1972Theorem1, OAI.ContingencyTables.TableTightening.Feasible, OAI.ContingencyTables.CompanionTerminalMass.Endpoints, OAI.ContingencyTables.ComputedCompanionInstance.instanceData