cortical_has_6
plain-language theorem explainer
Recognition Science records six cortical layers as one instance of the cube-face count that recurs across domains for spatial dimension three. A physicist or mathematician auditing the cross-domain module would reference this theorem when verifying the structural claim that six equals the number of faces on the three-dimensional cube. The proof is a one-line wrapper that unfolds the cardinality predicate and lets the decision procedure confirm equality on the six-constructor inductive type.
Claim. The inductive type CorticalLayer has cardinality six: $Fintype.card(CorticalLayer) = 6$.
background
The module CrossDomain.CubeFaceUniversality asserts that the count of six appears uniformly as the number of faces of the three-cube across several domains in Recognition Science. HasCubeFaceCount is the predicate asserting that a finite type T has exactly six elements. CorticalLayer is the inductive type with constructors l1 through l6 that derives a Fintype instance needed for cardinality computation.
proof idea
The proof is a one-line wrapper. It unfolds HasCubeFaceCount to expose the equality Fintype.card CorticalLayer = 6, then applies the decide tactic which computes the finite cardinality of the six-constructor inductive type.
why it matters
This theorem supplies the cortical_6 field in the cubeFaceUniversalityCert definition, which collects the six-domain instances to certify the cube-face universality. It directly supports the module claim that six equals the face count for D = 3 in the Recognition Science framework, linking to the spatial dimension derivation. The proof is complete with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.