def
definition
closed_count
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.InevitabilityStructure on GitHub at line 243.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
240 [choke_universality, choke_cost_axioms, choke_exclusivity, choke_dimension]
241
242/-- Count of closed choke points. -/
243def closed_count : ℕ := (all_choke_points.filter (fun c => c.status = "closed")).length
244
245/-- Count of scaffolded choke points. -/
246def scaffold_count : ℕ := (all_choke_points.filter (fun c => c.status = "scaffold")).length
247
248/-! ## The Inevitability Upgrade Path -/
249
250/-- The upgrade path: what needs to happen to make inevitability complete. -/
251structure UpgradePath where
252 /-- Current state -/
253 current_state : String
254 /-- Required steps -/
255 steps : List String
256 /-- Target state -/
257 target_state : String
258
259/-- The path to complete inevitability. -/
260def inevitability_upgrade : UpgradePath := {
261 current_state := "Partial: Cost uniqueness proven, other gates scaffolded"
262 steps := [
263 "1. Prove CPM Universality: selection = coercive minimization (no alternatives)",
264 "2. Prove Dimension Forcing: linking + gap-45 → D = 3",
265 "3. Complete Exclusivity: any zero-param framework ≅ RS",
266 "4. Remove EQUIV_AX scaffolds: connect abstract claims to concrete defs"
267 ]
268 target_state := "Complete: Any alternative must violate a necessity or add parameters"
269}
270
271/-! ## The Economic Inevitability Framing -/
272
273/-- The core insight in economic terms: