Constants Alpha Higher Order Half Period Dim Eq

The half-period dimension

The declaration half_period_dim_eq is a result in the machine-checked library of formal theorems used by Recognition Science. It states that a certain counting number, called the half-period dimension, equals 5. That number is defined as the measure dimension, which is itself defined as the sum 3 + 1 + 1. The result is proved by direct computation, since the definition fixes the value.

The half-period dimension appears in a specific context: the framework's attempt to construct the fine-structure constant α⁻¹. The construction starts from a geometric seed, 4π × 11 ≈ 138.230, then applies a gap weight and a curvature correction to land near the measured value. The half-period dimension of 5 enters through the integration measure over Z₂ sectors, where the number of sectors is 2⁵ = 32. This is a combinatorial bookkeeping detail inside the correction series, not a statement about physical space.

In Recognition Science, the framework models reality as maintaining a discrete record of recognition events, and the cost of recognition is forced by five plain conditions. Within that framework, the half-period dimension is part of the higher-order voxel-seam corrections to the α⁻¹ construction. The result establishes that the dimension of this correction space is five, nothing more.

What the result does not claim is important. It does not claim that physical spacetime has five dimensions; the framework's three spatial dimensions come from a separate forcing chain. It does not claim that the fine-structure constant is derived; the seed identification remains open, and the convergence of the correction series to the CODATA value is a hypothesis, not a theorem. The result only pins down an internal counting number used in a formal construction.

theorem half_period_dim_eq : half_period_dim = 5 := rfl

theorem half_period_dim_eq : half_period_dim = 5 := rfl

/-- Geometric seed: 4π × passive_edges. -/
def alpha_seed : ℝ := 4 * π * passive_edges

What this page does not claim

Physical spacetime has five dimensions. The fine-structure constant is derived from first principles. The correction series converges to the CODATA value.

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/Constants/AlphaHigherOrder.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: