Verification Dimension

The dimension check

In mathematics, dimension is a count of independent directions: a line has one, a plane has two, a solid has three. The recognition framework, a discrete record of events and their costs, asks whether that count can be derived rather than assumed. The verification dimension is the number D that survives a specific consistency test: a complete cover of a space by patterns of period 2^D, combined with a synchronization target of 360 set by a 45-gap timing rule.

The test is arithmetic. The framework requires that the least common multiple of 2^D and 45 equals 360. For D equals 1, the lcm of 2 and 45 is 90. For D equals 2, the lcm of 4 and 45 is 180. For D equals 3, the lcm of 8 and 45 is exactly 360. For D equals 4, the lcm of 16 and 45 is 720, which overshoots. Only D equals 3 satisfies the equation, and the module proves this in both directions: the condition holds if and only if D is 3.

The module, a machine-checked collection of formal theorems, establishes this as a biconditional. It proves that if the counting and synchronization conditions hold, then the dimension must be three, and conversely that dimension three satisfies both conditions. The proof relies only on facts about least common multiples and the specification layer, so the argument stays light. The coverage premise, that a complete cover with period 2^D exists, ensures the power of two is a real combinatorial period, not an arbitrary number.

In Recognition Science, this is one step in a larger forcing chain: the framework derives the golden ratio, an eight-tick cycle, and then this dimension result. The module itself does not address why three dimensions give interesting linking behavior. That question, about Hopf fibrations and linking costs, remains a scaffolded hypothesis with placeholder definitions, not a proved theorem.

What the module changes is the status of the number three. Within the framework, three is not an observed accident but a forced consequence of the counting and synchronization postulates. A reader can now see the exact arithmetic that eliminates every other dimension, and know precisely which parts of the story are proved and which remain open targets.

/-- Exact characterization: the RSCounting + Gap45 synchronization predicate holds
    if and only if the spatial dimension is three. This upgrades the one‑way
    necessity into a biconditional sufficiency. -/
theorem rs_counting_gap45_absolute_iff_dim3 {D : Nat} :
  RSCounting_Gap45_Absolute D ↔ D = 3 := by
  constructor
  · intro h; exact onlyD3_satisfies_RSCounting_Gap45_Absolute h
  · intro hD
    cases hD
    constructor
    · exact IndisputableMonolith.Patterns.cover_exact_pow 3
    · -- lcm(2^3,45)=360
      simpa using (IndisputableMonolith.RecogSpec.lcm_pow2_45_eq_iff 3).mpr rfl

/-- If both hypercube coverage at 2^D and 45-gap synchronization at 360 hold,
    then the spatial dimension must be D=3. -/
theorem dimension_is_three {D : Nat} (h : DimensionalRigidityWitness D) : D = 3 := by
  rcases h with ⟨hcov, hsync⟩
  -- Coverage not used quantitatively here; the synchronization equation pins D=3.
  -- A stronger version may link coverage/causality structure into uniqueness of the sync.
  simpa using (IndisputableMonolith.RecogSpec.lcm_pow2_45_eq_iff D).mp hsync

/-- Strong dimension‑3 necessity from independent witnesses: the existence of a
    complete cover with period `2^D` together with the synchronization identity
    `lcm(2^D,45)=360` forces `D=3`. The coverage premise ensures `2^D` is the
    actual combinatorial period of the cover, not merely an arithmetic placeholder. -/
theorem dimension_three_of_cover_and_sync {D : Nat}
  (hcov : ∃ w : IndisputableMonolith.Patterns.CompleteCover D, w.period = 2 ^ D)
  (hsync : Nat.lcm (2 ^ D) 45 = 360) : D = 3 := by
  simpa using (IndisputableMonolith.RecogSpec.lcm_pow2_45_eq_iff D).mp hsync

What this page does not claim

The module does not prove that three dimensions are unique in having non-trivial linking structure. The golden ratio penalty is defined but its derivation from the cost function is not proved in this module. The physical bridge from recognition events to spatial dimensions is not established here.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/Dimension.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: