RootedComponentSemantics.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The executed component sums equal the root penalty

The root-only filter in the manuscript costs no separate test: every nonroot has an empty root fibre. This connects the polynomial grouped signed-sum program to the actual selected-root discrepancy.

lemma OAI.ContingencyTables.RootedComponentProgram.componentTotal_zero line 20
theorem OAI.ContingencyTables.RootedComponentProgram.rootCount_eq_componentTotals line 35
theorem OAI.ContingencyTables.RootedComponentProgram.total_records_rootCount line 53
Source documentation
The positive and negative entries may be the actual row and column small-view sums. Their difference is the only representation invariant needed by the finite signed component program.
```
theorem total_records_rootCount (A : Instance I J) (S : Selection A.T)
    (x q : I → J → ℤ) {n : ℕ} (e : Fin n ≃ I⊕J) (p m : Fin n → ℕ)
    (hd : ∀ i,(p i:ℤ)-m i=ForestRootPenalty.smallDemand A.small A.X x q (e i)) :
    total (records (fun i => e.symm (S.root (e i))) p m)=
      RootedPenaltyProgram.rootCount A S x q := by
…
```
Mentions: OAI.ContingencyTables.ForestRootPenalty.smallDemand, OAI.ContingencyTables.RootedComponentProgram.total, OAI.ContingencyTables.RootedComponentProgram.records, OAI.ContingencyTables.RootedPenaltyProgram.rootCount
def OAI.ContingencyTables.RootedComponentProgram.positiveDemand line 86
def OAI.ContingencyTables.RootedComponentProgram.negativeDemand line 91
theorem OAI.ContingencyTables.RootedComponentProgram.naturalDemand_eq line 96