module module

`IndisputableMonolith.Information.PhysicsComplexityStructure`

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

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Information.ComputationLimitsStructure module_import

declarations in this module (25)

structure of L15
theorem jcost_nonneg L46
theorem jcost_unique_minimum L52
theorem jcost_squared_form L59
theorem jcost_pos_away_from_one L65
theorem jcost_symmetric L76
def jcost_deriv L83
theorem jcost_deriv_zero_at_one L87
theorem jcost_deriv_pos_of_gt_one L92
theorem jcost_deriv_neg_of_lt_one L108
structure LedgerConfig L120
def totalJCost L125
theorem total_jcost_nonneg L129
theorem balanced_config_zero_cost L138
lemma sum_nonneg_zero_iff L144
theorem verification_equivalence L153
def physics_complexity_from_ledger L171
theorem physics_complexity_structure L174
theorem physics_complexity_implies_limits L178
theorem phi_hierarchy_exponential L184
theorem phi_rung_complexity_unbounded L189
theorem jcost_gradient_descent_converges L195
theorem jcost_complexity_gap L211
def rs_complexity_classes L219
def ic005_certificate L230