ledgerCost_single
plain-language theorem explainer
A ledger posting multiplicity n at a single defect type i costs exactly n times the weight w(i). Anyone working the free additive recognition ledger floor cites this as the base evaluation rule for pure single-support ledgers. The proof unfolds the weighted Finsupp sum and applies the single-index summation identity.
Claim. For any weight $w : I \to \mathbb{R}$, index $i \in I$, and $n \in \mathbb{N}$, the recognition cost of the finitely supported ledger that places multiplicity $n$ only at $i$ equals $n \cdot w(i)$.
background
The module builds the free additive cost floor that closes the T-1/T0 audit gaps: the kernel gap (observable equivalence derived from cost) and the cokernel gap (independent defects accumulate with multiplicity). The carrier is the free commutative monoid on primitive distinctions, DefectLedger I := I →₀ ℕ, i.e. finitely supported maps from distinction labels to natural multiplicities.
Recognition cost under a per-distinction weight $w$ is the total weighted multiplicity: sum over support of $n_i \cdot w(i)$. That is the definition this lemma evaluates. The module states that on this carrier additivity is unconditional, the observable equivalence is the cost kernel, and two independent copies of the same defect cost $2w(i)$ rather than $w(i)$.
Upstream, the cost is exactly that Finsupp sum; the LedgerFloor package re-exports the same definition. This single-support evaluation is the atomic case of that sum.
proof idea
One-line style tactic proof. Unfold the cost definition to expose the Finsupp sum of $(n : \mathbb{R}) \cdot w(i)$ over the support. Rewrite by the standard library identity that summing a function against a single-point finitely supported map returns the value at that point (with the zero-at-empty side condition discharged by simp). No further arithmetic is needed.
why it matters
This is the atomic evaluation rule for the free ledger floor. Downstream, two_independent_same_defects rewrites additivity plus this lemma to get cost $2w(i)$ for two unit postings of the same defect: the cokernel fix that makes multiplicity genuine so independence need not be restricted to dodge $1=2$. The Boolean T0 floor is recovered as the unit-weight truncation via the same rewrite (boolean_floor_is_truncation). Non-vacuity of the observable floor also routes through single-support costs.
In holography, recognition multiplicity of a $k$-face cell is defined as unit-weight ledger cost of the cell ledger; equality to the face count $k$ is proved by induction using additivity together with this single-support rule, with no reference to the closure map. It also feeds the primitive-ledger posting argument that forces the additive response law for arbitrary real postings. Framework role: grounds the free monoid answer to the Anil T-1/T0 critique before the forcing chain (T5 J-uniqueness onward) builds on a non-vacuous cost floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.