t5_t3_to_variational_bridge_holds
plain-language theorem explainer
Given unique J-cost (T5) and a forced ledger (T3), the analytic surface supplies canonical variational dynamics: total defect is nonnegative, feasible moves conserve log-charge, and the successor is the global defect minimizer on that set. Forcing-chain authors cite this as the T5+T3 bridge into variational evolution. The proof assembles preexisting nonnegativity, feasibility, and VariationalDynamics lemmas into the bridge certificate.
Claim. Assume the Recognition Composition Law with reciprocity, normalization, and calibration forces $J(x)=\frac12(x+1/x)-1$ on $(0,\infty)$, and that the ledger is forced as additive recognition bookkeeping. Then the T5/T3 variational bridge holds: for every positive-ratio configuration $c$, the total defect satisfies $\mathrm{total\_defect}(c)\ge 0$; a successor is feasible iff it preserves total log-charge; a variational successor exists, strictly reduces defect when not at unity, is a global update, and realizes the variational layer.
background
The Unified Forcing Chain module aims to show T-1 through T8 as inevitabilities from the cost foundation (Recognition Composition Law plus normalization and calibration), not merely compatible choices. T5 packages uniqueness of the analytic cost: reciprocity, normalization $J(1)=0$, the composition law, calibration, and continuity force $J(x)=\frac12(x+1/x)-1$, equivalently $J_{\log}(t)=\cosh t-1$ in log coordinates. T3 packages the ledger as forced additive bookkeeping of recognition work (empty entry neutral, independent joins add costs).
Once that $J$ surface is in hand, configurations carry a total defect built from $J$ on entry ratios. The conserved ledger quantity is total log-charge; the feasible set is exactly the charge-preserving slice. Variational dynamics then mean: the next configuration is the global argmin of total defect on that feasible set. Strict convexity of $J_{\log}$ makes the minimizer unique up to entry equality, so the trajectory is deterministic.
The bridge structure records nonnegativity of defect, the feasibility/charge equivalence, existence and defect-reduction of the successor, unity as equilibrium, globality of the update, and that the variational layer holds.
proof idea
Structure construction, not a deep new argument. Nonnegativity of total defect is discharged by InitialCondition.total_defect_nonneg. Feasibility iff log-charge conservation is definitional and closed by rfl. Existence of a successor, defect reduction along a variational step, unity as equilibrium, and globality of the update are wired directly to the corresponding VariationalDynamics lemmas (variational_step_exists, variational_step_reduces_defect, unity_is_equilibrium, update_is_global). The final field cites variational_layer_holds. The T5 and T3 hypotheses are present as the bridge's logical premises but are not reopened inside the body; the proof only assembles the already-proved variational surface under those assumptions.
why it matters
In the forcing chain, T5 pins the unique cost $J$ and T3 forces the ledger; without a bridge, those remain static structure. This certificate turns them into dynamics: evolution is the canonical argmin of total defect on the charge-conserving set, not an extra postulate. Downstream, complete_forcing_chain consumes the bridge while assembling the unconditional CompleteForcingChain from T-1 through T8.
Framework landmarks: T5 is the J-uniqueness step ($J(x)=\cosh(\log x)-1$); T3 is ledger forcing from cost symmetry $J(x)=J(1/x)$. The variational reading is what later steps need when discrete self-similarity forces $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8). The module's stronger claim is complete inevitability from RCL plus normalization and calibration; this bridge is the hinge from unique cost plus ledger to deterministic defect-minimizing flow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.