CubeFaceUniversalityCert
plain-language theorem explainer
CubeFaceUniversalityCert bundles the statements that quarks, leptons, cortical layers, Braak stages, and robotic degrees of freedom each have exactly six elements, together with the arithmetic facts 6 = 2·3, the Euler characteristic 8-12+6=2, total fermion count 12, and 6³=216. A physicist tracing cross-domain enumerations in Recognition Science would cite this structure when collecting evidence that the cube-face count 6 appears uniformly for spatial dimension 3. The definition is assembled directly from six HasCubeFaceCount instances and the
Claim. A structure asserting that the set of quarks has cardinality 6, the set of leptons has cardinality 6, the set of cortical layers has cardinality 6, the set of Braak stages has cardinality 6, and the set of robotic degrees of freedom has cardinality 6, together with the identities $6=2·3$, $8-12+6=2$, the sum of quark and lepton cardinalities equals 12, and $6^3=216$.
background
HasCubeFaceCount(T) is the proposition that a finite type T satisfies |T|=6. The module defines five concrete types each equipped with Fintype instances: Quark (six flavors), Lepton (six species), CorticalLayer (six layers), BraakStage (six stages), and RoboticDOF (six axes). The local theoretical setting is the structural claim that the integer 6 equals the number of faces of the 3-cube and therefore appears as the enumeration size across independent domains once spatial dimension D=3 is fixed. Upstream, q3_euler records the identity 8-12+6=2 that supplies the topological origin of the count 6.
proof idea
The declaration is a structure definition whose fields are filled by direct reference to the sibling lemmas quark_has_6, lepton_has_6, cortical_has_6, braak_has_6, robotic_has_6 together with the three arithmetic facts proved by decide or rfl. No tactics are required beyond supplying the witnesses; the structure simply packages them into a single record.
why it matters
The structure supplies the single object consumed by the downstream definition cubeFaceUniversalityCert, which in turn witnesses the module-level claim that the cube-face count 6 recurs across particle physics, neuroanatomy, and robotics precisely because 6=2·3 for D=3. It therefore closes one concrete instance of the cross-domain universality pattern stated in the module header and aligns with the Recognition Science landmark that spatial dimension is forced to equal 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.