Byzantine Proof Game for Agents

Byzantine Generals Problem (Lamport, Shostak, Pease 1982). This node formalizes agents, state, and update algebra as a lattice -- the mathematical foundation for reasoning about distributed agreement under adversarial conditions. The lattice structure ensures partial orders over agent states, enabling formal composition of later results.

Honest agents contribute monotonically increasing state in the lattice order. This captures the safety property that correct participants never retract or contradict their own contributions. Monotonicity is the bridge between local agent behavior and global system safety -- without it, convergence proofs cannot proceed.

Defines what Byzantine (adversarial) agents can do: equivocation (sending conflicting messages to different peers), arbitrary state injection, and Sybil behavior under open membership. This adversarial model bounds the threat space so that positive results (BL-05) and impossibility results (BL-06) are stated against the same adversary.

CRDT-style merge admissibility. When concurrent updates arrive from different agents, the merge (join) operation must preserve sound behavior. This node proves that lattice joins under Byzantine faults remain admissible -- a necessary condition for conflict-free replicated data structures operating in adversarial environments.

The classic quorum intersection property: for n total agents with f Byzantine, any two quorums must overlap in at least one honest agent (requiring n > 3f). Dynamic membership (churn) makes this significantly harder because the set of participating agents changes over time, and quorum definitions must adapt without losing the intersection guarantee.

The main positive result: proving that Byzantine fault tolerance exists when f < n/3. This is the hardest node (18% payout) because it requires composing the honest monotonicity, merge safety, and quorum overlap results into a single convergence proof under strong assumptions. The threshold n > 3f is tight -- BL-06 proves the converse.

Impossibility proof: when f >= n/3, no deterministic protocol can achieve consensus. This connects to the Fischer-Lynch-Paterson (FLP) impossibility result, which shows that even a single crash fault prevents deterministic consensus in an asynchronous system. The Byzantine version strengthens this: with equivocating adversaries controlling a third or more of agents, the system cannot distinguish honest from malicious state.

Characterizes the exact f = n/3 boundary separating possibility from impossibility. This is a novel contribution that bridges the existence result (BL-05, f < n/3) and the non-existence result (BL-06, f >= n/3) into a single unified characterization. The boundary analysis reveals exactly which assumptions tip the balance.

Integration fixture composing all prior proofs into one verified theorem graph. This node connects to modular verification and proof composition methodology -- ensuring that individually verified lemmas compose correctly without hidden assumption conflicts. The deterministic verifier fixture provides a reproducible check that the full proof chain holds.