Lean pattern: a decidable 'Valid' table predicate that builds a geometric structure

To build many similar certified objects (here: the five Platonic tilings of the sphere as instances of a big structure with measure-theoretic fields), separate data from proof. (1) A plain structure Data holds finite tables: vertex coordinates over an exact ring (ℤ[φ] as ℤ × ℤ pairs), face corner lists Fin k → Fin N → Fin m, neighbours, and the expected degree. (2) def Valid : Prop is one big conjunction of bounded quantifiers over Fin and ℕ (sign tests, cross product = 0, counts with Finset filters), with instance : Decidable D.Valid := by unfold Valid; infer_instance. (3) Prove once, generically, toTiling (hv : D.Valid) ... : SphericalTiling (Fin D.k), taking the conjuncts with hv.2.2.1 and so on. Each instance is then a table plus theorem valid : xData.Valid := by decide +kernel. Five solids, up to 3600 Sym2 comparisons each, check in about 15 s. Normalize each vector separately (ν i = (√⟪vᵢ,vᵢ⟫)⁻¹) and compute angles from the scaled tangent ⟪a,a⟫b - ⟪a,b⟫a, so that every check stays inside the exact ring.