consciousnessGapCert
plain-language theorem explainer
This definition packages the assertion of exactly five consciousness theories together with a non-empty explanatory gap into a single certificate structure. Philosophers of mind working inside the Recognition Science treatment of the hard problem would cite the resulting object when stating the limits of J-cost accounts. The construction is a direct record assembly that pulls the theory count from its cardinality theorem and the gap witness from its inhabitance theorem.
Claim. A certificate structure asserting that the cardinality of the set of consciousness theories equals five and that the explanatory gap is non-empty.
background
Recognition Science treats the explanatory gap as the distance between J-cost descriptions of recognition structure and the intrinsic first-person character of experience. The module lists five candidate theories (integrated information, global workspace, higher-order thought, recurrent processing, predictive processing) whose count is fixed at five. The upstream theorem consciousnessTheoryCount establishes this cardinality by direct computation, while the upstream theorem explanatory_gap_nonempty supplies a concrete witness that the gap is non-trivially inhabited at the J-cost minimum (r=1 witnesses J=0).
proof idea
The definition is a one-line record constructor that populates the five_theories field from the cardinality theorem and the gap_nonempty field from the witness theorem.
why it matters
This definition supplies the formal object that encodes the RS position on the hard problem: the gap is relocated to the requirement of an inhabitance posit rather than derived from the J-cost functional equation. It completes the accounting in the module by certifying both the theory count and the gap's non-emptiness. The construction touches the framework landmark that recognition events carry a J-cost minimum at which qualia-like properties are posited but not reduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.