Phys
plain-language theorem explainer
The declaration defines the structure Phys holding a single real field G for the gravitational constant in ILG calculations. Workers on the pressure-form equivalence in the ILG scaffold cite it to parameterize the source term without altering the underlying physics. The definition is a direct structure declaration deriving Repr, with no further computation or lemmas.
Claim. Let $G$ denote the gravitational constant. The structure Phys consists of the single field $G : ℝ$.
background
The ILG.PressureForm module presents the ILG effective source as an algebraic pressure display scaffold, rewriting the source term via the auxiliary variable $p := ρ · w(k,a) · δ$ while leaving the physics invariant. The structure Phys supplies the gravitational constant $G$ that multiplies the kernel-weighted density term. Upstream, $G$ is supplied in two forms: the RS-native expression $G = λ_{rec}^2 c^3 / (π ℏ)$ and the CODATA numerical value; the ILG kernel itself is $w(k,a) = 1 + C · (a / (k τ_0))^α$ (with a safeguard max).
proof idea
This is a structure definition that directly declares the field G : ℝ together with a Repr instance. No lemmas or tactics are invoked; the declaration functions as a typed container for the constant later passed to effectiveSource and effectiveSource_pressure.
why it matters
Phys supplies the gravitational constant to the downstream definitions effectiveSource, effectiveSource_pressure and the equivalence theorem source_equiv, which together realize the pressure-display rewrite. It anchors the ILG scaffold inside the Recognition Science forcing chain (T0–T8) where G appears as the derived constant $G = φ^5 / π$ in native units. The structure also feeds the discrete-bridge metric invertibility check, keeping the Regge-calculus limit hypothesis visible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.