Pith. sign in
module module high

IndisputableMonolith.Physics.QuantumGravityFromRS

show as:
view Lean formalization →

The module defines the bounce radius at rung N as r_min(N) = phi^(N/2) along with the quantum gravity approach and certification in the Recognition Science setting. Researchers deriving gravitational effects from the RS forcing chain would cite these objects. The module supplies definitions and elementary properties such as positivity and monotonicity of the radius and echo delay.

claimThe bounce radius satisfies \( r_{\min}(N) = \phi^{N/2} \) at rung N, with supporting quantities for the quantum gravity approach and echo delay.

background

The module imports Constants, where the fundamental RS time quantum is defined as \tau_0 = 1 tick. It introduces the bounce radius using the phi-ladder from the unified forcing chain, together with the quantum gravity approach (QGApproach) and its certification. The local setting is the extraction of gravitational bounce phenomena from the Recognition Composition Law and the self-similar fixed point phi.

proof idea

This is a definition module with short supporting lemmas. The main objects are introduced directly from the phi-ladder; positivity and monotonicity follow from elementary properties of the exponential.

why it matters in Recognition Science

The definitions supply the concrete objects needed for the quantum gravity certification and approach. They link the phi fixed point (T6) and the eight-tick octave (T7) to gravitational scales, advancing the program of obtaining all physics from the single functional equation.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)