pith. machine review for the scientific record. sign in
theorem other other high

kappa_eq_8phi5

show as:
view Lean formalization →

The declaration fixes the Einstein coupling exponent at 5 and the associated period at 8 in Recognition Science units. A researcher computing G or the mass ladder from the coherence exponent would cite it to lock the prefactors once k=5 is established at D=3. The proof succeeds by a single decide tactic that evaluates the two constant definitions.

claimIn RS units the Einstein coupling satisfies exponent 5 and period 8, so that the coupling takes the concrete form $8φ^5$.

background

The module shows that the coherence exponent is forced to 5 uniquely at D=3 by agreement of two routes: the Fibonacci deficit $k_{fib}(D)=2^D-D$ and the integration measure $k_{int}(D)=D+2$. Both equal 5 only when D=3; they differ at D=1,2,4. The upstream definitions einsteinKappaExponent and einsteinKappaPeriod simply record the numerical values 5 and 8 that follow from this agreement and from the eight-tick octave.

proof idea

The proof is a one-line wrapper that applies the decide tactic to evaluate the two constant definitions directly.

why it matters in Recognition Science

The result supplies the concrete numbers for the Einstein coupling $κ=8φ^5$ that enters the gravitational constant $G=φ^5/π$ and the mass formula on the phi-ladder. It completes the numerical step of the Beltracchi response §3 on coherence-exponent uniqueness at D=3, consistent with the T7 eight-tick octave in the forcing chain. No downstream theorems are recorded.

scope and limits

formal statement (Lean)

  73theorem kappa_eq_8phi5 : einsteinKappaExponent = 5 ∧ einsteinKappaPeriod = 8 := by decide

proof body

  74

depends on (2)

Lean names referenced from this declaration's body.