FaithfulArithmeticInterpretation
plain-language theorem explainer
FaithfulArithmeticInterpretation packages the requirement that a LogicRealization R maps its forced orbit injectively into the carrier while keeping the zero element distinct from every first step. Workers verifying concrete embeddings of logic-derived arithmetic into physical or ordered carriers cite this property to certify non-degenerate realizations. The declaration is a bare structure definition that directly encodes the two fields with no proof body or lemmas.
Claim. A LogicRealization $R$ satisfies faithful arithmetic interpretation when the interpretation map from its orbit to its carrier is injective and $R.interpret(R.orbitZero) ≠ R.interpret(R.orbitStep(n))$ holds for every orbit element $n$.
background
LogicRealization supplies the common interface: a Carrier type, a Cost type equipped with zero, a compare operation, a zero element, a step generator, and an Orbit type with distinguished orbitZero and orbitStep. The module creates a setting-independent object so that continuous positive-ratio, discrete, and categorical realizations of the Law of Logic can be mapped uniformly into the same arithmetic extraction target. Upstream, LogicNat is the inductive type whose constructors identity and step generate the free orbit, while StrictRealization.interpret recurses over this orbit to produce the corresponding carrier element via the realization's generator and composition.
proof idea
This declaration is a structure definition with an empty proof body. It directly declares the two fields injective and zero_step_noncollapse without applying any lemmas or tactics.
why it matters
The definition supplies the faithfulness criterion invoked by positiveRatio_faithful, ordered_faithful, and physics_faithful to certify that their respective realizations embed the forced arithmetic without collapse. It fills the structural requirement inside the Universal Forcing program so that the extracted arithmetic object remains distinguishable in the ambient carrier, which is a prerequisite for non-periodic physical models. It touches the open distinction between free-orbit realizations and periodic carriers that still satisfy the local laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.