Pith. sign in
module module high

IndisputableMonolith.Physics.TopologicalDefectsFromRS

show as:
view Lean formalization →

The module defines topological defects arising in Recognition Science at D=3 via the relation 4=2^(D-1). Researchers modeling early-universe defect formation or phi-ladder mass spectra would cite these definitions. The module supplies the TopologicalDefect type, its count function, and the supporting four_eq_2pow_Dm1 identity as a definition block that imports only the RS time quantum τ₀.

claimThe module introduces the type $\mathrm{TopologicalDefect}$ and the function $\mathrm{topologicalDefect\_count}$ together with the identity $4=2^{D-1}$ evaluated at $D=3$.

background

The module resides in the Physics domain and imports IndisputableMonolith.Constants, whose sole documented object is the fundamental RS time quantum τ₀=1 tick. It builds directly on the forcing-chain result that fixes D=3 and therefore yields the numerical identity 4=2²=2^(D-1). Sibling declarations supply the defect type, a counting function, and a certificate type that together encode the topological content of the eight-tick octave at three spatial dimensions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the defect vocabulary required by any later derivation that invokes the eight-tick octave or the D=3 step of the unified forcing chain. No downstream declarations are recorded yet, indicating the block is currently a leaf that future physics lemmas will import.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)