pith. sign in
module module high

IndisputableMonolith.Foundation.UniversalForcingAudit

show as:
view Lean formalization →

UniversalForcingAudit aggregates five distinct Law-of-Logic realizations (categorical, discrete, modular, ordered, physics) together with the core UniversalForcing statement. Researchers verifying that initial Peano algebras remain equivalent across carriers cite this module. The module contains only import declarations and no local proofs or definitions.

claimAny two Law-of-Logic realizations $R$ and $S$ induce canonically equivalent initial Peano algebras $N_R$ and $N_S$.

background

The module imports UniversalForcing, whose doc-comment states the first formal version of the theorem: any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects because those objects are initial Peano algebras. It further imports five carrier-specific realizations. CategoricalLogicRealization packages the natural-number object in the initial-Peano-algebra language. DiscreteLogicRealization supplies the first non-continuous Boolean carrier. ModularLogicRealization demonstrates a periodic finite-cyclic carrier whose internal orbit remains free. OrderedLogicRealization supplies an ordered faithful realization. PhysicsLogicRealization provides the stable interface using identity ticks, recognition states, and equality cost.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the cross-realization audit required to apply the Universal Forcing theorem uniformly. It feeds the foundation layer by confirming that the initial-Peano-algebra equivalence holds in every imported carrier without adding new hypotheses or closing any scaffolding.

scope and limits

depends on (6)

Lean names referenced from this declaration's body.