no_eighth_plot

formal source

 203/-- **Falsifier 1 of the paper.** Every non-zero `δ : F2Power 3` is
 204    the encoding of some Booker plot. There is no eighth plot
 205    expressible on three axes. -/
 206theorem no_eighth_plot (δ : F2Power 3) (hδ : δ ≠ 0) :
 207    ∃ p : BookerPlotFamily, plotEncoding p = δ := by
 208  have hmem : δ ∈ Finset.univ.filter (fun v : F2Power 3 => v ≠ 0) := by
 209    simp [Finset.mem_filter, Finset.mem_univ, hδ]
 210  rw [← plotEncoding_image_eq_nonzero] at hmem
 211  rcases Finset.mem_image.mp hmem with ⟨p, _, hp⟩
 212  exact ⟨p, hp⟩
 213
 214/-- **Falsifier 3 of the paper.** Plot composition is XOR-additive:
 215    when `δ_p ⊕ δ_q ≠ 0`, the composite is again one of the seven
 216    plots. -/
 217theorem plot_composition_xor_additive (p q : BookerPlotFamily)
 218    (h : plotEncoding p + plotEncoding q ≠ 0) :
 219    ∃ r : BookerPlotFamily,
 220      plotEncoding r = plotEncoding p + plotEncoding q :=
 221  no_eighth_plot _ h
 222
 223/-- The companion to Falsifier 3: when the composite XOR is zero
 224    (the two plots cancel), the composite is the trivial transition,
 225    i.e., `p = q` (since `v + v = 0` in characteristic 2 and the
 226    encoding is injective). -/
 227theorem plot_composition_cancels_iff (p q : BookerPlotFamily) :
 228    plotEncoding p + plotEncoding q = 0 ↔ p = q := by
 229  constructor
 230  · intro h
 231    -- In characteristic 2, a + b = 0 ↔ a = b (via add_self).
 232    -- From plotEncoding p + plotEncoding q = 0, add plotEncoding q
 233    -- to both sides: plotEncoding p + (plotEncoding q + plotEncoding q)
 234    -- = plotEncoding q. The bracketed term is 0 by F2Power.add_self.
 235    have heq : plotEncoding p = plotEncoding q := by
 236      have := congrArg (· + plotEncoding q) h