docs(theory): part II — error bounds, reproducibility, and the verification game - #379
Merged
Conversation
…a stale bias comment
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 section 6 lists the claims we deliberately refuse
to make.
The load-bearing results:
Thm 1 2*bias = offset_max, so the ladder is exponent-symmetric about
unity by construction.
Thm 3 Multiplication needs at most one renormalization step: the
product significand lies in [1,4).
Thm 5 GF-T addition is commutative but NOT associative, with a 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.
Section 4 places the ternary claim honestly. It cites the radix-economy
theorem correctly (3 minimizes b/ln b over the integers; 2 and 4 tie
EXACTLY, so "closest to e" is coincidence-shaped reasoning), and it
quotes the 1950 ERA source disclaiming its own result in the next
sentence. It records that Setun's cost advantage is self-reported by
Brusentsov and never independently benchmarked, that Knuth's "prettiest
number system" is an aesthetic judgment, and that balanced ternary
predates both (Lalanne 1840, weights problem in Bachet 1624).
Section 5 argues the substantive contrast is with posits, not with 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.
It also states plainly that the exponent base is 2, NOT phi. The
phi^a * phi^b = phi^(a+b) comment asserts exponent additivity, true for
any base; phi's real role is generating the ladder geometry
(Et = fib(k+1)+1, M = fib(k+1)^2). Claiming a phi-radix format would be
the easiest way to lose a reviewer, and it would be false.
Spec fix found by that 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 and icarus (10/10) and zig stay green.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part I stated the format and the ring as theorems. Part II does the two things it could not: it makes the reduction-order result quantitative, and it places the bond/challenge design against the verification-game literature — including eight published results that bound or contradict what a design of this shape can claim.
Positive results
v = 2u, one-sided — twice the round-to-nearest bound (Boldo et al. 2023 §2.5)dot4balanced tree has a strictly tighter bound than a left fold —2vvs3vat n=4;6vvs63vat n=64. Part I pinned the tree because a verifier folding differently would slash an honest executor; it turns out to also be the numerically better choice. That's a dividend, not the reason.§5 — the eight obstructions (the important section)
λn² + cn. Above that, bribable at any bond.Two corrections the research forced on the draft
Both would have been wrong in print:
3f+1is a synchronous-model result. Dwork–Lynch–Stockmeyer Table I: under partial synchrony authenticated Byzantine still needs3t+1— verbatim "authentication does not improve resiliency". Dropping "under synchrony" makes the claim false.2q−n>fyieldsn>3f, not2f+1, and presupposes signed results (Malkhi–Reiter dissemination quorums). Unsigned needsn>4f. Signing is what buys the drop from4fto3f.Also states the correct bond-sizing citation — Polinsky–Shavell eq. (6),
f* = h/p, with underdeterrence whenever wealth< h/p— not Becker, who gives the risk-neutral special case rather than deriving it. And documents verbatim that TrueBit (§4.3, §5.2) and Arbitrum (§3.5) declare value-at-risk bond sizing out of scope, which is the gap the ring's outstanding-scaled bond addresses.Docs only; no spec, gen, or workflow changes.
🤖 Generated with Claude Code