module module

`IndisputableMonolith.Foundation.InevitabilityStructure`

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.Foundation.InevitabilityEquivalence module_import

depends on (6)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.DAlembert.TriangulatedProof module_import
IndisputableMonolith.Foundation.DiscretenessForcing module_import
IndisputableMonolith.Foundation.LawOfExistence module_import
IndisputableMonolith.Foundation.LedgerForcing module_import
IndisputableMonolith.Foundation.PhiForcing module_import

declarations in this module (26)

structure NecessityGate L64
def gate_cost_uniqueness L73
def gate_selection_rule L80
def gate_discreteness L87
def gate_ledger L94
def gate_phi L101
def gate_dimension L108
def all_gates L115
structure AlternativeFramework L122
def RS_framework L133
def zero_parameter L141
def violates_gate L144
theorem inevitability L172
structure ChokePoint L202
def choke_universality L211
def choke_cost_axioms L218
def choke_exclusivity L225
def choke_dimension L232
def all_choke_points L239
def closed_count L243
def scaffold_count L246
structure UpgradePath L251
def inevitability_upgrade L260
def economic_inevitability_statement L275
theorem economic_inevitability L282
theorem inevitability_structure_summary L314