bond_multipliers
plain-language theorem explainer
Assigns every bond in a foundation ledger state the constant real multiplier 1. Downstream positivity and thermodynamic cost lemmas treat this as the trivial positive scale on active bonds. The body is a pure constant definition, not a derived claim.
Claim. For every ledger state $s$ and every bond identifier $b\in\mathbb{N}$, the bond multiplier attached to $(s,b)$ equals $1\in\mathbb{R}$.
background
In Foundation.RecognitionOperator, a ledger state is an eight-channel signal (Signal8), and bond identifiers are natural numbers. Bonds are the discrete links whose scales enter recognition cost.
The multiplier is the real factor $m$ fed to the J-cost $J(m)=(m+m^{-1})/2-1$ (equivalently $\cosh(\log m)-1$). Sibling active_bonds selects which bonds are live; this definition supplies the scale on each bond, independently of the state argument in the present stub.
The information-layer Thermodynamics.LedgerState later packages the same idea as a structure field `bond_multipliers : \mathbb{N}\to\mathbb{R}$ with an explicit positivity hypothesis on active bonds.
proof idea
No proof. The declaration is a definition whose right-hand side is the constant real 1, ignoring both the ledger state and the bond id. Downstream bond_pos discharges positivity by simp [bond_multipliers].
why it matters
Gives a uniform positive scale so foundation lemmas can talk about bond cost without choosing a nontrivial spectrum. Immediate consumer: bond_pos, which records $0 < m$ for every active bond.
In Information.Thermodynamics, the same name appears as the multiplier field inside total recognition cost $\sum J(m_b)$, reciprocity skew $\sum|\log m_b|$, and the quadratic lower bound $J(m)\ge(\log m)^2/2$. The scaffold hypothesis H_ThermodynamicsVerified is exactly that inequality for every active bond.
With the constant $m=1$ one has $\log m=0$ and $J(1)=0$, so the bound holds trivially and dissipation vanishes. Nontrivial physics needs a later non-constant assignment; this unit choice only closes the positivity and type interface at the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.