IndisputableMonolith.Foundation.DiscreteLogicRealization
This module supplies the Boolean realization of the Law-of-Logic inside the Universal Forcing program. It defines a comparison cost that vanishes on equality and equals one on distinction, plus the supporting orbit and invariance objects. Workers on initial Peano algebras cite it to obtain an explicit propositional model. The module consists of definitions and short lemmas rather than a single theorem.
claimThe Boolean realization carries the cost function $\mathrm{boolCost}(x,y)=0$ when $x=y$ and $1$ otherwise, the orbit map $\mathrm{boolOrbitInterpret}$, and the full structure $\mathrm{boolRealization}$ together with its arithmetic invariants.
background
The module imports UniversalForcing, whose doc-comment states that any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects because those objects are initial Peano algebras.
It introduces the Boolean comparison cost boolCost (zero on equality, one on distinction) and the lemmas boolCost_self, boolCost_symm, bool_arithmetic_invariant, and bool_peano_surface. These sit alongside boolRealization and boolOrbitInterpret.
The setting is the discrete propositional model required by the forcing construction; no continuous or modular carriers appear here.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module feeds the concrete Boolean model into CategoricalLogicRealization, ModularLogicRealization, UniversalForcingAudit, and UniversalForcing.DiscreteRealization. It supplies the propositional instance needed to instantiate the initial-Peano-algebra argument of the Universal Forcing theorem in a finite setting.
scope and limits
- Does not prove the Universal Forcing theorem itself.
- Does not treat continuous or modular realizations.
- Does not derive physical constants or the phi-ladder.
- Does not address the eight-tick octave or spatial dimensions.