interpret_zero
plain-language theorem explainer
The interpret function maps the identity constructor of LogicNat to the distinguished one element of any StrictLogicRealization. Authors constructing concrete Law-of-Logic models cite this base case to confirm alignment with the free-orbit construction used in universal forcing. The equality follows immediately from the recursive clause in the definition of interpret.
Claim. For every strict realization $R$, the interpretation of the identity element of LogicNat equals the distinguished unit element of $R$: $interpret(R, identity) = R.one$.
background
StrictLogicRealization is a structure supplying a carrier type, a cost type equipped with a zero instance, comparison and composition operations, a distinguished one element, a generator, and two laws: comparison of any element with itself costs zero, and comparison is symmetric. The module derives the free orbit uniformly as LogicNat instead of storing an orbit field internally, as noted in the module documentation: 'a strict realization supplies only native comparison, composition, identity, invariance, and non-triviality data.'
proof idea
One-line wrapper that applies the identity case of the interpret definition, reducing directly to reflexivity.
why it matters
This base case is required for interpret to be well-defined on the free orbit LogicNat inside every strict realization. It is invoked by downstream constructions including boolRealization, natOrderedRealization, modularRealization, and physicsRealization when they embed into the LogicRealization interface. The result supports the initial step of the universal forcing program by fixing how the identity element behaves under interpretation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.