module module

`IndisputableMonolith.Foundation.DiscretenessForcing`

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 (11)

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

IndisputableMonolith.Foundation.InevitabilityStructure module_import
IndisputableMonolith.Foundation.LedgerForcing module_import
IndisputableMonolith.Foundation.OntologyPredicates module_import
IndisputableMonolith.Foundation.PhiForcing module_import
IndisputableMonolith.NumberTheory.ZeroCompositionInterface module_import
IndisputableMonolith.NumberTheory.ZeroCompositionLaw module_import
IndisputableMonolith.NumberTheory.ZeroDoublingLaw module_import
IndisputableMonolith.NumberTheory.ZeroLocationCost module_import
IndisputableMonolith.Papers.GCIC.DiscreteGauge module_import
IndisputableMonolith.Papers.GCIC.Thermodynamics module_import
IndisputableMonolith.Unification.CouplingLaw module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.LawOfExistence module_import

declarations in this module (20)

def J_log L47
theorem J_log_zero L50
theorem J_log_nonneg L53
theorem J_log_eq_zero_iff L60
theorem J_log_pos L84
theorem J_log_symmetric L90
theorem J_log_eq_J_exp L94
theorem J_log_second_deriv_at_zero L103
theorem cosh_quadratic_bound L118
theorem J_log_quadratic_approx L286
def IsStable L313
theorem continuous_no_isolated_zero_defect L326
theorem continuous_space_no_lockIn L391
structure DiscreteConfigSpace L409
theorem discrete_minimum_stable L427
theorem discreteness_forced L450
def RSExists_stable L468
theorem rs_exists_impossible_continuous L475
theorem stable_existence_requires_discrete L495
theorem discreteness_forcing_principle L517