Recog Spec Bands

Recognition bands

A recognition band, in the Recognition Science framework, is a tolerance window: a pair of real numbers, a lower bound and an upper bound, that marks an interval on a number line. The framework uses these bands to test whether a computed value falls within an acceptable range of a target. A band is valid when its lower bound does not exceed its upper bound, so it describes a nonempty interval. The width of a band is simply the difference between its upper and lower bounds.

The central object here is the wide band, built around a center point x with a tolerance ε. It is the interval from x − ε to x + ε. The module proves, as a machine-checked theorem, that a wide band with nonnegative tolerance always contains its own center. This is not a deep result, but it is the load-bearing sanity check for everything that follows: a tolerance window that did not contain its own target would be useless. The same theorem also shows the band is valid and has width 2ε, and that its endpoints lie inside it.

On top of this, the module defines a checker that tests whether a list of sampled values meets any of a list of candidate bands. The checker returns false on empty input, whether the list of values or the list of bands is empty. A separate lemma shows that the centered wide band around a constant c always satisfies the check for that constant, and that this check is invariant under rescaling of units, meaning the framework's unit choices do not affect whether a value lands in a band.

In Recognition Science, the module also contains one arithmetic hinge for a dimension-forcing argument. It proves that the least common multiple of 2^D and 45 equals 360 if and only if D = 3. This is the kernel of a claim that links the framework's eight-tick cycle to three spatial dimensions, though the physical bridge from recognition to linking is itself an open target.

lemma wideBand_contains_center {x ε : ℝ} (hε : 0 ≤ ε) :
  Band.contains (wideBand x ε) x := by
  dsimp [Band.contains, wideBand]
  constructor
  · have : x - ε ≤ x := by simpa using sub_le_self x hε
    simpa using this
  ·
    have hx : x ≤ x + ε := by
      simpa using (le_add_of_nonneg_right hε : x ≤ x + ε)
    simpa using hx

/-- The LCM of 2^D and 45 equals 360 if and only if D = 3.
    This is the arithmetic kernel of the "8↔45 hinge" dimension forcing argument. -/
theorem lcm_pow2_45_eq_iff (D : ℕ) : Nat.lcm (2 ^ D) 45 = 360 ↔ D = 3 := by
  constructor
  · intro h
    -- gcd(2^D, 45) = 1 for all D since 45 = 3² × 5 has no factors of 2
    -- Thus lcm(2^D, 45) = 2^D × 45
    -- 2^D × 45 = 360 ⟺ 2^D = 8 ⟺ D = 3
    have hgcd : Nat.gcd (2 ^ D) 45 = 1 := by
      have hcop : Nat.Coprime 2 45 := by decide
      exact Nat.Coprime.pow_left D hcop
    have hlcm : Nat.lcm (2 ^ D) 45 = 2 ^ D * 45 / Nat.gcd (2 ^ D) 45 := Nat.lcm_eq_mul_div (2 ^ D) 45
    rw [hgcd, Nat.div_one] at hlcm
    rw [hlcm] at h
    have h8eq : 2 ^ D = 8 := by omega
    have : 2 ^ D = 2 ^ 3 := by simp at h8eq ⊢; exact h8eq
    exact Nat.pow_right_injective (by norm_num : 1 < 2) this
  · intro hD
    subst hD
    decide

/-- The centered `wideBand` around `U.c` always includes `U.c`. -/
lemma evalToBands_c_wideBand_center
  (U : IndisputableMonolith.Constants.RSUnits) (tol : ℝ) (htol : 0 ≤ tol) :
  evalToBands_c U [wideBand U.c tol] := by
  refine ⟨wideBand U.c tol, by simp, ?_⟩
  simpa using wideBand_contains_center (x:=U.c) (ε:=tol) htol

What this page does not claim

This module does not prove that three spatial dimensions physically exist. This module does not derive any specific physical constant from the band structure. The lcm theorem alone does not force the eight-tick cycle or any other framework structure.

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/RecogSpec/Bands.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: