pith. machine review for the scientific record. sign in
theorem proved term proof

J_phi_ceiling_band

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 165theorem J_phi_ceiling_band :
 166    0.11 < J_phi_ceiling ∧ J_phi_ceiling < 0.13 := by

proof body

Term-mode proof.

 167  unfold J_phi_ceiling
 168  have h1 := phi_gt_onePointSixOne
 169  have h2 := phi_lt_onePointSixTwo
 170  refine ⟨?_, ?_⟩ <;> linarith
 171
 172/-! ## §6. Master certificate -/
 173
 174/-- **TIDAL LOCKING FROM φ-RESONANCE MASTER CERTIFICATE (Track AS6).**
 175
 176Eight clauses, each derived from `Constants.phi` real-arithmetic:
 177
 1781. `moon_resonance_eq` : Moon-Earth 1:1 ratio.
 1792. `moon_J_cost_zero` : Moon at J-cost zero (trivial resonance).
 1803. `mercury_resonance_eq` : Mercury-Sun 3:2 = `3/2`.
 1814. `mercury_deviation_in_J_phi_band` : `|φ - 3/2| ∈ (0.11, 0.13)`,
 182   the canonical golden-section J-cost band.
 1835. `venus_resonance_eq` : Venus-Sun 4:1 (retrograde, period
 184   ratio = 4).
 1856. `phi_cubed_eq` : `φ^3 = 2φ + 1`.
 1867. `phi_cubed_band` : `φ^3 ∈ (4.22, 4.24)`.
 1878. `J_phi_ceiling_band` : ceiling `J(φ) ∈ (0.11, 0.13)`.
 188-/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (20)

Lean names referenced from this declaration's body.