landauer_bound_holds
plain-language theorem explainer
The declaration proves that for any ledger state the J-cost of each active bond multiplier m satisfies Jcost(m) ≥ (log m)^2 / 2. Information theorists and physicists deriving thermodynamic limits from recognition costs cite it when establishing global dissipation inequalities. The tactic proof substitutes the exponential form of m, invokes the identity Jcost(exp u) = cosh u - 1, applies the quadratic lower bound on cosh, and closes with linarith.
Claim. For a ledger state $s$ and every active bond $b$, letting $m$ be the corresponding bond multiplier, the recognition cost obeys $J(m) ≥ (ln m)^2 / 2$, where $J$ is the J-cost function.
background
LedgerState is the minimal structure holding a Finset of active bonds, a map from bonds to positive real multipliers, and the positivity witness for each multiplier. The J-cost is the function J(x) = cosh(log x) - 1 induced by the Recognition Composition Law and the multiplicative recognizer. The module sits in Phase 7.5.2, which formalizes the link between recognition cost and thermodynamic entropy by anchoring the theory at the Landauer limit.
proof idea
The tactic proof obtains positivity of m from the ledger state, sets u = log m, rewrites m as exp u, applies the lemma Jcost_exp_cosh to replace Jcost m by cosh u - 1, invokes the upstream theorem cosh_quadratic_lower_bound to obtain cosh u ≥ 1 + u²/2, and finishes with linarith.
why it matters
The per-bond inequality supplies the local estimate required by the downstream total_dissipation_bound theorem, which asserts that total recognition cost is bounded below by half the sum of squared log-multipliers. It places the information-theoretic side of Recognition Science inside the Landauer principle while remaining consistent with the eight-tick octave and the cost derived from the multiplicative recognizer. No open scaffolding is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.