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.