Variational_To_BornRule_Canonical_Bridge
plain-language theorem explainer
Packages the claim that the configuration weight w(c)=exp(−total defect) is the canonical Born measure on ledger configurations. It records positivity, the log-link log w=−defect, strict antitonicity in defect, maximality at variational successors, unit normalization at zero defect, and uniqueness among positive functions with the same log-defect identity. Measurement-layer and CompleteForcingChain arguments cite this certificate. As a Prop structure it is definitional; the companion theorem discharges every field from the variational layer.
Claim. A certificate that the Born-rule weight $w(c)=\exp(-\Delta(c))$ on configurations $c$ of size $N$ is strictly positive, satisfies $\log w(c)=-\Delta(c)$, is strictly antitone in total defect $\Delta$, is maximized at every variational successor on the feasible set, equals $1$ whenever $\Delta(c)=0$, and is the unique strictly positive real function on configurations whose logarithm equals $-\Delta$.
background
The Unified Forcing Chain module aims to show T−1 through T8 as inevitabilities from the cost foundation (Recognition Composition Law, normalization, calibration), not merely as compatible layers. Inside that chain, the variational and measurement layers sit above the ledger: configurations carry a total defect built from the J-cost, and dynamics select successors that minimize that defect on a feasible set.
The J-cost weight used here is the exponential of minus total defect. That is the standard Boltzmann/Born link: lower recognition cost means higher weight. Upstream measure-forcing work already isolates a continuous weight with factorization, antitonicity, and self-similar dressing (the canonical self-similar dressing), so the same exponential shape is not ad hoc when it reappears on discrete configurations.
This structure does not re-derive the weight. It names the interface a later theorem must satisfy: positivity, the defining equation, the log-link, strict antitonicity, Born maximality at variational successors, normalization at zero defect, and a universal-property uniqueness clause.
proof idea
No proof body: this is a Prop-valued structure (a certificate type). Each field is a named hypothesis about the measurement weight relative to total defect and variational succession.
The companion theorem variational_to_bornrule_canonical_bridge_holds builds an inhabitant under a forced variational layer. Positivity is handed off to the measurement lemma that the weight is positive; the defining equation is definitional (rfl); the log identity, antitonicity, maximality, zero-defect normalization, and uniqueness are discharged from the same exponential definition plus standard real-analysis facts (log/exp inverse, strict decrease of exp(−·), uniqueness of positive reals with a fixed logarithm). The structure itself only packages those obligations.
why it matters
In Recognition Science the Born rule is not an extra quantum postulate: it is the probability reading of the J-cost on configurations. This bridge is the named interface between the variational dynamics (successors minimize defect on the feasible set) and the measurement weight w=exp(−Δ).
Downstream, CompleteForcingChain requires the variational and measurement layers inside the main inevitability bundle (T−1 through T8 plus quarter-turn, Hamiltonian, projective, coupled-core, variational, and measurement). The companion theorem variational_to_bornrule_canonical_bridge_holds is the discharge point that feeds that complete chain.
The uniqueness field is the important conceptual load: any strictly positive weight whose log equals −total defect must coincide with the J-cost weight. That is the universal property of the canonical Born measure in RS-native units, tying measurement back to the same cost foundation that forces T5 (unique J) and the later ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.