theorem
proved
constrained_count_eq_4
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Superhuman.Core on GitHub at line 134.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
131theorem accessible_count_eq_23 :
132 (allPowers.filter Power.accessible).length = 23 := by native_decide
133
134theorem constrained_count_eq_4 :
135 (allPowers.filter (fun p => !(Power.accessible p))).length = 4 := by native_decide
136
137/-- Class A has exactly 6 powers. -/
138theorem classA_count :
139 (allPowers.filter (fun p => powerClass p == .DirectMechanism)).length = 6 := by native_decide
140
141/-- Class B has exactly 6 powers. -/
142theorem classB_count :
143 (allPowers.filter (fun p => powerClass p == .Derivable)).length = 6 := by native_decide
144
145/-- Class C has exactly 6 powers. -/
146theorem classC_count :
147 (allPowers.filter (fun p => powerClass p == .NautilusClass)).length = 6 := by native_decide
148
149/-- Class D has exactly 5 powers. -/
150theorem classD_count :
151 (allPowers.filter (fun p => powerClass p == .Speculative)).length = 5 := by native_decide
152
153/-- Class E has exactly 4 powers. -/
154theorem classE_count :
155 (allPowers.filter (fun p => powerClass p == .Constrained)).length = 4 := by native_decide
156
157/-! ## Constraint Type -/
158
159/-- Why a power is constrained or forbidden. -/
160inductive ConstraintReason where
161 | zConservation -- Z is conserved; cannot duplicate patterns
162 | jUniqueness -- J is uniquely forced; cannot override cost structure
163 | costOfNothing -- J(0⁺) → ∞; cannot create from nothing
164 | boundaryDissolution -- Dissolution always thermodynamically available