module module

`IndisputableMonolith.Verification.Necessity.PhiNecessity`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.PhiSupport.Lemmas module_import

declarations in this module (7)

structure HasSelfSimilarity L11
lemma preferred_scale_pos L24
def self_similarity_from_discrete L46
lemma preferred_scale_fixed_point L64
lemma phi_result L87
theorem self_similarity_forces_phi L101
theorem phi_is_mathematically_necessary L111