claim5-analytic/PROOF.md

# Claim 5 analytic certificate

Decision: **verified** by an independent measure-zero proof and a direct
convexity proof.

The all-time singleton statement is reduced, on each finite leader history, to
the zero set of a nonzero quadratic polynomial.  The coefficient argument uses
only `sum(a)=1`, `sum(b)=0`, and invertibility of the key-query matrix.  A
finite union covers each time and a countable union covers all integer times.

Lemma 2.2 follows immediately because every new token is a scalar convex
combination of two points in the old hull.

The rational-arithmetic audit checked 10,236
leader-map/step-size combinations, 50,214
row invariants, and 487,935 exact
query/candidate coefficient systems.  It found no case where the tie
polynomial vanished identically for distinct candidate maps.

Destructive controls passed:

- Singular `B=0` produced multiplicity
  [2, 2].
- `gamma=6/5` moved 0 toward 1 to
  6/5, outside
  `[0,1]`.
- The coordinate-wise matrix step produced
  ['2/5', '7/10'] with coordinate
  sum 11/10, outside the
  unit triangle.