pith. sign in
module module high

IndisputableMonolith.Physics.QuantumCoherenceTimeFromJCost

show as:
view Lean formalization →

This module defines quantum coherence times derived from the J-cost function on the phi-ladder in Recognition Science. It supplies coherenceTimeAtRung, coherenceTimeRatio, and a CoherenceTimeCert structure, plus supporting phi-power identities and bounds. Researchers computing RS-native quantum time scales would cite it for coherence calculations. The module consists of direct definitions from the Cost module together with short algebraic lemmas on phi powers.

claimLet $τ_0 = 1$ be the fundamental RS time quantum. Coherence time at rung $r$ is given by $τ_c(r)$ derived from $J$-cost applied at phi-ladder positions, with the identity $φ^8 = 21φ + 13$ used to obtain bounds such as $φ^8 > 46$ and $φ^{12} > 300$.

background

Recognition Science derives all physics from the single J-cost functional equation. This module sits in the physics domain and imports the RS time quantum $τ_0 = 1$ tick from Constants together with the J-cost definitions from the Cost module. It works on the phi-ladder whose self-similar fixed point is forced at T6 of the UnifiedForcingChain, using the eight-tick octave period from T7. The supplied module doc-comment records the Fibonacci identity $φ^8 = 21φ + 13$ that supplies the numerical bounds appearing in the sibling declarations.

proof idea

This is a definition module. coherenceTimeAtRung and coherenceTimeRatio are defined directly by applying the J-cost at the appropriate phi-ladder rung. The lemma phi8_fibonacci establishes the identity $φ^8 = 21φ + 13$ by algebraic expansion of the golden-ratio recurrence. The inequalities phi8_gt_46 and phi12_gt_300 are obtained by direct numerical comparison once the identity is available. CoherenceTimeCert packages the resulting time values for downstream certification.

why it matters in Recognition Science

The module supplies the concrete time-scale objects required for quantum coherence calculations inside the Recognition framework. It feeds the parent structures that close the link between J-cost and observable time intervals, supporting the T7 eight-tick octave and the phi-ladder mass/time formulas. No open scaffolding remains inside the module itself.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)