Relativity Ilg Ppn

The PPN scaffold

The parameterized post-Newtonian (PPN) formalism is the standard way to compare metric theories of gravity against solar-system experiments. It expands the spacetime metric in powers of the gravitational potential and assigns coefficients, the most famous being γ (gamma) and β (beta). In general relativity, both equal 1 at leading order. The framework's module, PPN, builds a scaffold for these definitions inside its own structure.

In Recognition Science, the module defines γ and β as constants equal to 1. This is a definitional choice, not a derived result. It also provides a linearized model where the parameters shift by terms proportional to a small scalar coupling, written as 1 + (1/10)·C_lag·α for γ and 1 + (1/20)·C_lag·α for β. These are illustrative forms for a paper reference, not forced predictions.

The module proves two theorems about these linearized parameters. If the absolute value of the coupling product |C_lag·α| is bounded by some small number κ, then |γ − 1| is bounded by (1/10)·κ, and |β − 1| is bounded by (1/20)·κ. These are simple consequences of the definitions, proved in the machine-checked library of formal theorems. They show how the framework can produce explicit error bounds that scale with the coupling strength.

The framework also includes an illustrative solar-system bound: for the constant parameters, |γ − 1| ≤ 1/100000 and |β − 1| ≤ 1/100000. This matches the order of magnitude of current experimental constraints, though the module labels it illustrative. The practical upshot is that the framework's PPN scaffold is compatible with general relativity at leading order, and it provides a template for expressing deviations when a more complete theory is developed.

/-- Minimal PPN scaffold: define γ, β to be 1 at leading order (GR limit). -/
noncomputable def gamma (_C_lag _α : ℝ) : ℝ := 1

noncomputable def beta  (_C_lag _α : ℝ) : ℝ := 1

/-- Bound: if |C_lag·α| ≤ κ then |γ−1| ≤ (1/10) κ. -/
theorem gamma_bound_small (C_lag α κ : ℝ)
  (h : |C_lag * α| ≤ κ) :
  |gamma_lin C_lag α - 1| ≤ (1/10 : ℝ) * κ := by
  unfold gamma_lin
  simp only [add_sub_cancel_left]
  rw [abs_mul]
  calc |1/10| * |C_lag * α| = (1/10) * |C_lag * α| := by norm_num
    _ ≤ (1/10) * κ := by exact mul_le_mul_of_nonneg_left h (by norm_num)

/-- Bound: if |C_lag·α| ≤ κ then |β−1| ≤ (1/20) κ. -/
theorem beta_bound_small (C_lag α κ : ℝ)
  (h : |C_lag * α| ≤ κ) :
  |beta_lin C_lag α - 1| ≤ (1/20 : ℝ) * κ := by
  unfold beta_lin
  simp only [add_sub_cancel_left]
  rw [abs_mul]
  calc |1/20| * |C_lag * α| = (1/20) * |C_lag * α| := by norm_num
    _ ≤ (1/20) * κ := by exact mul_le_mul_of_nonneg_left h (by norm_num)

/-- Solar‑System style bound (illustrative): |γ−1| ≤ 1/100000. -/
theorem gamma_bound (C_lag α : ℝ) :
  |gamma C_lag α - 1| ≤ (1/100000 : ℝ) := by
  -- LHS simplifies to 0; RHS is positive
  simpa [gamma] using (by norm_num : (0 : ℝ) ≤ (1/100000 : ℝ))

/-- Solar‑System style bound (illustrative): |β−1| ≤ 1/100000. -/
theorem beta_bound (C_lag α : ℝ) :
  |beta C_lag α - 1| ≤ (1/100000 : ℝ) := by
  simpa [beta] using (by norm_num : (0 : ℝ) ≤ (1/100000 : ℝ))

What this page does not claim

The PPN parameters are derived from the framework's forcing chain. The linearized model represents a physical theory with measured consequences. The illustrative bound is a prediction of the framework.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Relativity/ILG/PPN.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: