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)
50theorem angle_bias : 0 < tetra_bias := by
proof body
Tactic-mode proof.
51 dsimp [tetra_bias]
52 have hφ : 1 < Constants.phi := Constants.one_lt_phi
53 have hφpos : 0 < Constants.phi := lt_trans (by norm_num) hφ
54 have h_inv_lt : (1 / Constants.phi) < 1 := by
55 rw [div_lt_one hφpos]
56 exact hφ
57 exact sub_pos.mpr h_inv_lt
58
59/-! ## Optimal Bond Angle for n Equivalent Bonds -/
60
61/-- Optimal cosine of bond angle for n equivalent bonds.
62 cos(θ_opt) = -1/(n-1) for n ≥ 2. -/
depends on (12)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
tetra_bias
in IndisputableMonolith.Chemistry.BondAngles
decl_use
-
one_lt_phi
in IndisputableMonolith.Constants
decl_use
-
Constants
in IndisputableMonolith.CPM.LawOfExistence
decl_use
-
lt_trans
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
one_lt_phi
in IndisputableMonolith.PhiSupport
decl_use
-
one_lt_phi
in IndisputableMonolith.PhiSupport.Lemmas
decl_use