Pith. sign in
module module moderate

IndisputableMonolith.Physics.StringCompactificationFromRS

show as:
view Lean formalization →

The module establishes that Recognition Science yields string compactification with precisely six internal dimensions through the arithmetic relation 10 total minus 4 observable. String theorists and RS unification researchers would cite the family definitions and certification lemmas when connecting the frameworks. The module proceeds by introducing compactification families, count identities, and a certification object that encodes the dimension subtraction.

claimIn Recognition Science, string compactification satisfies $10-4=6$ internal dimensions, formalized by the type CompactificationFamily, the lemma ten_minus_four, the equality six_eq_rank_sum, and the certificate StringCompactificationCert.

background

The module sits in the Physics domain and imports IndisputableMonolith.Constants, whose doc-comment defines the fundamental RS time quantum as τ₀ = 1 tick. It introduces the sibling declarations CompactificationFamily (parameterizing families of compactifications), compactFamily_count, ten_minus_four, six_eq_rank_sum, and StringCompactificationCert (the certification object). These build on the upstream forcing-chain results T7 (eight-tick octave) and T8 (D = 3 spatial dimensions) already established in the monolith.

proof idea

This is a definition module, no proofs. The argument is carried by the sequence of sibling definitions and direct algebraic identities that encode the 10-4-6 relation.

why it matters in Recognition Science

The module supplies the explicit dimension count for string compactification inside the Recognition Science framework, directly realizing the doc-comment claim that 10 - 4 = 6 internal dimensions. It supplies the necessary interface objects for any downstream unification or higher-dimensional physics results that would depend on this count.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)