jcost_weight
plain-language theorem explainer
The J-cost weight of an N-entry ledger configuration is exp(−total defect). It is the Boltzmann-style factor that turns the defect landscape into a probability landscape for measurement outcomes. Anyone citing Born-rule structure or the measurement-layer certificate uses this weight. The body is a one-line exponential of the negated total defect.
Claim. For a configuration $c$ of $N$ positive ledger ratios, the J-cost weight is $w(c) := \exp(-D(c))$, where $D(c) = \sum_{i=1}^{N} J(c_i)$ is the total defect (sum of individual J-costs of the entries).
background
Module F-009 (Measurement Mechanism) explains how deterministic ledger dynamics look random to an internal observer. An observer is a subsystem of $K < N$ ledger entries and sees only a partial view; many full configurations are compatible with that view. Apparent randomness is ignorance of the complementary entries, not external stochastic collapse.
A configuration is an $N$-tuple of positive real ratios. Each entry carries a J-cost (defect) from the Law of Existence; the total defect $D(c)$ is the sum of those costs and is nonnegative. The unique cost functional forced upstream is $J(x) = (x + x^{-1})/2 - 1$.
This definition converts that cost into a positive weight, the direct analogue of a Boltzmann factor $e^{-E/kT}$ and of the $|\psi|^2$ weighting in quantum measurement statistics.
proof idea
Pure definition: unfold to $\mathrm{Real.exp}(-\mathrm{total_defect}, c)$. No lemmas. Downstream positivity is immediate from $\exp > 0$; the monotone link lower defect $\leftrightarrow$ higher weight is $\exp$ strictly decreasing in the negated argument.
why it matters
This weight is the bridge from variational cost minimization to Born-like outcome statistics. jcost_born_structure proves that among configurations feasible for the observer's partial view, the variational successor maximizes the weight (minimizes defect), so outcome probability is proportional to total weight of full states yielding that outcome.
It feeds jcost_weight_pos, lower_defect_higher_weight, and the F-009 measurement_mechanism_certificate. In the unified forcing chain it appears in MeasurementLayer_Forced, CompleteForcingChain, and the variational-to-Born canonical bridge. Landmark link: T5 J-uniqueness supplies the cost whose exponential yields the measurement weights; the module's Born-rule structure clause is exactly this weighting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.