evidence/claim5/method.md

# Method

The verifier implements the actual attention data path: dot-product scores,
softmax exponentials, normalization, and weighted value aggregation. Because
`Q=K=0`, every score is zero, `exp(0)=1`, and exact `Fraction` arithmetic
produces weights `1/k`.

It compares attention output with a separately implemented direct mean for all
873 permutations of fixed two-dimensional rational feature sequences at
lengths one through six.

The negative control changes the score vector to `[0,1]`. A 50-digit Decimal
softmax gives unequal weights, so the control must be rejected as uniform
attention.