mk'
The mk' definition constructs a closed interval with rational endpoints lo and hi whenever a proof of lo ≤ hi is supplied. Researchers building verified numerical enclosures for Recognition Science computations cite it to establish exact bounds on real quantities. The implementation is a direct structure constructor that assigns the inputs to the corresponding fields of the Interval type.
claimGiven rational numbers $a$ and $b$ together with a proof $h$ that $a ≤ b$, the constructor yields the closed interval whose lower endpoint is $a$ and upper endpoint is $b$.
background
The module supplies verified interval arithmetic that uses exact rational endpoints to enclose real values of transcendental functions. Its central object is the Interval structure: a pair of rationals lo and hi equipped with a proof that lo ≤ hi. The supplied upstream structures (nuclear densities, J-cost factorization, spectral emergence, and physics complexity) depend on such enclosures to maintain rigorous bounds when deriving physical quantities from the Recognition Science forcing chain.
proof idea
The definition is a one-line wrapper that applies the Interval structure constructor, setting the lo field to the supplied lower bound, the hi field to the upper bound, and the valid field to the inequality hypothesis.
why it matters in Recognition Science
This constructor is invoked by the integer and rational constructors in IntegersFromLogic.mk and RationalsFromLogic.mk, supplying the numerical substrate for the Recognition Science framework. It enables exact rational bounds required for phi-ladder mass formulas, eight-tick octave dynamics, and alpha-band constant derivations. The module thereby closes a scaffolding gap between abstract forcing theorems and concrete numerical verification.
scope and limits
- Does not accept irrational or real endpoints.
- Does not implement interval multiplication or division.
- Does not certify containment of specific physical constants without further lemmas.
- Does not handle open or half-open intervals.
formal statement (Lean)
38def mk' (lo hi : ℚ) (h : lo ≤ hi := by decide) : Interval where
proof body
Definition body.
39 lo := lo
40 hi := hi
41 valid := h
42
43/-! ## Interval Arithmetic Operations -/
44
45/-- Addition of intervals: [a,b] + [c,d] = [a+c, b+d] -/