Explain the Lean theorem `alpha_is_bandwidth_exponent` in module `IndisputableMonolith.Unification.BandwidthSaturation`. Write for an educated reader who knows science and programming but may not know Lean. Cover: (1) what the declaration says in plain English, (2) why it matters in Recognition Science, (3) how to read the formal statement, (4) visible dependencies or certificates in the supplied source, and (5) what this declaration does not prove. Cite only declarations present in the supplied Recognition source.

Explanation of alpha_is_bandwidth_exponent

(1) Plain English

The declaration states that alpha_locked (the RS-native fine-structure parameter) equals exactly (1 - 1/φ)/2, where φ is the golden ratio forced by the cost functional.

(2) Why it matters in Recognition Science

It identifies the power-law exponent α in the bandwidth kernel's scaling with dynamical time (when T_dyn ≫ τ₀) as the same φ-derived quantity that appears in the fine-structure constant. This directly ties holographic bandwidth limits in saturated gravitational regimes to the ledger's reciprocal symmetry, showing ILG parameters emerge from recognition throughput without external inputs.

(3) How to read the formal statement

theorem alpha_is_bandwidth_exponent :
    alpha_locked = (1 - 1 / phi) / 2 := rfl

• theorem declares a proved statement.
• The left side is the identifier alpha_locked (imported from Constants/ILG).
• The right side is the explicit φ-expression.
• := rfl means the equality holds by reflexivity (i.e., alpha_locked is definitionally equal to the expression).

(4) Visible dependencies or certificates

• Imports: IndisputableMonolith.Constants, IndisputableMonolith.Constants.ILG, IndisputableMonolith.Cost, IndisputableMonolith.Unification.RecognitionBandwidth.
• Relies on phi and the definition of alpha_locked from the Constants hierarchy.
• Sits alongside proved facts in the same module such as saturationAccel_pos and kernel_gt_one_when_saturated.
• No sorry or external axioms appear in this declaration; it is a pure definitional unfolding.

(5) What this declaration does not prove

It does not derive or force the exponential form of α⁻¹ itself, nor prove that the constant logarithmic derivative must hold from first principles. Those remain open (see the uniqueness Prop in the AlphaExponentialForm module). It also does not connect the equality to measured CODATA values or close the gap to SI units.