VariationalLayer_Forced
plain-language theorem explainer
The variational layer packages the ledger equation of motion: every positive-size configuration admits a log-charge-preserving defect minimizer as successor, defect never rises along successors, the all-ones state is equilibrium, and total defect is nonnegative. Globality adds that some successor is not realized by a merely local update. Cite it when wiring T5/T3 into dynamics, Born-rule weights, measurement, or the Complete Forcing Chain. It is a bare Prop structure; inhabitation is discharged by a one-line certificate theorem.
Claim. A variational dynamics layer holds on ledger configurations of size $N>0$: for every configuration $c$, (i) there exists a variational successor (a feasible, log-charge-preserving state of minimal total $J$-defect), (ii) every such successor $c'$ satisfies $\mathrm{total\_defect}(c')\le\mathrm{total\_defect}(c)$, (iii) the unity configuration (all entries equal to $1$) is an equilibrium, and (iv) $\mathrm{total\_defect}\ge 0$ on every configuration. Moreover the dynamics is global: there exist $N$, $c$, and a successor $c'$ with no local-update witness.
background
In the Unified Forcing Chain, T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. After T5 pins the unique analytic cost $J(x)=(x+x^{-1})/2-1$ and T3 supplies ledger symmetry $J(x)=J(1/x)$, configurations carry a nonnegative total defect and a conserved log-charge.
A configuration of size $N$ is an $N$-tuple of positive real ratios. Its total defect is the sum of individual $J$-costs (defects). The unity configuration sets every entry to $1$ and has zero total defect. A variational successor of $c$ is any feasible (log-charge-preserving) state that minimizes total defect on the feasible set; this is the ledger equation of motion. Equilibrium means a configuration is its own variational successor. A local update is a restricted, entrywise change; globality asserts that the true successor is not always of that form.
Upstream, IsVariationalSuccessor is defined as membership in the feasible set plus universal defect minimality, and IsEquilibrium is self-successorship. The module records that this layer needs no extra axioms beyond the cost foundation.
proof idea
This declaration is a Prop-valued structure, not a proved theorem: it bundles two fields, certificate and globality, with empty body. Inhabitation is supplied downstream by variational_layer_holds, a one-line constructor that fills certificate from VariationalDynamics.variational_dynamics_certificate (existence of successors, defect monotonicity, unity equilibrium, and nonnegativity of total defect) and globality from VariationalDynamics.update_is_global (a witness that some successor is not a local update).
why it matters
This interface is the variational slot inside CompleteForcingChain, which claims all of T0–T8 plus quarter-turn, Hamiltonian, projective, coupled-core, variational, and measurement layers. It is the hypothesis of the T5/T3→variational bridges: once T5 supplies unique $J$ and T3 supplies ledger conservation, configurations inherit nonnegative total defect, feasible successors preserve log-charge, and the update is the global argmin of defect.
Downstream, variational_to_bornrule_canonical_bridge_holds and variational_to_measurement_bridge_holds take an inhabitant of this layer to install Born-rule $J$-cost weights and the measurement mechanism. In the forcing ladder it sits after T5 (unique $J$) and T3 (ledger), before measurement and Born-rule closure. No open scaffold remains here: the layer is formalized without extra axioms, and the inhabiting theorem is already proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.