jcost_born_structure
plain-language theorem explainer
Among configurations compatible with an observer's partial ledger view, the variational successor carries the maximum J-cost weight exp(-total defect). Measurement and Born-rule bridges cite this to equate the dynamics-selected state with the highest-weight outcome. The proof is a short term argument: exponential monotonicity plus the successor's defect-minimality among feasible states.
Claim. Let $c$ and $next$ be $N$-entry ledger configurations, and suppose $next$ is a variational successor of $c$. Then for every configuration $c'$ feasible relative to $c$ (compatible with the observer's partial view), the J-cost weight satisfies $\exp(-D(c')) \le \exp(-D(next))$, where $D$ denotes total defect.
background
Module F-009 (Measurement Mechanism) answers how deterministic ledger dynamics can look random to an internal observer. An observer is a subsystem: $K<N$ ledger entries. It sees only its own partial view; many full $N$-entry configurations share that view. That compatible class is the feasible set. Apparent randomness is ignorance of the complementary entries, not ontological chance. Bell-type nonlocality is already carried by the global variational update.
A configuration is an $N$-tuple of positive real ratios. Total defect is the sum of entrywise $J$-costs, with $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The J-cost weight is $\exp(-D(c))$: lower defect means higher weight, the Boltzmann analogue that later supplies Born structure. A variational successor is the minimum-defect update among feasible states.
Upstream, Configuration packages the positive entries and defect sum; the weight definition is exactly $\mathrm{exp}(-\mathrm{total,defect})$. Cost notions from the recognizer and observer layers all reduce to this same $J$.
proof idea
Introduce an arbitrary feasible $c'$. Unfold the weight to $\exp(-D(\cdot))$. The second component of the variational-successor hypothesis states that $next$ minimizes total defect on the feasible class, so $D(next)\le D(c')$. Negating both sides and applying monotonicity of the real exponential (Real.exp_le_exp_of_le) yields $\exp(-D(c'))\le\exp(-D(next))$. A short linarith closes the arithmetic from the hypothesis field. No further lemmas are required.
why it matters
This is the Born-weighting step inside F-009: variational dynamics selects minimum defect, hence maximum $\exp(-J)$ weight, among observer-compatible states. The module certificate packages five structural facts resolving the measurement problem; weight maximality is the link from dynamics to outcome likelihood. In the unified forcing chain it feeds the variational-to-measurement bridge (outcomes determined by the full state, partial views underdetermine, J-weight positive and maximized at the successor) and the canonical variational-to-Born-rule bridge.
Combined with T5 $J$-uniqueness, $J(e^{t})=\cosh t-1$ is quadratic near equilibrium ($\approx t^{2}/2$), so the weight is Gaussian in log-ratio and yields $|\psi|^{2}$-like statistics under the usual identification. The theorem itself only supplies structural maximality; the quadratic expansion and normalization sit in neighboring results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.