Counterexample · quantifier separation

FPRD-MN-C02

One good power need not imply an eventual tail

Exact statement

The scalar matrix M=[−1]M=[-1] is power nonnegative because M2=[1]M^2=[1], but it is not eventually nonnegative because every odd power is negative.

StatusProved by direct calculation
External reviewNo documented external or specialist review of this FPRD exposition is recorded.

Context

If one power M^k is nonnegative, then every positive multiple power M^{rk} is nonnegative, but other residue classes may remain negative forever.

Proof or evidence

Even powers of [-1] equal [1] and odd powers equal [-1].

Verification notes

The example was checked under the positive-exponent and universal-tail definitions.

Limitations

  • The example separates definitions; it says nothing about decision complexity.

Open work

Use this example as the standing guardrail against conflating an arithmetic progression of good powers with a cofinite tail.