eq_constant_config_of_defect_eq
plain-language theorem explainer
If a configuration of length N achieves equality between its total defect and N times Jlog of the mean log-charge, then every entry equals the same constant value. Researchers proving uniqueness of the variational update step cite this result. The argument rewrites the defect equality as equality in the weighted Jensen sum for Jlog, invokes the strict-convexity characterization to force all logarithms identical, and recovers the constant configuration by exponentiation.
Claim. Let $c$ be a configuration of length $N>0$. If its total defect equals $N$ times $Jlog$ of the average log-charge, then every entry of $c$ equals the constant value whose logarithm is that average.
background
The VariationalDynamics module supplies the missing update rule for the Recognition ledger: each step is the global argmin of total defect over configurations that preserve the total log-ratio (charge). Jlog is the log-domain cost Jcost composed with exp; its strict convexity on the reals is recorded in Jlog_strictConvexOn. The upstream theorem states that Jlog equals cosh minus one and inherits strict convexity from the hyperbolic cosine. This convexity supplies the equality case of Jensen's inequality that the present lemma isolates.
proof idea
The proof normalizes the given defect equality to obtain Jlog of the weighted average of the logs equal to the weighted average of the Jlogs. It applies the map_sum_eq_iff direction of Jlog_strictConvexOn with uniform weights 1/N. Strict convexity forces every log-entry to equal the common average. Exponentiation then yields the constant configuration whose value is exp of that average.
why it matters
The lemma supplies the equality case required by the downstream theorem variational_step_unique, which asserts that any two variational successors of a given state coincide. It therefore completes the uniqueness half of the constrained global minimization principle for ledger evolution. The argument rests on the strict convexity of J established in the Determinism module and on the T5 J-uniqueness landmark of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.