pith. sign in
module module high

IndisputableMonolith.Unification.ConstantsPredictionsProved

show as:
view Lean formalization →

This module collects proved predictions for RS constants, centering on positivity and bounds for the fine-structure constant α. Researchers deriving constants from the phi-forcing chain without free parameters would cite these results. The module assembles direct applications of imported lemmas on gap weights and self-similar forcing.

claimThe fine-structure constant satisfies $0 < α < 0.1$ together with the positivity claim $α > 0$, both derived from the gap term $f_{gap} = w_8 · ln(φ)$ and the forced value of $φ$.

background

The module sits inside the unification domain and imports the RS time quantum τ₀ = 1 tick. PhiForcing establishes that φ arises as the self-similar fixed point of a discrete ledger equipped with J-cost. GapWeight supplies the closed-form, parameter-free projection weight w₈ used in the single gap term f_gap = w₈ · ln(φ) that enters the α pipeline.

proof idea

The module contains a collection of short theorems. Each is a direct one-line wrapper that applies the relevant lemma from Constants.Alpha or GapWeight after the phi-forcing results have fixed φ and w₈.

why it matters in Recognition Science

The module supplies the calculated α > 0 and α bounds that close the alpha pipeline inside the unification framework. It thereby supports the broader claim that all constants emerge from the T5–T8 forcing chain and the Recognition Composition Law without adjustable parameters.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (16)