predictedObservable
plain-language theorem explainer
The definition maps each of the nine CombinationID constructors to a distinct PredictedObservable. Researchers checking empirical protocols for the cross-domain theorems cite it to verify that every structural claim carries an attached observable. The implementation is a direct exhaustive case split on the inductive type with no lemmas applied.
Claim. The function $f$ from CombinationID to PredictedObservable is given by $f(c_1) = o_1$, $f(c_2) = o_2$, ..., $f(c_9) = o_9$, where the pairs are (cognitive tensor, tensor rank 125), (planet strata, strata ratio phi power), (oncology tensor, multiplicative therapy response), (quantum molecular depth, five-bit address bound), (attention tensor, forty stable five transient), (Erikson reverse, reverse Erikson order), (universal response, unit response coefficient), (Miller span, q-space span sequence), and (regulatory ceiling, regulatory ceiling 70).
background
The module defines a finite registry that pairs each of the nine implemented cross-domain theorems with a concrete empirical test class. CombinationID is the inductive type whose nine constructors enumerate the combinations C1 through C9. PredictedObservable is the inductive type whose nine constructors list the observables that the Recognition Science structural theorems plus the RS hypothesis predict for each case.
proof idea
The definition is realized by exhaustive pattern matching on the nine constructors of CombinationID, returning the corresponding constructor of PredictedObservable in each branch. No upstream lemmas are applied; the mapping is a static one-to-one assignment.
why it matters
This definition supplies the observable field required by ProtocolFalsifiable, protocolFalsifiable_all, ProtocolMatches, and protocolSpec. It directly realizes the registry's stated purpose of keeping falsifiers attached to the Lean theorem bundle so the cross-domain claims cannot drift into unfalsifiable numerology. The construction supports the framework requirement that every theorem remain tied to an empirical test.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.