pith. machine review for the scientific record. sign in
theorem proved term proof

plot_composition_xor_additive

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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 :=

proof body

Term-mode proof.

 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). -/

depends on (9)

Lean names referenced from this declaration's body.