[Autoplectic]

Summary

lifted_heaviest_term_bound(problem, ...) gives a certified lower bound on the state entropy of every lifted generator (consecutive states drawn independently from one channel given the bidirectional edge). Until now sofic had only upper bounds for lifted generators, so "the minimal generator is not lifted" could not be shown.

A lifted generator's states form an exact decomposition, and its heaviest state e has channel c_e(a, b) = t q_a r_b / p(a, b) at both ends of every edge. Coarse-graining the other end to [W = e] cannot raise the lifting conditions' conditional mutual informations, so for every symbol x:

• L_B(a, x) = sum_b r_b / p(a, b) * sum_{pair1} E[(a, b), x, pair1] u(pair1) is constant over a in supp q,
• L_A(b', x), its mirror, is constant over b' in supp r,

with u(a, b) = q_a r_b / p(a, b) and E the joint edge law (t cancels). The coefficients are nonnegative, so a box's corners bound both, and a box is pruned when two surely supported states have disjoint intervals. This is a weight_cap for heaviest_term_bound (#60). The root's weight floor stays valid because the forward ε-machine is lifted.

Results

• Dataset process ((0,1),(0,2),(0,2)) (3 × 3 joint): every lifted generator has entropy >= 1.48148 (120 s), and a lifted generator at 1.48166 exists, while C_g = G = 1.42254 (certified; the minimal generator comes from an exact-common-information optimum, with lifting residual 0.026 bits). The bound passes G in under 5 s.
• Soundness sweep over 218 dataset processes (15 s each): the bound never exceeds the best lifted generator by more than the lifted search's own tolerance (minimal_generative_model accepts near-feasible channels, so its entropies can undercut by ~6e-5). Where the lifted model is minimal the bound usually meets it to 5 decimals.
• Interleaved at eps = 9/20 (4 × 4): 0.762 after 300 s, below the proved lifted minimum 1 + h(1/11) = 1.4395 (valid, but slow on 4 × 4 joints).

Test plan

• The ε-machine's states pass the lifted term test (violation < 1e-12)
• On ((0,1),(0,2),(0,2)) the lifted bound reaches 1.43 while the static bound stays at G <= 1.42255
• tests/test_exact_ci_bounds.py: 9 passed; ruff, ty, sphinx-build -W

Made with Cursor