bond_pos
plain-language theorem explainer
Any active bond in a ledger state has strictly positive multiplier. Thermodynamics and Landauer-bound arguments cite this to justify taking logarithms and evaluating the J-cost on bond ratios. The proof is a one-line simplification: multipliers are defined as the constant 1.
Claim. For every ledger state $s$ and every bond identifier $b$ belonging to the active-bond set of $s$, the bond multiplier $m_s(b)$ satisfies $0 < m_s(b)$.
background
In this foundation module a ledger state is identified with an eight-tick signal (Signal8). Bond identifiers are natural numbers. Two companion definitions fix the bond data used here: the active-bond set of any state is the empty finite set, and every bond multiplier is the constant real value $1$.
Positivity of multipliers is the elementary precondition for writing $u = \log m$ and for evaluating the recognition cost $J(m) = (m + m^{-1})/2 - 1$ on bond ratios. Downstream, the information-theoretic ledger packages the same positivity as a structure field so that Landauer-type inequalities can quantify over active bonds without side conditions.
proof idea
One-line wrapper. Unfold bond_multipliers, which is definitionally the constant function $1$, and discharge $0 < 1$ by simp. The membership hypothesis on the active-bond set is unused because the multiplier does not depend on the bond or the state.
why it matters
Supplies the positivity side-condition required by landauer_bound_holds in Information.Thermodynamics: that theorem states that for every active bond the J-cost of its multiplier is at least half the squared log-ratio, $J(m) \ge u^2/2$ with $u = \log m$. Without $m > 0$ the logarithm and the reciprocal in $J$ are undefined in the reals.
The same obligation appears as the bond_pos field of the minimal thermodynamic ledger state. In the broader Recognition framework this is bookkeeping for the cost functional forced at T5 ($J(x) = \cosh(\log x) - 1$), not a dynamical claim about which bonds are live.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.