IndisputableMonolith.Unification.CriticalRecognitionLoading

declarations in this module (29)

• def pulseTicks L44
• def supervisoryTicks L47
• theorem supervisoryTicks_eq L49
• theorem supervisoryTicks_is_lcm L52
• theorem pulse_divides_supervisory L56
• def loadRatio L64
• def IsUnderloaded L68
• def IsSubcritical L72
• def IsOverloaded L76
• def InCriticalBand L80
• abbrev rhoCriticalMin L84
• theorem rhoCriticalMin_eq L86
• def InForcedCriticalBand L90
• theorem loadRatio_pos L93
• theorem criticalBand_implies_subcritical L98
• theorem criticalBand_not_overloaded L109
• def semanticFreeEnergy L121
• theorem higher_entropy_lowers_freeEnergy L125
• theorem higher_berry_lowers_freeEnergy L135
• def SemanticCondensationGate L146
• theorem semanticGate_implies_attention_cap L154
• theorem semanticGate_implies_gap_ready L161
• structure ControllerState L171
• def IsCriticalRecognitionLoading L185
• def IsForcedCriticalRecognitionLoading L192
• def loadPenalty L196
• theorem loadPenalty_zero_of_critical L199
• theorem criticalRecognitionLoading_certificate L211
• theorem forcedCriticalRecognitionLoading_certificate L226