no_injective_real_to_bool
plain-language theorem explainer
No function from the reals to the booleans is injective. Researchers tracing the T5 to T6 bridge in Recognition Science cite this to show that ClosedObservableFramework alone cannot force an injective orbit embedding. The proof assumes injectivity and derives a contradiction by case analysis on the images of 0, 1, and 2.
Claim. No function $f : ℝ → Bool$ is injective.
background
The module HierarchyRealizationObstruction supplies an honesty check for the T5→T6 bridge. It demonstrates that the ClosedObservableFramework primitive is too weak to derive ratio_self_similar or additive_posting on the orbit levels k ↦ r(T^[k] baseState). The upstream embed from ArithmeticFromLogic maps LogicNat into the positive reals by repeated multiplication by a generator value. This theorem supplies the basic cardinality obstruction used to construct the explicit finite counterexample boolFramework.
proof idea
Assume for contradiction that the map embed is injective. Case on whether embed 0 equals embed 1. If equal, injectivity forces 0 = 1, contradiction. Otherwise case on the three boolean values of embed 0, embed 1, embed 2 to obtain that either embed 0 equals embed 2 or embed 1 equals embed 2. Injectivity then yields 0 = 2 or 1 = 2, again contradiction.
why it matters
The theorem is the key lemma feeding boolFramework, the finite counterexample whose orbit alternates between observable values 1 and 2. It directly supports the module claim that ClosedObservableFramework does not force realizedHierarchy fields. This closes the honesty check for the T5 J-uniqueness to T6 phi fixed-point step and shows that stronger structure, such as the Recognition Composition Law, is required downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.