pith. machine review for the scientific record. sign in
def definition def or abbrev high

gamma

show as:
view Lean formalization →

The PPN gamma parameter is fixed to the constant 1 for arbitrary lag and alpha inputs, supplying the general-relativity limit inside the parametrized post-Newtonian scaffold. Workers constructing leading-order expansions in modified-gravity or Recognition-Science models cite this definition when anchoring to the GR case. The implementation is a direct constant assignment that discards both real arguments.

claimIn the parametrized post-Newtonian formalism the parameter satisfies $gamma(C_{lag}, alpha) := 1$, matching the general-relativity value at leading order.

background

The ILG.PPN module constructs potential-based PPN definitions by deriving the gravitational potentials Phi and Psi from the metric perturbation psi together with auxiliary parameters. This supplies the standard PPN parameters gamma and beta as a minimal scaffold. Upstream results include the Euler-Mascheroni constant defined as the limit of H_n minus ln n and a network-science gamma fixed at 3 for power-law degree distributions; the present gamma reuses the identifier for the PPN context.

proof idea

The definition is a direct constant assignment returning 1 and ignoring its two real parameters.

why it matters in Recognition Science

This definition anchors the GR-limit value of the PPN gamma parameter and is referenced by forty downstream declarations, among them phi_fifth_in_alpha_band (placing phi^5 inside the alpha EEG band) and the family of crystal-symmetry constraints. It occupies the leading-order slot in the PPN scaffold, consistent with the eight-tick octave and phi-ladder structures of the Recognition framework. It leaves open the derivation of gamma from the J-cost functional or the Recognition Composition Law.

scope and limits

formal statement (Lean)

  14noncomputable def gamma (_C_lag _α : ℝ) : ℝ := 1

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.