uniform_sum_one
plain-language theorem explainer
For any positive integer n, the sum of the constant 1/n over the n elements of Fin n equals 1. Anyone building a normalized discrete input distribution for channel capacity cites this. The proof is elementary Finset arithmetic: constant sum, card of Fin, then field simplification after ruling out n = 0.
Claim. For every natural number $n > 0$, $\sum_{i \in \mathrm{Fin}\, n} \frac{1}{n} = 1$ as a real equality.
background
Module INFO-002 aims to derive Shannon channel capacity from Recognition Science ledger bandwidth. Capacity is $C = \max_{p(x)} I(X;Y)$ bits per use; discrete input distributions are records of nonnegative probabilities on $\mathrm{Fin}, n$ that sum to one.
An InputDistribution n therefore carries three fields: a probability map, a nonnegativity proof, and a normalization proof. The uniform candidate sets every mass to $1/n$. This lemma discharges the normalization obligation for that candidate.
The local setting is classical finite-alphabet information theory inside the RS ledger story; no J-cost or phi-ladder structure is used here.
proof idea
Tactic proof. Rewrite the sum via Finset.sum_const and Finset.card_fin, so it becomes $n \cdot (1/n)$ in the reals (nsmul_eq_mul). Obtain $(n : \mathbb{R}) \neq 0$ from Nat.cast_ne_zero and omega on the hypothesis $n > 0$. Finish with field_simp.
why it matters
Direct parent is uniformDistribution, which packages the constant map $x \mapsto 1/n$ as a valid InputDistribution n by citing this lemma for normalized. That helper sits among the channel-capacity scaffolding (mutualInformation, channelCapacity, shannons_theorem, capacity_from_ledger) that implements the module target: capacity from ledger bandwidth.
In the broader RS picture this is bookkeeping, not a forcing-chain step. It lets the discrete max over input laws include the uniform law, which is the usual first test case before Gaussian or ledger-derived bounds. No T5–T8 landmark is touched; the link to RS is only through the surrounding capacity-from-ledger program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.