braak_has_6
plain-language theorem explainer
BraakStage, the inductive type enumerating six stages of Parkinson's progression, satisfies the cube-face count predicate. Cross-domain Recognition Science work cites this when assembling the universality certificate across quarks, leptons, cortical layers, and kinematics. The proof is a one-line wrapper that unfolds the cardinality predicate and decides the finite type.
Claim. The inductive type with six constructors for Parkinson's disease stages satisfies $Fintype.card = 6$.
background
HasCubeFaceCount is the proposition that a type T with a Fintype instance has exactly six elements. BraakStage is the inductive type whose constructors b1 through b6 label the stages of disease progression and derives the Fintype instance. The module collects these instances to show that the count six equals the face count of the three-cube, a direct consequence of three spatial dimensions.
proof idea
The proof is a one-line wrapper that unfolds HasCubeFaceCount and invokes the decide tactic on the finite cardinality.
why it matters
This theorem populates the braak_6 field inside cubeFaceUniversalityCert, the bundled certificate that gathers six-count results from five other domains. It directly instantiates the module claim that six equals two times three, the product of binary face states and spatial dimension three, consistent with the forcing chain step that fixes D equals three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.