module module

`IndisputableMonolith.Verification.ILGAPrioriPredictionCert`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.ILG module_import
IndisputableMonolith.Foundation.PhiForcing module_import
IndisputableMonolith.ILG.Kernel module_import

declarations in this module (22)

structure SelfSimilarMemory L81
theorem self_similarity_forces_alpha L114
theorem alpha_from_two_scale_decomposition L125
structure APrioriPrediction L142
def rs_a_priori_prediction L160
theorem a_priori_alpha L168
theorem a_priori_C L171
structure SPARCBestFit L179
def sparc_best_fit L190
def within_n_sigma L201
lemma one_div_phi_gt L207
lemma one_div_phi_lt L216
lemma alphaLock_gt L225
lemma alphaLock_lt L236
theorem alpha_prediction_validated L256
lemma phi_neg2_eq L274
lemma phi_neg2_gt L286
lemma phi_neg2_lt L298
theorem C_prediction_validated L313
structure ILGAPrioriCert L343
theorem prediction_validation_logic L400
def upgrade_status L423