206theorem no_eighth_plot (δ : F2Power 3) (hδ : δ ≠ 0) : 207 ∃ p : BookerPlotFamily, plotEncoding p = δ := by
proof body
Tactic-mode proof.
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. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.