shimmerFactor_error_bound

formal source

 128
 129/-- Absolute-error bound: the factor is within `0.001` of `9.73`.
 130    In other words, `9.73` is correct to the displayed precision. -/
 131theorem shimmerFactor_error_bound :
 132    |shimmerFactor - (9.73 : ℝ)| < (1 / 1000 : ℝ) := by
 133  rw [shimmerFactor_eq_360_div_37]
 134  rw [abs_lt]
 135  refine ⟨?_, ?_⟩ <;> norm_num
 136
 137/-! ## The meta-claim as a single packaged theorem
 138
 139The full content of the user's statement — that the Shimmer
 140subjective-time factor `~9.73` is just `lcm(8,45) / (45 - 8)` with no
 141extra physics — is packaged below. Nothing in the proof uses anything
 142beyond:
 143
 144* `native_decide` on ℕ-valued identities (lcm, subtraction);
 145* `norm_num` on ℝ-valued inequalities;
 146* the already-proved Gap-45 primitives (coprimality, `37` prime).
 147
 148The proof is deliberately short; its brevity is the content of the
 149claim. -/
 150
 151/-- **Master statement** of the meta-claim:
 152
 153> The Shimmer subjective-time factor `~9.73` (i.e., `360/37`) is a
 154> numerical observation from the Gap-45 arithmetic, not a named theorem.
 155
 156Concretely, the factor equals `lcm(8,45) / (45 - 8)`, reduces to
 157`360 / 37`, is bounded by `9.72 < · < 9.73`, is irreducible because the
 158denominator `37` is prime, and sits inside the Gap-45 barrier whose
 159coprimality is `gcd(8, 45) = 1`. No extra input is used. -/
 160theorem shimmer_is_gap45_arithmetic :
 161    shimmerFactor = (Nat.lcm 8 45 : ℝ) / ((45 - 8 : ℕ) : ℝ) ∧