module module moderate

`IndisputableMonolith.Unification.CriticalRecognitionLoading`

The CriticalRecognitionLoading module defines the native actuation period together with pulseTicks, supervisoryTicks, loadRatio and the predicates IsUnderloaded, IsSubcritical, IsOverloaded, InCriticalBand and rhoCriticalMin. Researchers modeling transitions between holographic information budgets and recognition costs would cite these when checking loading states against the 8-tick cadence. The module is purely definitional and contains no proofs.

claimNative actuation period given by pulseTicks and supervisoryTicks; load ratio and predicates IsUnderloaded, IsSubcritical, IsOverloaded, InCriticalBand, rhoCriticalMin.

background

The module sits inside the Unification domain and imports the RS time quantum τ₀ = 1 tick from Constants. RecognitionBandwidth supplies the 8-tick cadence (R̂ completes one cycle per 8τ₀), the recognition cost per bit k_R = ln(φ), and the ILG parameters C_lag = φ^{-5}, α = (1-1/φ)/2. ConsciousnessBandwidth states that a conscious boundary of extent L persisting for τ ticks has maintenance cost set by the holographic information budget (max information ∝ boundary area / 4 Planck areas). RecognitionBandGeometry supplies the geometric setting for the critical band.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the loading predicates and native actuation period that support unification of recognition bandwidth with consciousness bandwidth. It directly instantiates the 8-tick octave (T7) and the recognition cost k_R inside the critical-band geometry. No downstream theorems are recorded yet.

scope and limits

Does not derive numerical values for rhoCriticalMin from first principles.
Does not prove realizability of any critical loading state.
Does not connect the predicates to particle mass formulas or alpha band.
Does not address spatial dimension D = 3 or J-uniqueness.

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Unification.ConsciousnessBandwidth module_import
IndisputableMonolith.Unification.RecognitionBandGeometry module_import
IndisputableMonolith.Unification.RecognitionBandwidth module_import

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