IndisputableMonolith.Meta.ConstructiveNote
The ConstructiveNote module records the standard definition of a computable real number for use inside Recognition Science. Researchers establishing algorithmic access to constants such as pi and phi would cite it as the base notion. The module contains only this definitional note, imports Mathlib and the Constants module, and carries no proofs or further structure.
claimA real number $x$ is computable if there exists an algorithm that, given any natural number $n$, outputs a rational $q$ satisfying $|x - q| < 2^{-n}$.
background
The module resides in the Meta domain and rests on the RS time quantum defined in IndisputableMonolith.Constants, where the fundamental tick satisfies τ₀ = 1. It supplies the classical notion of computable reals so that later declarations can assert effective approximations to RS-native quantities without leaving the constructive setting. This choice keeps all subsequent results on the phi-ladder and forcing chain explicitly algorithmic.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the interface used by sibling declarations that establish computability of specific constants. It thereby anchors the constructive layer that supports explicit verification throughout the Recognition Science framework.
depends on (1)
declarations in this module (15)
-
class
Computable -
theorem
pi_computable -
theorem
phi_computable -
lemma
two_zpow_pos -
instance
rational_computable -
theorem
computable_neg -
theorem
computable_add -
theorem
computable_sub -
theorem
computable_mul -
theorem
computable_div -
theorem
computable_pow -
theorem
computable_log -
theorem
alpha_seed_computable -
theorem
log_phi_computable -
theorem
curvature_computable