module module

`IndisputableMonolith.Foundation.PhiForcing`

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

used by (40)

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

IndisputableMonolith.Constants.ElectronMass module_import
IndisputableMonolith.Constants.FineStructureConstant module_import
IndisputableMonolith.Constants.GravitationalConstant module_import
IndisputableMonolith.Constants.PlanckScaleMatching module_import
IndisputableMonolith.Cosmology.DarkMatter module_import
IndisputableMonolith.Cosmology.FlatnessProblem module_import
IndisputableMonolith.Cosmology.GalaxyRotation module_import
IndisputableMonolith.Cosmology.Nucleosynthesis module_import
IndisputableMonolith.Foundation.ConstantDerivations module_import
IndisputableMonolith.Foundation.DimensionForcing module_import
IndisputableMonolith.Foundation.HierarchyDissolution module_import
IndisputableMonolith.Foundation.HierarchyEmergence module_import
IndisputableMonolith.Foundation.HierarchyMinimality module_import
IndisputableMonolith.Foundation.InevitabilityStructure module_import
IndisputableMonolith.Foundation.OntologyPredicates module_import
IndisputableMonolith.Foundation.ParticleGenerations module_import
IndisputableMonolith.Foundation.StillnessGenerative module_import
IndisputableMonolith.Gravity.GalacticTimescale module_import
IndisputableMonolith.Masses.LeptonMassLadder module_import
IndisputableMonolith.Masses.MassHierarchy module_import
IndisputableMonolith.Masses.MassRatiosProved module_import
IndisputableMonolith.Mathematics.Euler module_import
IndisputableMonolith.Papers.GCIC.DiscreteGauge module_import
IndisputableMonolith.Physics.ElectroweakBosons module_import
IndisputableMonolith.Physics.KaonMasses module_import
IndisputableMonolith.Physics.PionMasses module_import
IndisputableMonolith.Physics.ThermalFixedPoint module_import
IndisputableMonolith.Physics.WeakForceEmergence module_import
IndisputableMonolith.QFT.RunningCouplings module_import
IndisputableMonolith.QFT.UVCutoff module_import

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.DiscretenessForcing module_import
IndisputableMonolith.Foundation.LawOfExistence module_import
IndisputableMonolith.Foundation.LedgerForcing module_import
IndisputableMonolith.Foundation.PhiForcingDerived module_import

declarations in this module (24)

theorem phi_equation L43
theorem phi_pos L51
theorem phi_gt_one L62
theorem phi_lt_two L73
theorem phi_gt_onePointSixOneEight L84
theorem phi_lt_onePointSixOneNine L93
theorem phi_lt_onePointEight L102
theorem phi_gt_onePointSix L106
theorem phi_inv L110
theorem J_phi L123
structure SelfSimilar L131
def satisfies_golden_constraint L148
theorem self_similar_forces_golden_constraint L151
theorem phi_satisfies L159
theorem golden_constraint_unique L162
theorem phi_unique_self_similar L186
structure DiscreteLedger L193
def is_self_similar L200
theorem phi_forced L213
def J_bit L220
theorem J_bit_pos L223
def E_coh L226
theorem E_coh_pos L229
theorem phi_forcing_principle L246