lower_defect_higher_weight
plain-language theorem explainer
Strictly lower total defect yields strictly higher J-cost weight on configurations of N ledger entries. Cite this when linking minimum-defect variational dynamics to Born-style outcome weights. The argument is a one-line transfer of the defect inequality through exp after unfolding the Boltzmann-like weight exp(−defect).
Claim. Let $c_1,c_2$ be configurations of $N$ positive ledger ratios. If the total defect of $c_1$ is strictly smaller than that of $c_2$, then the J-cost weight of $c_2$ is strictly smaller than that of $c_1$: $\mathrm{Def}(c_1)<\mathrm{Def}(c_2)$ implies $\exp(-\mathrm{Def}(c_2))<\exp(-\mathrm{Def}(c_1))$.
background
Module F-009 (Measurement Mechanism) explains how deterministic ledger dynamics can look random to an internal observer. An observer is a subsystem: it sees only its own entries, while the measurement outcome is fixed by the full N-entry state. Many full configurations share one partial view; ignorance of the complement is the source of apparent randomness, not Bell-local hidden variables.
A configuration is an N-tuple of positive real ratios. Pointwise defect is the J-cost $J(x)=(x+x^{-1})/2-1$ (also $\cosh(\log x)-1$). Total defect sums these over entries and is nonnegative. The J-cost weight is $\exp(-\mathrm{total\ defect})$, the module's Boltzmann analogue of a Born weight: lower defect means higher weight.
Upstream, total defect is the sum of Law-of-Existence defects on configuration entries. The weight definition is local to this module and is the object whose monotonicity is proved here.
proof idea
Unfold J-cost weight to $\exp(-\mathrm{total\ defect})$. From $\mathrm{Def}(c_1)<\mathrm{Def}(c_2)$, negation reverses the inequality: $-\mathrm{Def}(c_2)<-\mathrm{Def}(c_1)$. Apply Real.exp_lt_exp_of_lt (strict increase of $\exp$ on $\mathbb{R}$) to conclude $\exp(-\mathrm{Def}(c_2))<\exp(-\mathrm{Def}(c_1))$. No further structure of configurations or of $J$ is used.
why it matters
This is the elementary cost-to-probability comparison in the measurement mechanism: the cost ordering is exactly the weight ordering. It is consumed by the Unified Forcing Chain theorem that the variational layer supplies the canonical Born-rule weight bridge (positive weights, definitional form, log-weight identities).
In RS terms it underwrites the F-009 claim that variational successors (minimum defect) carry maximum weight among observer-compatible configurations, so the dynamics' actual outcome is the mode of the weight distribution. With $J(e^t)=\cosh t-1\approx t^2/2$ near the minimum, weights are Gaussian in log-ratio and can match $|\psi|^2$-like statistics under the module's identification. It does not close the full Born derivation; it locks the monotonic bridge those later steps quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.