boolOrbitInterpret
boolOrbitInterpret defines the parity map sending the base identity of the LogicNat orbit to false and negating on each step, furnishing the Boolean carrier for the discrete propositional realization. Researchers building non-continuous models of the Law of Logic cite it as the first explicit test case for Universal Forcing outside continuous settings. The definition is supplied directly by recursion on the two constructors of LogicNat.
claimDefine the map from the orbit generated by the Law of Logic to the Boolean carrier by parity: the identity element is sent to false and each successive step negates the image of its predecessor.
background
The module introduces the second Law-of-Logic realization as a discrete Boolean carrier, serving as the first non-continuous test case for Universal Forcing. LogicNat is the inductive type whose constructors identity and step generate the free orbit closed under the generator, with identity as the zero-cost base element. Upstream results include the inductive definition of LogicNat in ArithmeticFromLogic, the J-cost structures from PhiForcingDerived and DAlembert.LedgerFactorization, and the identity event from ObserverForcing.
proof idea
The definition proceeds by direct pattern matching on the constructors of LogicNat: the identity case returns false while the step case applies Boolean negation to the recursive call on the predecessor.
why it matters in Recognition Science
This definition supplies the interpretation function used by boolRealization to equip the Boolean carrier with the required structure for the discrete propositional Law-of-Logic realization. It provides the first explicit non-continuous test case for Universal Forcing and links to the forcing chain steps T5 through T8. It touches the open question of which discrete carriers admit faithful realizations of the Recognition Composition Law.
scope and limits
- Does not prove any invariance or cost properties of the map.
- Does not extend the construction to continuous carriers or other types.
- Does not compute J-costs or reference physical constants.
- Does not address higher-dimensional or multi-carrier realizations.
formal statement (Lean)
29def boolOrbitInterpret : ArithmeticFromLogic.LogicNat → Bool
30 | ArithmeticFromLogic.LogicNat.identity => false
31 | ArithmeticFromLogic.LogicNat.step n => Bool.not (boolOrbitInterpret n)
32
33/-- The discrete propositional Law-of-Logic realization. -/