pith. sign in
module module high

IndisputableMonolith.Foundation.UniversalForcingAudit

show as:
view Lean formalization →

UniversalForcingAudit imports the core Universal Forcing theorem together with five distinct Law-of-Logic realizations (discrete Boolean, categorical, modular periodic, ordered, and physics). Researchers formalizing the derivation of arithmetic from logic would cite the module to confirm that the initial-Peano-algebra equivalence holds uniformly across carriers. The module contains only import statements and no internal declarations or proofs.

claimAny two Law-of-Logic realizations yield canonically equivalent forced arithmetic objects, each an initial Peano algebra.

background

The module sits inside the Foundation domain and 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 also imports five realization modules whose doc-comments describe the carriers: DiscreteLogicRealization supplies the first non-continuous Boolean/propositional test case; CategoricalLogicRealization packages the natural-number object in initial-Peano-algebra language; ModularLogicRealization uses a periodic finite-cyclic carrier while keeping the internal orbit free; OrderedLogicRealization supplies an ordered faithful realization; PhysicsLogicRealization gives the stable interface using identity ticks, recognition states, and equality cost.

proof idea

This is a definition module, no proofs. Its structure consists solely of six import statements that activate the Universal Forcing theorem inside each listed realization carrier.

why it matters in Recognition Science

The module audits the Universal Forcing theorem (the parent result declared in UniversalForcing) by exercising it across the five realization modules. It thereby supports the claim that the forced arithmetic objects remain initial Peano algebras independently of the concrete carrier chosen for the Law of Logic.

scope and limits

depends on (6)

Lean names referenced from this declaration's body.