Relativity Ilg Ppnderive

A small certificate for PPN parameters

Post-Newtonian (PN) theory is the standard toolkit for describing how gravity behaves when objects move slowly compared to light and fields are weak. Instead of solving Einstein's field equations exactly, physicists expand them in powers of a small velocity parameter. The two leading correction terms that appear in this expansion are the PPN parameters gamma and beta. In general relativity, both equal exactly 1. Their measured values, if they ever differed from 1, would signal a departure from Einstein's theory.

The Recognition Science framework's ledger, a discrete record of recognition events that the framework uses as its foundational picture, includes its own layer for relativity. Within that layer, a file called PPNDerive.lean addresses a specific housekeeping problem: an earlier stub had simply declared that the PPN derivation holds, with no actual proof. The file replaces that empty claim with a small, honest certificate. It defines two toy extraction formulas that take a coupling constant alpha and a Lagrangian coefficient C_lag, and map them to gamma and beta. The formulas are deliberately simple: gamma is 1 plus one tenth of the product alpha times C_lag, and beta is 1 plus one twentieth of that same product.

The module then states and proves a theorem, tagged as a THEOREM in the framework's library, a machine-checked collection of formal theorems. The theorem asserts that, for every real alpha and C_lag, these toy formulas exactly equal the linearized PPN functions gamma_lin and beta_lin from the framework's own PPN stack, once the parameter order is identified. The proof is a direct simplification: it expands both sides, uses commutativity of multiplication, and shows the coefficients match. The file's docstring notes the choice to keep these formulas local to the ILG layer, avoiding heavy dependency edges from the main Relativity file.

What this establishes in plain language is modest but real. The framework does not claim to have derived the PPN parameters from first principles here. It has verified, with a machine-checked proof, that two simple extraction formulas agree with its own linearized model. That agreement is a consistency check, not a derivation of general relativity. The value of the module is that it removes a placeholder and replaces it with a small, checkable identity, which is exactly the kind of bookkeeping the framework's emphasis on exact provenance rewards.

theorem ppn_derivation_holds : PPNDerivationHolds := by
  intro α C_lag
  constructor
  · -- γ: coefficients match and multiplication commutes
    simp [gamma_extraction_formula, PPN.gamma_lin, mul_comm, mul_left_comm, mul_assoc]
  · -- β: coefficients match and multiplication commutes
    simp [beta_extraction_formula, PPN.beta_lin, mul_comm, mul_left_comm, mul_assoc]

/-- Toy “extraction formulas” for PPN parameters.

We intentionally keep these *local* to the ILG layer (rather than importing the full
PostNewtonian stack) to avoid creating heavy dependency edges from `Relativity.lean`.
The point of this file is to eliminate the previous `Prop := True` stub
with a small, honest certificate.
-/
noncomputable def gamma_extraction_formula (α C_lag : ℝ) : ℝ :=
  1 + (1/10 : ℝ) * (α * C_lag)

What this page does not claim

This module does not derive the PPN parameters from the framework's foundational principles. The equality proven here does not establish that general relativity's PPN parameters equal 1 in the framework. The toy extraction formulas are definitional choices, not consequences of the forcing chain.

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/PPNDerive.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: