list_sum_pos
plain-language theorem explainer
A standard positivity lemma for finite lists of positive reals guarantees that their sum is positive. It is invoked inside the GCIC derivation to turn per-boundary J-cost positivity into a strict collective inequality between the aligned configuration and any perturbed collection. The proof runs by induction on list length, with a nil contradiction, head extraction, tail recursion, and linarith closure on the two positive summands.
Claim. Let $(c_i)_{i=1}^n$ be a finite sequence of real numbers with $n>0$ and $c_i>0$ for every $i$. Then the sum of the sequence is strictly positive.
background
The GCICDerivation module obtains the Global Co-Identity Constraint directly from the J-cost forcing chain (T5 J-uniqueness through T8 three-dimensionality) with no empirical axioms. Upstream structures supply the definition of J-cost as the Recognition Science cost functional on ratios together with the ledger factorization that places it on the positive reals. list_sum_pos is the arithmetic bridge that converts the hypothesis that every perturbed boundary carries positive J-cost into the statement that their total exceeds the aligned (J=0) cost.
proof idea
The proof is by induction on the input list. The nil case contradicts the length hypothesis via simp. In the cons case the head is extracted as positive by membership, the tail is re-expressed with its own positivity and length hypotheses, the inductive hypothesis is applied to the tail, and linarith adds the two positive quantities.
why it matters
The lemma supplies the final arithmetic step in aligned_beats_perturbed, which asserts that the aligned configuration is strictly cheaper than any collection of perturbed boundaries and thereby replaces an empirical axiom in the GCIC derivation. It closes the subadditivity argument that follows from the J-cost definition in the forcing chain (T5–T8). No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.