boolOrbitInterpret
plain-language theorem explainer
boolOrbitInterpret supplies a parity-based map from the inductive LogicNat orbit to the Boolean domain. Researchers constructing discrete propositional carriers for the Law of Logic cite it when building the first non-continuous test case of Universal Forcing. The definition is a direct recursive pattern match on the two constructors of LogicNat.
Claim. Define the function $f :$ LogicNat $→$ Bool by $f($identity$) =$ false and $f($step $n) = ¬ f(n)$, where LogicNat is the inductive type whose constructors generate the free orbit under the Law of Logic.
background
The module DiscreteLogicRealization supplies the second Law-of-Logic realization: a discrete Boolean/propositional carrier that serves as the first non-continuous test case for Universal Forcing. LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity) and step (one further iteration of the generator), mirroring the orbit {1, γ, γ², …} as the smallest subset of ℝ₊ closed under multiplication by γ and containing 1. The definition depends on this inductive type from ArithmeticFromLogic together with auxiliary structures such as ObserverForcing.identity and PhiForcingDerived.of that calibrate J-cost minima.
proof idea
The definition is given directly by pattern matching: the identity constructor maps to false and the step constructor recurses with Boolean negation.
why it matters
boolOrbitInterpret is invoked inside boolRealization to equip the Boolean carrier of the discrete propositional Law-of-Logic realization. It therefore supplies the concrete interpretation needed to test the forcing chain (T0–T8) and the Recognition Composition Law on a non-continuous domain before moving to continuous J-cost structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.