alpha_locked_in_unit
plain-language theorem explainer
The theorem establishes that the ILG modification parameter α = (1 - 1/φ)/2 lies strictly between 0 and 1. Researchers modeling modified gravity at long dynamical times within Recognition Science would cite this to confirm the parameter remains physically admissible. The proof is a one-line term-mode wrapper that directly pairs the positivity lemma with the strict upper-bound lemma for α.
Claim. $0 < α < 1$, where $α = (1 - φ^{-1})/2$ and $φ$ denotes the golden ratio.
background
The RecognitionBandwidth module connects five elements of Recognition Science: the holographic bound on information, the per-bit recognition cost k_R = ln(φ), the ILG parameters C_lag = φ^{-5} and α = (1 - 1/φ)/2 that modify gravity at long dynamical times, the eight-tick cadence completing one cycle per 8τ₀, and the consciousness boundary cost. Recognition bandwidth is defined as the maximum ledger throughput R_max = S_holo / (k_R · 8τ₀) = A / (4ℓ_P² · ln(φ) · 8τ₀), imposing a hard ceiling from the holographic bound and per-bit cost. Upstream, alpha_locked is defined by the expression (1 - 1/phi)/2, with separate lemmas alpha_locked_pos and alpha_locked_lt_one establishing its range.
proof idea
The proof is a term-mode construction that applies the lemma alpha_locked_pos to obtain the left conjunct and the lemma alpha_locked_lt_one to obtain the right conjunct, then packages both into a single pair.
why it matters
This result locks the ILG parameter α inside (0,1) so that the long-time modification to Newtonian dynamics remains consistent with the recognition bandwidth ceiling and the eight-tick octave. It supplies a prerequisite for any downstream use of the ILG modification inside holographic or unification arguments. No open scaffolding remains; the claim is fully discharged by the two upstream lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.