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)
29noncomputable def scale (k : ℕ) : ℝ := phi ^ k
proof body
Definition body.
30
used by (40)
From the project-wide theorem graph. These declarations reference this one in their body.
-
pentatonicSize
in IndisputableMonolith.Aesthetics.MusicalScale
decl_use
-
scale_fibonacci
in IndisputableMonolith.Aesthetics.MusicalScale
decl_use
-
third_quality
in IndisputableMonolith.Aesthetics.MusicalScale
decl_use
-
PhiInt
in IndisputableMonolith.Algebra.PhiRing
decl_use
-
ResonantScale
in IndisputableMonolith.Applied.CoherenceTechnology
decl_use
-
phi_energy_rung_pos
in IndisputableMonolith.Applied.PhotobiomodulationDevice
decl_use
-
luminosity_tier_local
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
NuclearTier
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
nuclear_tier_local
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
E_coh
in IndisputableMonolith.Astrophysics.ObservabilityLimits
decl_use
-
J_mass
in IndisputableMonolith.Astrophysics.ObservabilityLimits
decl_use
-
M_max
in IndisputableMonolith.Astrophysics.ObservabilityLimits
decl_use
-
OptimalConfig
in IndisputableMonolith.Astrophysics.ObservabilityLimits
decl_use
-
two_rung_gap_eq_phi_squared
in IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost
decl_use
-
J_bit_pos
in IndisputableMonolith.Astrophysics.StellarAssembly
decl_use
-
J_nonneg
in IndisputableMonolith.Astrophysics.StellarAssembly
decl_use
-
alphaInv_dimensionless
in IndisputableMonolith.Bridge.GaugeVsParams
decl_use
-
barrierLadder
in IndisputableMonolith.Chemistry.ActivationEnergy
decl_use
-
higher_temp_faster
in IndisputableMonolith.Chemistry.ActivationEnergy
decl_use
-
k_larger_shell_than_li
in IndisputableMonolith.Chemistry.AtomicRadii
decl_use
-
energyScale
in IndisputableMonolith.Chemistry.CrystalStructure
decl_use
-
hcp_ratio_near_phi
in IndisputableMonolith.Chemistry.CrystalStructure
decl_use
-
argon_ea_zero
in IndisputableMonolith.Chemistry.ElectronAffinity
decl_use
-
shell
in IndisputableMonolith.Chemistry.PeriodicBlocks
decl_use
-
familyLadderStep
in IndisputableMonolith.Chemistry.SuperconductingTc
decl_use
-
P_vs_NP_resolved
in IndisputableMonolith.Complexity.ComputationBridge
decl_use
-
J_cost
in IndisputableMonolith.CondensedMatter.JCostPhaseTransition
decl_use
-
phi_critical_energy
in IndisputableMonolith.CondensedMatter.JCostPhaseTransition
decl_use
-
sc_gap_scale
in IndisputableMonolith.CondensedMatter.JCostPhaseTransition
decl_use
-
alphaInv_linear_rate
in IndisputableMonolith.Constants.AlphaExponentialForm
decl_use
… and 10 more