cognitiveStateSpaceCert
plain-language theorem explainer
This definition assembles the certificate asserting that the product of three 5-element sets for sense, emotion, and memory yields a cognitive state space of cardinality 125 with surjective projections and strict irreducibility to any factor or pair. Researchers modeling conscious moments under the Recognition Science cross-domain decomposition would cite it as the formal enumeration of the 5³ structure. The construction is a direct record that bundles the cardinality theorem with the surjectivity and non-collapse lemmas proved earlier in the同一
Claim. The certificate asserts that $|S| = 5$, $|E| = 5$, $|M| = 5$ where $S$, $E$, $M$ are the sense, emotion, and memory-system types, that the product $S × E × M$ has cardinality 125, that each of the three projections is surjective, and that the product cardinality strictly exceeds each factor cardinality and the pairwise product cardinality of sense and emotion.
background
The module defines three factor types each of cardinality 5 and forms their product type CognitiveState. It then proves the product has exactly 125 elements and that the natural projections onto each factor are surjective. The certificate structure collects these facts together with four irreducibility statements showing the product is strictly larger than any single factor or the sense-emotion pair. Upstream, the cardinality theorem is obtained by direct simplification over the three factor cardinalities and the product rule for finite types. The local setting is the structural claim that a conscious moment is spanned by three orthogonal recognition axes each of configDim 5, with the explicit caveat that empirical independence in neural data lies outside the formal system.
proof idea
This is a definition that constructs the certificate record by assigning the product_count field to the result of the cardinality theorem and wiring the three surjectivity fields and four irreducibility fields directly to the corresponding sibling theorems for sense projection, emotion projection, memory projection, and the four non-collapse statements.
why it matters
The definition supplies the complete certificate for the 125-state cognitive space that realizes the module's structural claim. It closes the local development chain for the cross-domain enumeration under the three-axis decomposition. The module explicitly notes that the result does not address empirical independence of the axes in neural data, which remains a testable hypothesis outside the Lean formalization. No downstream uses are recorded, indicating the certificate functions as a terminal summary object for this domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.