pith. sign in
module module high

IndisputableMonolith.Foundation.OrderedLogicRealization

show as:
view Lean formalization →

The module supplies an equality cost function on natural numbers to realize ordered logic in the Universal Forcing setup. It would be referenced when constructing lightweight physics realizations that use identity ticks and recognition states. The content consists of definitions for the cost function together with lemmas on its symmetry and ordered invariance, extending the periodic carrier approach without faithful arithmetic embedding.

claimEquality cost function $c(m, n)$ on natural numbers satisfying $c(n, n) = 0$, symmetry $c(m, n) = c(n, m)$, and ordered arithmetic invariance, providing a minimal realization of physical tick arithmetic in the periodic finite-cyclic setting.

background

The theoretical setting is the foundation for Universal Forcing, where realizations of logic need not embed arithmetic faithfully into the carrier. This module imports the modular logic realization, which features a free internal orbit (LogicNat) and periodic carrier interpretation. It introduces the equality cost on Nat as the minimal cost function, along with ordered realization and invariants for arithmetic and faithfulness properties. Upstream documentation notes that this demonstrates Universal Forcing does not require every realization to embed arithmetic faithfully into the carrier.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the equality cost realization that serves as the stable interface for physical tick arithmetic in the PhysicsLogicRealization module. It also supports the reproducible audit in UniversalForcingAudit. By defining the equality cost on Nat, it fills the minimal realization step in the Universal Forcing program, allowing identity ticks and recognition states without full arithmetic faithfulness.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)