Pith. sign in
module module low

IndisputableMonolith.Mathematics.LogicSystemsFromConfigDim

show as:
view Lean formalization →

The module defines logic systems and their counts derived from configuration dimension in the Recognition Science setting. Researchers constructing discrete logic models from RS parameters would cite these definitions. It is a definition-only module importing Mathlib and Constants with no proofs.

claimLogicSystem and logicSystem_count derived from configuration dimension, together with LogicSystemsCert and logicSystemsCert.

background

The module imports Mathlib and IndisputableMonolith.Constants. The latter supplies the fundamental RS time quantum τ₀ = 1 tick. It introduces the sibling definitions LogicSystem, logicSystem_count, LogicSystemsCert, and logicSystemsCert to formalize logic systems from configuration dimension.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the core definitions for logic systems from configuration dimension that support higher-level constructions in the Recognition Science monolith, including links to the forcing chain and D = 3. No direct parent theorems are listed in the dependency graph.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)