recognition /
Astrophysics /
Astrophysics.MassToLight /
explainer
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)
193 def AllConstantsDerived : Prop := ∃ c : ℝ, c = Constants.phi
proof body
Definition body.
194
195 /-- **HYPOTHESIS**: Zero-Parameter Status of Recognition Science.
196
197 STATUS: SCAFFOLD — While M/L is derived in this module, the full proof that
198 *all* physical constants are derived from the Meta-Principle is distributed
199 across the codebase.
200
201 TODO: Create a master certificate that imports all constant derivations. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (22)
Lean names referenced from this declaration's body.
all
in IndisputableMonolith.Aesthetics.NarrativeGeodesic
decl_use
all
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
Constants
in IndisputableMonolith.CPM.LawOfExistence
decl_use
all
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
Status
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
all
in IndisputableMonolith.Musicology.ModalPreferenceFromPhi
decl_use
that
in IndisputableMonolith.NumberTheory.PhiLadderLattice
decl_use
L
in IndisputableMonolith.Recognition
decl_use
M
in IndisputableMonolith.Recognition
decl_use
L
in IndisputableMonolith.Recognition.Cycle3
decl_use
M
in IndisputableMonolith.Recognition.Cycle3
decl_use
constant
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use