thirteen_natural_interpretations

formal source

 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
 243The only unresolved step is: *why* the edge-symmetric pair (E+1, E-1) appears
 244as the "opening" of the cyclic chain (i.e., why Up-quark generation steps
 245are {V+F-C, E-A} = {13, 11} rather than e.g. {V+F, V-C} = {14, 7}).
 246
 247This reflects a physical identification of the U(1) gauge channel with the