jcost_weight_pos
plain-language theorem explainer
Every configuration of N ledger entries carries a strictly positive J-cost weight exp(−total defect). Anyone building Born-rule or Boltzmann-style statistics from the measurement mechanism cites this. The proof is a one-line application of positivity of the real exponential.
Claim. For every $N\in\mathbb{N}$ and every configuration $c$ of $N$ positive ledger ratios, the J-cost weight $w(c)=\exp(-D(c))$ is strictly positive, where $D(c)$ is the total defect (sum of individual $J$-costs of the entries).
background
Module F-009 formalizes measurement in Recognition Science: observers are subsystems of the ledger, outcomes are deterministic functions of the full configuration, and apparent randomness is ignorance of the complementary entries. The Born-rule side of that story needs a positive weight on configurations.
A Configuration N is an $N$-tuple of positive real ratios. The defect of a single ratio is $J(x)=(x+x^{-1})/2-1$ (the unique cost forced by the Recognition Composition Law). Total defect $D(c)$ sums $J$ over the entries. The J-cost weight is then defined as $w(c)=\exp(-D(c))$, the direct analogue of a Boltzmann factor and of $|\psi|^2$ weighting.
Upstream, jcost_weight is exactly that exponential; related cost defs in ObserverForcing and MultiplicativeRecognizerL4 identify recognition cost with $J$. Positivity of $w$ is the elementary analytic fact needed before any normalization or comparison of weights.
proof idea
Term-mode one-liner. Unfolding the definition, $w(c)=\exp(-D(c))$. Mathlib's Real.exp_pos states $\exp(t)>0$ for every real $t$, so the goal is immediate on the (implicit) argument $-D(c)$. No configuration hypotheses beyond the type are used.
why it matters
This is the positivity half of the J-cost weight package that turns the variational defect landscape into a probability landscape ("lower defect ↔ higher weight"). Downstream it is wired into measurement_mechanism_certificate (F-009 certificate) and into the UnifiedForcingChain bridges: Variational_To_Measurement_Bridge and variational_to_measurement_bridge_holds list positivity of $\exp(-D)$ among the structural facts that convert the variational layer into measurement dynamics; variational_to_bornrule_canonical_bridge_holds cites it explicitly as jcost_weight_positive.
In the forcing chain this sits after variational dynamics and before Born-rule statistics: once $J$ is unique (T5) and the ledger evolves by defect descent, the exponential weight is the canonical positive measure. Without strict positivity one cannot normalize to a probability or claim a unique maximizing configuration at zero defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.