ratioConfig_entry
plain-language theorem explainer
For any positive real ratio packaged as a one-channel configuration, every entry equals that ratio. Anyone simplifying ground-state or zero-charge equilibrium arguments on a single ratio observable will cite this. The proof is pure definitional equality (rfl) from the constant-entry constructor.
Claim. Let $r > 0$ be a real number and let $C_r$ be the one-channel configuration whose single entry is constantly $r$. Then for the unique index $i \in \{0\}$, the $i$-th entry of $C_r$ equals $r$.
background
The module extracts a B4-style dynamic claim from the variational ledger update rule: equilibria coincide with variational minimizers; in a zero-charge sector the unique equilibrium is the unity configuration; and for a one-channel ratio observable, stability therefore forces the ratio to equal one.
A Configuration n is a finite tuple of strictly positive reals (the ledger channel values). The helper ratioConfig r hr packages a single positive real $r$ as a Configuration 1 by setting every entry (there is only one) to $r$ and recording positivity from hr. This is the canonical one-channel ratio observable used later when stability is specialized to a single ratio.
proof idea
One-line definitional proof. The constructor of ratioConfig sets entries := fun _ => r, so projecting .entries i is definitionally $r$. The tactic is rfl; the lemma is marked @[simp] so downstream rewrites unfold the packaging automatically.
why it matters
This is the projection simp lemma for the one-channel ratio packaging that the ground-state story rests on. The module's target is that stability in a zero-charge sector forces the ratio observable to equal one (stable_zero_charge_ratio_eq_one and related siblings). Without a clean entry projection, those arguments would repeatedly unfold the configuration constructor by hand. No downstream edges are recorded yet; the lemma is local scaffolding for the zero-charge unity and stable-ratio claims in the same file. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it only prepares the observable those dynamics act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.