ratioConfig
plain-language theorem explainer
Packages any positive real ratio as a one-channel ledger configuration (N=1). Cited wherever ground-state stability is reduced to a single observable ratio, and by the φ-power mass bridge. Pure structure construction: constant Fin-1 map with the given positivity witness.
Claim. For $r > 0$, write $\mathrm{Config}_1(r)$ for the one-channel configuration whose unique ledger entry equals $r$.
background
A configuration of $N$ ledger entries is a map $\mathrm{Fin},N\to\mathbb{R}_{>0}$: each slot holds a positive real ratio. Total defect is the sum of individual $J$-costs on those entries. The module studies ground states of the variational ledger update: equilibria coincide with variational minimizers, and in a zero-charge sector the unique equilibrium is the unity configuration.
Here $N=1$, so the configuration is just a single positive ratio. The one-channel case is the minimal setting in which a ratio observable can be tested for stability under the neutral-sector dynamics. Upstream, the same Configuration structure appears in the initial-condition and recognition-forcing layers as the carrier of ledger data.
proof idea
Definitional construction, not a proof. The structure field entries is the constant function on Fin 1 with value $r$; the positivity field is discharged by the hypothesis $r>0$ at every index.
why it matters
Local glue for the B4-style dynamic claim in this module: stable one-channel ratios in the neutral sector are forced to unity. Downstream simp lemmas read the entry and the log-charge as $r$ and $\log r$; the stability theorem then concludes $r=1$ from equilibrium plus vanishing log-charge.
Outside the module, the mass/generation torsion bridge builds $\varphi$-power one-channel configurations by feeding $\varphi^n$ into this constructor. That ties the ground-state unity force to the $\varphi$-ladder used for mass rungs, connecting variational neutrality to the RS mass formula setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.