pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Numerics.Interval.GalacticBounds

show as:
view Lean formalization →

GalacticBounds supplies verified interval bounds for the galactic-to-fundamental time ratio τ★/τ₀ ≈ 5.75e29. Researchers modeling large-scale RS phenomena cite these bounds to anchor galactic timescales to the base tick without floating-point error. The module constructs the bounds by composing interval arithmetic from Basic with power operations from Pow on phi-powered expressions.

claim$τ^★ / τ_0 ∈ I$ where $I$ is a rational-endpoint interval obtained from interval exponentiation of $φ$ and centered near $5.75 × 10^{29}$.

background

Recognition Science fixes the fundamental time quantum τ₀ = 1 tick in the Constants module. The Basic module supplies verified interval arithmetic that encloses real values using exact rational endpoints. The Pow module extends this to power functions via the identity $x^y = exp(y · log x)$ for positive $x$, delivering rigorous bounds when both base and exponent lie in intervals.

proof idea

This is a definition module, no proofs. It declares named interval objects such as galactic_ratio_rational and supporting phi_pow intervals by direct composition of the imported interval constructors and power functions.

why it matters in Recognition Science

The module anchors galactic-scale numerics inside the Recognition framework, supplying bounds that connect the phi-ladder to observable time ratios. It supports downstream verification of large-scale consistency with the eight-tick octave and mass-ladder formulas while preserving exact rational enclosure.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (26)