predictedObservable_injective
plain-language theorem explainer
The theorem shows that the assignment of predicted observables to the nine CombinationIDs is injective. Registry maintainers cite it to confirm distinct signatures for each cross-domain theorem. The proof is a term-mode case split on the constructors of CombinationID followed by simplification against the definition of predictedObservable.
Claim. Let $f$ be the function from CombinationID to PredictedObservable that sends each of the nine combinations to its assigned observable (tensorRank125 for the first, strataRatioPhiPower for the second, and so on). Then $f$ is injective.
background
The Option A Falsifier Registry pairs each C1-C9 cross-domain theorem with an empirical test class while keeping the falsifiers attached to the Lean bundle. This prevents the cross-domain claims from drifting into unfalsifiable numerology. The upstream definition predictedObservable supplies the concrete mapping: c1CognitiveTensor to tensorRank125, c2PlanetStrata to strataRatioPhiPower, c3OncologyTensor to multiplicativeTherapyResponse, and likewise for the remaining six combinations.
proof idea
The term proof introduces a and b together with the equality hypothesis h. Exhaustive case analysis on the constructors of a and b is performed, after which simp rewrites with the definition of predictedObservable and discharges the resulting equalities by the distinct target observables.
why it matters
Injectivity guarantees that the nine predicted observables remain distinct, which is recorded in the count used by falsifierRegistryCert. The result therefore directly supports the module's purpose of anchoring the C1-C9 theorems to concrete empirical observables inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.