cortical_has_6
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the six-layer structure from the J-cost functional equation or forcing chain.
- Does not claim that six is the only possible count outside the six enumerated domains.
- Does not connect the result to the phi-ladder, mass formula, or alpha band.
- Does not prove that the inductive type is the unique model for cortical layers.
Lean usage
cortical_has_6formal statement (Lean)
55theorem cortical_has_6 : HasCubeFaceCount CorticalLayer := by
proof body
One-line wrapper that applies unfold.
56 unfold HasCubeFaceCount; decide