BraakStage
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive Braak stages from the J-uniqueness functional equation.
- Does not model the physical mechanism of Parkinson's progression.
- Does not assert that 6 appears in every Recognition Science domain.
- Does not invoke the Recognition Composition Law or the phi-ladder.
formal statement (Lean)
43inductive BraakStage where
44 | b1 | b2 | b3 | b4 | b5 | b6
45 deriving DecidableEq, Repr, BEq, Fintype
46