Pith. sign in
module module high

IndisputableMonolith.Foundation.OrderedLogicRealization

show as:
view Lean formalization →

OrderedLogicRealization supplies the equality-cost model on the naturals for the Universal Forcing program. Downstream physics and audit modules cite it when they need a minimal ordered realization that preserves arithmetic invariants. The module imports the modular base and adds Nat-specific cost definitions together with their elementary symmetry and faithfulness properties.

claimAn ordered logic realization on the naturals equipped with equality cost $c:\mathbb{N}\times\mathbb{N}\to\mathbb{R}$ (vanishing precisely on equal pairs) together with the arithmetic invariant and faithful interpretation lemmas.

background

The module imports ModularLogicRealization, whose doc states: 'Periodic finite-cyclic realization for Universal Forcing. The internal orbit is still free (LogicNat), while the carrier interpretation is periodic. This demonstrates that Universal Forcing does not require every realization to embed arithmetic faithfully into the carrier.' OrderedLogicRealization extends that setting by specializing the cost to equality on Nat, thereby supplying the ordered arithmetic needed for tick counting.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds PhysicsLogicRealization (lightweight hook using identity ticks, recognition states, and equality cost as minimal physical tick arithmetic) and UniversalForcingAudit (reproducible audit surface). It supplies the ordered Nat realization required by the foundation layer of the forcing chain (T0-T8) without imposing periodic carrier embedding.

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)