[Autoplectic]

Summary

New module sofic.generators.exact_ci_bounds with heaviest_term_bound, a certified lower bound on (\operatorname{G}[X : Y]) obtained by branching on the heaviest term of the decomposition.

• The identity. Any exact decomposition with heaviest term (T = t,q r^\top) has entropy (h(t) + (1 - t),H(\text{rest})), where the rest decomposes ((P - T)/(1 - t)) with every atom at most (t/(1-t)).
• The box bound. Over a box of ((q, r, t)), the remainder lies entrywise below (P - t_{lo},q_{lo} r_{lo}^\top). The rest's top weights are therefore capped by mu1_vertex and the spectral caps of that envelope. capped_coverage_entropy turns those caps and the atom cap into an entropy lower bound, taking the least concave majorant of the caps first; plain greedy partial sums are not valid. The objective is concave in (t), so each box is evaluated at its two endpoints.
• Cardinality. Kumar, Li & El Gamal's cardinality bound (at most (2^{\min} - 1) terms) gives (t \ge 1/(2^{\min} - 1)) (cited in the docstring and the docs).
• Pipeline hook. generative_model runs it after the exact stage, with 15% of the remaining budget, when the certified lower is still below the exact-common-information estimate and (|S^+| + |S^-| \le 7). It aims within half the certification tolerance of the best upper, so a bracket that closes is reported as certified.

Results

On the three survey joints whose lower bound was below the exact-common-information estimate (all 3 × 3):

case	v11 bracket	standalone bound (1e-5 of the estimate)	pipeline
((0,1),(2,·),(0,1))	[0.9118, 0.9335]	0.9335 (67k nodes, 59 s)	[0.9335075, 0.9335082], certified
((0,1),(2,1),(0,·))	[0.4436, 0.5120]	0.4717 (24k nodes, 20 s)	[0.4717, 0.5120]
((0,1),(0,2),(0,1))	[0.9056, 0.9702]	0.9243 (1.5M nodes, 25 min)	[0.9151, 0.9702] (stage share ran out)

This takes the 3-state benchmark from 18 to 19 certified.

Test plan

• tests/test_exact_ci_bounds.py:
  • the capped coverage is valid where the greedy is not;
  • DSBS(9/20) reaches (h(1/11));
  • hypothesis check that the bound is at most every exact decomposition found;
  • the bound converges on the survey joint.
• Generator suites (111 passed)
• ruff check, ruff format --check, ty check (no errors), sphinx-build -W

Made with Cursor