Pith. sign in
module module moderate

IndisputableMonolith.Verification.Dimension

show as:
view Lean formalization →

Verification module that packages dimensional rigidity for Recognition Science: a complete cover of period 2^D together with 45-gap synchronization via lcm(2^D,45)=360. Anyone citing T8 (D=3) or the absolute RS-counting gap-45 criterion lands here. Sibling theorems show the conjunction holds iff D=3, with linking hypotheses ruling out D=2 and D=4. Structure is witness plus iff and uniqueness lemmas, not a single deep proof.

claimDimensional rigidity witness: there exists a complete cover of period $2^D$, and the 45-gap synchronization target satisfies $\mathrm{lcm}(2^D,45)=360$. The module proves this absolute RS-counting condition holds if and only if $D=3$, with hypotheses that $D=2$ admits no linking and $D=4$ only trivial linking, so unique nontrivial Hopf linking occurs in three dimensions.

background

Recognition Science forces spatial dimension through discrete cover periods and synchronization. A complete cover has period $2^D$; the T7 landmark (eight-tick octave) is the case $D=3$, period $8$. Separately, a 45-gap synchronization target asks that $\mathrm{lcm}(2^D,45)$ equal $360$, tying the cover clock to a full-turn angular budget.

This module lives in Verification. It imports pattern machinery (covers, ticks) and the RecogSpec layer. The doc-comment states the witness enforces both cover existence and the lcm condition. Siblings include DimensionalRigidityWitness, absolute gap-45 predicates, dimension_is_three, and linking hypotheses: no linking in $D=2$, trivial linking in $D=4$, and uniqueness of three-dimensional Hopf linking. The golden ratio $\varphi$ appears as the T6 self-similar fixed point inside hopf-linking penalty scores.

proof idea

Definition-and-witness module, not one monolithic proof. A rigidity witness bundles (i) existence of a complete cover of period $2^D$ and (ii) absolute 45-gap sync $\mathrm{lcm}(2^D,45)=360$. Theorems then prove the conjunction is equivalent to $D=3$, and that only $D=3$ satisfies the absolute RS-counting gap-45 criterion. Side hypotheses encode dimensional linking failures ($D=2$ none, $D=4$ trivial); a uniqueness statement isolates three-dimensional Hopf linking. Supporting facts record $\varphi$ as fixed point and a hopf-linking penalty used to score candidates.

why it matters in Recognition Science

Closes the T8 step of the forcing chain: spatial dimension is three. That lock fixes the T7 eight-tick octave at period $8$ and supplies the ambient $D=3$ geometry assumed by mass ladders, Berry thresholds, and later constant derivations. Downstream readers of dimension-is-three and the only-$D=3$ gap-45 theorems depend on this package even though the module graph lists no further used-by edges yet. The absolute counting bridge from $2^D$ to the $360$ sync target is the discrete reason angular structure and cover period must cohere only in three dimensions.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)