module module

`IndisputableMonolith.RRF.Foundation.MetaPrinciple`

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

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

IndisputableMonolith.RRF.Foundation module_import

declarations in this module (15)

theorem MetaPrinciple L39
theorem recognition_implies_existence L45
theorem empty_has_no_self_recognition L50
structure RecognitionStructure L61
theorem recognition_structure_nonempty L68
structure MinimalLedger L75
class MPForcesLedger L86
structure SelfSimilarity L108
def phi L117
theorem phi_pos L120
theorem phi_sq L126
theorem self_similarity_forces_phi L137
structure DerivationChain L175
theorem derivation_chain_consistent L184
theorem phi_unique L193