BraakStage
plain-language theorem explainer
BraakStage enumerates the six stages of Parkinson's disease progression as a finite inductive type equipped with decidable equality. Cross-domain researchers cite it to exhibit the recurrence of the cube-face count 6 in medical staging alongside quarks and leptons. The construction is a direct inductive definition that derives the standard typeclass instances automatically.
Claim. Let $B$ be the inductive type with six distinct elements $b_1, b_2, b_3, b_4, b_5, b_6$, equipped with decidable equality, representation, boolean equality, and finite-type structure.
background
The Cube-Face Universality module advances claim C15 that the integer 6 equals the face count of the 3-cube, satisfying Euler's formula with $F=6$. This count is required to appear uniformly across domains, including the six Braak stages of Parkinson's progression. The module imports Mathlib to obtain the derived instances DecidableEq, Repr, BEq, and Fintype.
proof idea
The declaration is a direct inductive definition introducing the six constructors b1 through b6. The deriving clause supplies the four typeclass instances from the standard library with no further proof obligations.
why it matters
BraakStage supplies the type used by braak_has_6, which asserts HasCubeFaceCount BraakStage, and by the CubeFaceUniversalityCert structure that aggregates six such instances. It supports the cross-domain claim that the 3-cube face count appears in disease staging, consistent with the derivation of three spatial dimensions. No open scaffolding questions are closed by this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.