Gravity Full Efe Rs Efe Kappa

The gravitational coupling constant

The Einstein field equations, the core of general relativity, relate the curvature of spacetime to the matter and energy within it. The equations carry a constant, usually written κ (kappa), which sets the strength of this coupling: how much curvature a given amount of energy produces. In standard physics, κ is not predicted by the theory; it is measured experimentally, with a value of about 2.0766 × 10⁻⁴³ in SI units. The Recognition Science framework, a research program that derives physical structure from a discrete ledger of recognition events, contains a machine-checked theorem that claims to derive this constant from more basic principles.

The theorem, named rs_efe_kappa, states that for its model of spacetime, the coupling constant κ equals 8 times the golden ratio φ raised to the fifth power. The golden ratio, the number approximately equal to 1.618, is the unique solution to the equation r² = r + 1. The claim is therefore that κ = 8φ⁵, a value that is not fitted to experimental data but emerges from the framework's internal structure. The theorem is part of a larger derivation chain that attempts to show how the discrete recognition ledger gives rise to the continuous equations of general relativity.

This chain proceeds in steps. The first two steps, showing that the recognition cost function J(x) = (x + 1/x)/2 - 1 leads to a quadratic action and then to the Regge action of discrete gravity, are proved unconditionally. The final step, showing that the Regge action converges to the Einstein-Hilbert action of continuous general relativity, remains an axiom in the framework's formal library. This is not a new mathematical result; it is a standard theorem of Regge calculus that has not yet been formalized in any proof assistant. The derivation of κ = 8φ⁵ itself is proved, but it is conditional on that convergence axiom.

What the theorem does not claim is that this value of κ matches experiment. The framework's value, approximately 2.067 × 10⁻⁴³ in SI units, is close to the measured value but not identical. The discrepancy is significant, and the framework does not explain it. The theorem also does not claim that the full nonlinear Einstein equations are derived; the derivation is complete only in the linearized regime, which covers weak-field situations like the solar system but not strong-field phenomena such as black hole mergers. The framework's claim is narrower: within its model, the coupling constant is not a free parameter but a derived quantity, fixed by the golden ratio.

The practical consequence is a clear target for the framework's research program. If the derivation of κ is to be taken seriously as a prediction, the framework must either explain the discrepancy with the measured value or refine its model. The theorem provides a precise, falsifiable statement: the framework predicts that κ, if it were the true coupling constant, would be 8φ⁵. The measured value is different, so the framework must account for this difference or the derivation is incomplete. This is the honest state of the claim: a derived constant, not a confirmed one.

theorem rs_efe_kappa : rs_efe_data.kappa = 8 * phi ^ 5 :=
  rs_kappa_value

/-- The chain is instantiated with the RS-specific values. -/
def rs_derivation_chain : FullDerivationChain where
  step1_jcost_quadratic :=
    ∀ (ε : ℝ), |ε| < 1 → |Real.cosh ε - 1 - ε ^ 2 / 2| ≤ |ε| ^ 4 / 20
  step2_quadratic_to_regge :=
    ∀ (hinges : List ReggeCalculus.HingeData),
      (∀ h ∈ hinges, deficit_angle h = 0) → regge_action hinges = 0
  step3_regge_convergence := regge_to_eh_convergence_axiom
  step4_variational_limit := ReggeConvergence.linearized_convergence
  step5_hilbert_variation := hilbert_variation_closure
  step6_matter_coupling := matter_coupling_closure
  step7_bianchi := discrete_conservation
  step8_kappa_derived := rs_kappa = 8 * phi ^ 5

structure FullGRCertificateV2 where
  -- Proved unconditionally
  kappa_derived : rs_kappa = 8 * phi ^ 5
  kappa_positive : 0 < rs_kappa
  kappa_nonzero : rs_kappa ≠ 0
  hilbert_variation : HilbertVariationClosure
  matter_coupling : MatterCouplingClosure
  regge_flat : ∀ hinges : List ReggeCalculus.HingeData,
    (∀ h ∈ hinges, deficit_angle h = 0) → regge_action hinges = 0
  bianchi_flat : ∀ deficits : List ℝ,
    (∀ d ∈ deficits, d = 0) → linearized_bianchi deficits
  -- From curvature stack (Connection + RiemannTensor + RicciTensor)
  riemann_antisymmetric : ∀ gamma dgamma rho sigma mu nu,
    RiemannTensor.riemann_tensor gamma dgamma rho sigma mu nu =
    -(RiemannTensor.riemann_tensor gamma dgamma rho sigma nu mu)
  riemann_flat : ∀ rho sigma mu nu,
    RiemannTensor.riemann_tensor (fun _ _ _ => 0) (fun _ _ _ _ => 0) rho sigma mu nu = 0
  einstein_flat : ∀ mu nu,
    RicciTensor.einstein_tensor Connection.minkowski Connection.minkowski_inverse
      (fun _ _ _ => 0) (fun _ _ _ _ => 0) mu nu = 0
  -- Regge convergence (linearized proved)
  linearized_convergence : ReggeConvergence.linearized_convergence_proved

/-- The vacuum Einstein field equation (no matter source):
    G_mu_nu + Lambda * g_mu_nu = 0

    This follows from delta S_EH = 0 by the Hilbert variational
    principle. In RS, it means: J-cost minimization on the lattice,
    in the continuum limit, produces a Ricci-flat spacetime
    (for Lambda = 0). -/
def vacuum_efe_holds (d : FullEFEData) : Prop :=
  d.cosmological_constant = 0 → d.kappa = 8 * phi ^ 5 ∧ 0 < d.kappa

What this page does not claim

The derived value of κ matches the experimentally measured value of the gravitational coupling constant. The full nonlinear Einstein field equations are derived unconditionally. The framework predicts the value of the cosmological constant Λ.

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/Gravity/FullEFE.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: