RootedOracleChain.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual bin chain for the computed-root forest penalty

All cut geometry is proved from the selected-root density. The only conditional inputs are the same finite-box Prékopa–Leindler inequality and finite reversible-chain Cheeger theorem used by the original chain.

def OAI.ContingencyTables.RootedOracleDensity.oracleChain line 23
lemma OAI.ContingencyTables.RootedOracleDensity.oracleChain_pi line 32
lemma OAI.ContingencyTables.RootedOracleDensity.corner_injective line 37
theorem OAI.ContingencyTables.RootedOracleDensity.oracleChain_poincare line 45
Source documentation
All geometric cut obligations are discharged for the literal forest penalty. Only finite-box PL and finite-chain Cheeger remain conditional.
```
theorem oracleChain_poincare (A : Instance I J) (R : RootedCompletion.Selection A.T) (C a : ℝ) (hC : 0 < C)
    (ha : 0 ≤ a) (haH : a ≤ height A C) (z : View A → ℕ)
    {K : ℕ} (hK : 1 ≤ K)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K)) :
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger