docs(theory): formal GF-T theory with 30 labelled propositions + fix a stale bias comment

[gHashTag]

Adds docs/GF_T_FORMAL_THEORY.md — the GF-T format and the compute ring stated as theorems over the executable spec definitions, each discharged by an in-spec assertion, an exhaustive sweep, or a proof given inline. Every claim carries an epistemic label (PROVEN / MEASURED / MODELED / FOLKLORE / OPEN), and §6 lists the claims we deliberately refuse to make.

The load-bearing results

Thm 1	2·bias = offset_max — the ladder is exponent-symmetric about unity by construction
Thm 3	multiplication needs at most one renormalization step (product significand ∈ [1,4))
Thm 5	GF-T addition is commutative but not associative — 1-ULP counterexample, confirmed on iverilog
Cor 5.1	therefore reduction order is part of the specification: a verifier folding a dot claim differently would slash an honest executor. Systems that leave reduction order to the implementation cannot support this dispute model at all.
Thm 7	the zero sentinel is not injective — (0,0) collides with the smallest normal. Recorded as a limitation, not hidden.
Thm 9	single-op disputes need no bisection: bit-exactness makes a fraud proof O(1), not O(log n)
Thm 12	freshness must precede every other guard and must not advance the watermark on non-terminal outcomes — else one malformed high-epoch dispute is a replay-nonce DoS
Thm 19	the reputation cap must be computed in u64: in u32 a crafted gain wraps the sum to 0, so honest work would zero a maxed reputation
Thm 24	(family, op) is a lossy skill proxy — GFT8 and GFT16 multiply share both, so a width-blind gate pays GF-T16 rates for 8-bit work

Honest placement in the literature (§4–5)

• Radix economy cited correctly: 3 minimizes b/ln b over the integers, and 2 and 4 tie exactly — so "3 wins because it's closest to e" is coincidence-shaped reasoning. We quote the 1950 ERA source disclaiming its own result in the next sentence.
• Setun's cost advantage is self-reported by Brusentsov, never independently benchmarked. Knuth's "prettiest number system" is an aesthetic judgment. Balanced ternary predates both (Lalanne 1840; weights problem in Bachet 1624).
• The substantive contrast is with posits, not radix mysticism: tapering costs scale invariance of accuracy (de Dinechin et al., CoNGA 2019), so error analyses stop transferring. GF-T is untapered by choice — stated as a trade, with what it gives up.
• BitNet's 71.4× energy figure is labelled MODELED (arithmetic-only, excludes memory) with the published Amdahl counter-result cited.

The exponent base is 2, not φ. The phi^a · phi^b = phi^(a+b) comment asserts exponent additivity, true for any base; φ's real role is generating the ladder geometry (Et = fib(k+1)+1, M = fib(k+1)²). Claiming a φ-radix format would be the easiest way to lose a reviewer — and it would be false.

Spec fix found by the audit

gft_bias's comment claimed GF-T32 -> 121, a fossil of the pre-ratification Et5 geometry. The ratified value is 364 (Et6), which the assertion three lines below already pins. Comment-only: gen output is byte-identical, icarus 10/10 and zig stay green.

🤖 Generated with Claude Code