dimension_status
plain-language theorem explainer
Recognition dimension equals the minimum count of independent recognizers needed to separate all configurations in a geometry. Quantum information theorists and geometric foundation researchers would cite the definition for its direct operational link between recognizer independence and Hilbert space dimension. The definition assembles the status string through direct concatenation of fixed ASCII blocks that list module theorems and state the spacetime and quantum interpretations.
Claim. The recognition dimension is the minimum number of independent recognizers required to distinguish all configurations, with spacetime dimension equal to four and quantum dimension equal to the count of independent observables.
background
The module sets recognition dimension as the operational count of independent recognizers that separate configurations, directly explaining why spacetime requires four coordinates and why quantum state spaces have dimension equal to the number of independent observables. The supplied doc-comment states that Hilbert space dimension equals the number of independent observables, with spin-1/2 requiring two (Sz, Sx) and the harmonic oscillator requiring infinitely many Fock states. Upstream results supply auxiliary definitions such as independent axes carried by distinct primitives and evaluation of counted-once resource expressions, which the module imports to support the broader recognizer composition framework.
proof idea
The definition constructs the string by direct concatenation of a fixed multi-line ASCII literal that enumerates the separating recognizer properties and physical interpretations; no lemmas or tactics are applied.
why it matters
The definition supplies the module-level status summary that records the central claim of recognition geometry: dimension equals the minimum independent recognizer count. It supports the framework step that derives geometric dimension from recognizer structure and notes the physical reading that four coordinates separate events. The declaration touches the open question of closing the link between the eight-tick octave and observed spacetime dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.