Conditional potentials for transition encodings

The states at depth t are prefixes of an encoding, not successive graph cuts. Their masses are obtained from the actual joint distribution of a transition. A potential satisfying the displayed local inequalities bounds the final square-root moment by telescoping. This allows dependencies and history-dependent charges; replacing the conditional distributions by independent signal marginals is not valid.

This is a certificate interface. A universal circuit bound on its initial potential remains a separate requirement.

noncomputable def Complexity.Frontier.Communication.rootPotential {State : ℕ → Type u_1} [(t : ℕ) → Fintype (State t)] (mass potential : (t : ℕ) → State t → ℝ) (t : ℕ) : ℝ

Sum of square-root masses weighted by a prefix potential.

Equations

• Complexity.Frontier.Communication.rootPotential mass potential t = ∑ u : State t, √(mass t u) * potential t u

theorem Complexity.Frontier.Communication.rootPotential_step {State : ℕ → Type u_1} [(t : ℕ) → Fintype (State t)] (mass potential : (t : ℕ) → State t → ℝ) (parent : (t : ℕ) → State (t + 1) → State t) (t : ℕ) (h : ∀ (u : State t), ∑ v : State (t + 1) with parent t v = u, √(mass (t + 1) v) * potential (t + 1) v ≤ √(mass t u) * potential t u) : rootPotential mass potential (t + 1) ≤ rootPotential mass potential t

A local conditional certificate can charge one prefix by all its refinements.

theorem Complexity.Frontier.Communication.rootPotential_le {State : ℕ → Type u_1} [(t : ℕ) → Fintype (State t)] (mass potential : (t : ℕ) → State t → ℝ) (parent : (t : ℕ) → State (t + 1) → State t) (T : ℕ) (h : ∀ t < T, ∀ (u : State t), ∑ v : State (t + 1) with parent t v = u, √(mass (t + 1) v) * potential (t + 1) v ≤ √(mass t u) * potential t u) : rootPotential mass potential T ≤ rootPotential mass potential 0

Local conditional certificates amortize over the whole encoding. With leaf potential one and a single unit-mass root, this bounds the sum of square roots of codeword masses by the root potential.