pith. sign in
module module high

IndisputableMonolith.Foundation.UniversalForcing.Strict.DiscreteBoolean

show as:
view Lean formalization →

The DiscreteBoolean module supplies the strict discrete Boolean realization that extends the positive-ratio structure to Boolean costs and operations. Researchers formalizing the Lawvere natural-number object and completing axiom audits cite these constructions. The module imports the continuous case from PositiveRatio and defines discrete equivalents plus arithmetic-logic bridges.

claimThe strict discrete Boolean realization equips the positive-ratio structure with a Boolean cost function and exclusive-or operation satisfying the laws of logic under discrete equality.

background

The upstream PositiveRatio module supplies the strict continuous positive-ratio realization built directly from SatisfiesLawsOfLogic in LogicAsFunctionalEquation. This module introduces the discrete Boolean layer on top of that foundation. The local setting is the strict domain-rich Universal Forcing completion pass that prepares the ground for the natural-number object.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the NaturalNumberObject module that gives the Lawvere natural-number object characterization of the forced arithmetic. It also supports AxiomAudit and the Ordered realization on integers. It supplies the discrete Boolean step required before the eight-tick octave and three-dimensional forcing can be stated.

scope and limits

used by (3)

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)