variational_to_bornrule_canonical_bridge_holds
plain-language theorem explainer
Given that variational ledger dynamics is forced, the configuration weight w(c)=exp(-D(c)) (D = total defect) is the unique canonical Born-rule measure: positive, log-linear in defect, strictly antitone, maximized on variational successors, and unit at zero defect. Measurement and probability steps in the forcing chain cite this bridge. The proof fills each certificate field by unfolding the exponential weight and applying the measurement-mechanism lemmas.
Claim. If the variational ledger layer is forced (every configuration has a variational successor of nonincreasing total defect, and the unity configuration is an equilibrium), then the canonical Born-rule bridge holds: the weight $w(c)=\exp(-D(c))$ is strictly positive, satisfies $\log w(c)=-D(c)$ by definition, is strictly antitone in defect, is maximized at variational successors, equals $1$ at zero defect, and is the unique strictly positive function sharing the same log-defect identity.
background
The Unified Forcing Chain module shows T0–T8 as inevitabilities from the Recognition Composition Law (with normalization and calibration). Between ledger/variational dynamics and measurement sits a bridge that identifies Born weights with the exponential of total defect.
The variational-layer certificate states that for every positive $N$ and configuration $c$, a variational successor exists, total defect never increases along successors, and the unity configuration is an equilibrium. The measurement mechanism defines the J-cost weight $w(c)=\exp(-D(c))$, with $D(c)$ the total defect of $c$.
The target bridge structure packages the standard Born-rule properties of this weight: positivity, the defining log identity, strict antitonicity in defect, maximality on successors, unit value at vanishing defect, and uniqueness among positive log-defect functions.
proof idea
Structure constructor, field by field. Positivity is the measurement lemma that the J-cost weight is positive. The definitional equation is reflexivity after the weight is fixed as $\exp(-D)$. The log identity is Real.log_exp after unfolding. Strict antitonicity is the lower-defect-higher-weight lemma. Maximality at successors is the J-cost Born-structure lemma. Zero-defect unit value rewrites $D=0$ and simplifies the exponential to $1$. Uniqueness: any strictly positive $w'$ with $\log w'=-D$ has the same log as $w$, so Real.log_injOn_pos forces $w'=w$ pointwise.
why it matters
Consumed by the top-level complete_forcing_chain package, which assembles the unconditional inevitability chain. The bridge turns cost/defect minimization into a probability calculus: lower-defect configurations receive exponentially higher weight, so Born structure is not an extra postulate once the variational layer is forced.
In the module's stronger claim (complete inevitability from the cost foundation, not mere compatibility), this is the named intermediate certificate from variational dynamics to measurement. It sits alongside the spine-to-extras bridges (Gödel dissolution from T0, unique existent from T5 analytic refinement, constants from T6) that the chain later packages. Framework landmarks nearby: T5 J-uniqueness underpins defect-as-J-cost; the RCL cost foundation is the single axiom bundle driving the whole chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.