Numerics Interval Pow Two Pow Neg22 In Interval

A tiny number, boxed

The number 2 raised to the power -22 is about 2.384 times 10 to the minus 7, a value so small it appears in physics as a scale for quantum effects. The declaration two_pow_neg22_in_interval states that this exact real number lies inside the interval from 2.38e-7 to 2.39e-7. The interval is defined with rational endpoints, and the theorem is checked by the machine-checked library of formal theorems, meaning the containment is a proved statement, not an approximation or a numerical guess.

The proof works by direct computation. The library defines the interval with lower bound 238/1000000000 and upper bound 239/1000000000, then verifies that the real number 2^(-22) falls between them. This is a simple, exact containment result. It does not rely on the logarithmic identity used for general power functions; it uses the natural-number exponent case directly, which is more precise.

In Recognition Science, this declaration is a building block. The framework derives physical constants from a forcing chain, and interval arithmetic provides rigorous bounds for values like powers of the golden ratio. The theorem two_pow_neg22_in_interval is one such bound, though it concerns the number 2, not the golden ratio. It establishes a numerical fact that could support later calculations, but it does not itself connect to the forcing chain or to any physical constant.

The declaration does not claim that 2^(-22) equals any particular decimal value, only that it lies within the stated interval. It does not assert that this interval is the tightest possible, nor that the number has any special significance in the framework. It is a precise, isolated numerical containment, useful as a tool but carrying no broader theoretical weight by itself.

/-- 2^(-22) is in the interval - PROVEN -/
theorem two_pow_neg22_in_interval : two_pow_neg22_interval.contains ((2 : ℝ) ^ (-22 : ℤ)) := by
  simp only [Interval.contains, two_pow_neg22_interval]
  -- 2^(-22) = 1/2^22 = 1/4194304
  have h : (2 : ℝ) ^ (-22 : ℤ) = 1 / 4194304 := by
    have h2 : (2 : ℝ) ^ (22 : ℤ) = 4194304 := by norm_num
    have h3 : (2 : ℝ) ^ (-22 : ℤ) = ((2 : ℝ) ^ (22 : ℤ))⁻¹ := by
      rw [zpow_neg]
    rw [h3, h2]
    norm_num
  rw [h]
  constructor
  · -- 238/1000000000 ≤ 1/4194304
    -- 238 * 4194304 ≤ 1000000000
    -- 998223552 ≤ 1000000000 ✓
    norm_num
  · -- 1/4194304 ≤ 239/1000000000
    -- 1000000000 ≤ 239 * 4194304
    -- 1000000000 ≤ 1002438656 ✓
    norm_num

/-- 2^(-22) = 1/4194304 ≈ 2.384e-7 -/
def two_pow_neg22_interval : Interval where
  lo := 238 / 1000000000  -- 2.38e-7
  hi := 239 / 1000000000  -- 2.39e-7
  valid := by norm_num

What this page does not claim

The declaration does not assert that 2^(-22) equals any specific decimal value. It does not claim the interval is the narrowest possible. It does not connect 2^(-22) to any physical constant or framework derivation.

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/Numerics/Interval/Pow.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: