euler_identity_Q3

formal source

 209-/
 210
 211/-- The Euler-characteristic identity for Q₃. -/
 212theorem euler_identity_Q3 :
 213    cube_vertices' 3 + cube_faces' 3 - cube_body = cube_edges' 3 + 1 := by
 214  native_decide
 215
 216/-- Therefore 13 has three equivalent natural-invariant interpretations. -/
 217theorem thirteen_natural_interpretations :
 218    -- V + F - C
 219    cube_vertices' 3 + cube_faces' 3 - cube_body = 13 ∧
 220    -- E + 1
 221    cube_edges' 3 + 1 = 13 ∧
 222    -- The value equals itself
 223    (13 : ℕ) = 13 := by
 224  refine ⟨?_, ?_, rfl⟩ <;> native_decide
 225
 226/-! ## Summary of What This Module Proves
 227
 2281. **Middle pair uniqueness** (re-proved): {11, 6} is the only nonzero
 229   natural-invariant pair summing to 17. See `middle_pair_unique_nonzero`.
 230
 2312. **Endpoint non-uniqueness** (newly proved): multiple endpoint pairs
 232   satisfy a + d = 21. See `endpoint_pairs_not_unique`.
 233
 2343. **Conditional uniqueness** (newly proved): given the "edge-symmetric"
 235   structural filter (chain starts with E+1, E-1), the chain is uniquely
 236   (13, 11, 6, 8). See `current_chain_unique_modulo_edge_pair_filter`.
 237
 2384. **Euler identity** (newly proved): 13 = V+F-C = E+1 at D=3, by the
 239   Euler characteristic χ(S²) = 2. See `euler_identity_Q3`.
 240
 241## Residual Openness
 242