CorticalLayer
plain-language theorem explainer
The CorticalLayer inductive type enumerates six distinct brain layers as a finite set. Neuroscientists or Recognition Science modelers cite it to confirm that cortical architecture matches the universal face count of the 3-cube. The definition lists six constructors and derives DecidableEq, Repr, BEq, and Fintype instances in one step.
Claim. Let $C$ be the finite type whose elements are six distinct labels. Then $C$ carries decidable equality, a representation, Boolean equality, and a Fintype instance of cardinality six.
background
The CubeFaceUniversality module asserts that the integer 6 arises as the face count of the 3-cube (V-E+F=8-12+6=2) and recurs across independent domains when spatial dimension equals three. CorticalLayer supplies the neuroscience instance: the six layers of the neocortex. The sibling predicate HasCubeFaceCount is the statement that a type has exactly six elements; the downstream theorem cortical_has_6 simply unfolds this predicate and decides it for the layer type.
proof idea
The declaration is a direct inductive definition that introduces six constructors followed by a deriving clause. No lemmas are applied; the Fintype and equality instances are generated automatically by the Lean typeclass machinery.
why it matters
CorticalLayer populates the cortical_6 field of the CubeFaceUniversalityCert structure, which collects the six-element proofs for quarks, leptons, cortical layers, Braak stages, and robotic degrees of freedom. It thereby instantiates the cross-domain claim that 6 equals 2 times 3 for any D=3 enumeration, consistent with the Recognition Science forcing chain that fixes three spatial dimensions at step T8. The module reports zero sorrys, closing this particular enumeration without further scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.