IndisputableMonolith.Relativity.GRLimit.ParametersTest
Test module for the GR-limit parameter bundle used when Recognition Science recovers classical general relativity. It exercises the parameter record from Relativity.GRLimit.Parameters (units, coupling scales, and limit flags) against Mathlib arithmetic. Cite it when auditing that the GR-limit knobs are well-formed before they enter continuum or post-Newtonian arguments. Structure is executable checks, not a theorem proof.
claimSanity and well-formedness checks on the GR-limit parameter record: dimensionless couplings, unit conventions ($c=1$, RS-native $G$ and $\hbar$), and flags that control the classical limit of the Recognition gravity sector.
background
In Recognition Science, continuum GR is recovered as a limit of a discrete recognition dynamics on the $\phi$-ladder, with RS-native constants $c=1$, $\hbar=\phi^{-5}$, and $G=\phi^5/\pi$. The parent module Relativity.GRLimit.Parameters packages the knobs of that limit (couplings, scales, and regime flags) into a single record consumed by continuum and post-Newtonian developments.
This file sits under Relativity.GRLimit and imports only Mathlib plus that Parameters module. It is the executable companion that checks the parameter bundle is numerically and algebraically coherent before downstream GR-limit theorems rely on it. No new physics definitions are introduced here; the setting is regression and interface validation for the GR-limit layer.
proof idea
This is a test module, not a theorem development. It loads the GR-limit parameter definitions and runs concrete Mathlib-backed checks (equalities, bounds, and flag consistency) on the record fields. There is no forcing-chain argument and no tactic proof of a physical claim; failures surface as broken tests rather than unfinished proofs.
why it matters in Recognition Science
The GR-limit stack needs a stable parameter interface so continuum recovery, Newtonian limits, and post-Newtonian expansions share one set of units and couplings. This module guards that interface. It does not itself prove the GR limit; it feeds confidence that Parameters is safe to import into those parent arguments. In the broader RS picture it sits downstream of the forcing landmarks that fix $D=3$ and the $\phi$-scaled constants, and upstream of any theorem that specializes gravity to the classical regime.
scope and limits
- Does not prove recovery of Einstein equations or any GR field equation.
- Does not derive $G$, $\hbar$, or $\phi$ from the forcing chain.
- Does not define new physical parameters beyond testing Parameters.
- Does not substitute for continuum or post-Newtonian theorems that consume the record.