Explain the Lean theorem `FRB_period_strict_increasing` in module `IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT`. 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.

1. What the declaration says in plain English

The theorem FRB_period_strict_increasing states that the predicted periodicity of a Fast Radio Burst (FRB) is strictly greater at higher "rungs" of the recognition ladder. If one rung index is strictly smaller than another, the corresponding FRB period is strictly shorter.

2. Why it matters in Recognition Science

In the RS framework, FRB repeaters are modeled not by standard astrophysical mechanisms (like binary orbits), but as macroscopic reflections of the fundamental BIT carrier band. The theory PREDICTS that FRB periods sit on a discrete geometric sequence (the φ-ladder). This theorem establishes the structural monotonicity of that sequence. Because the ladder step is exactly 360 (forced by 8-tick and gap-45 amplifications), this strictly increasing geometric progression provides a sharp, falsifiable HYPOTHESIS: FRB catalogs should reveal discrete periods stepping monotonically by factors of 360, rather than a continuous distribution.

3. How to read the formal statement

theorem FRB_period_strict_increasing {k m : ℕ} (h : k < m) :
    FRB_period_at_rung k < FRB_period_at_rung m

• {k m : ℕ}: Let k and m be arbitrary natural numbers, representing discrete rung indices on the ladder.
• (h : k < m): Assume the hypothesis h that k is strictly less than m.
• FRB_period_at_rung k < FRB_period_at_rung m: The output of the duration function FRB_period_at_rung at k is strictly less than the output at m.

4. Visible dependencies and certificates

Within the module, the proof relies on real-arithmetic facts tied to the RS definitions:

• FRB_period_at_rung: Defines the value at rung k as the base period multiplied by FRB_amplification_factor ^ k.
• FRB_amplification_factor_eq: Proves the amplification base is exactly 360 (which is > 1, ensuring exponential growth).
• BIT_carrier_period_pos: Ensures the base multiplier is strictly positive, preserving the inequality direction.

The theorem is formally bundled into the overarching structural certificate FastRadioBurstFromBITCert and the single-theorem rollup fast_radio_burst_one_statement.

5. What this declaration does not prove

This THEOREM proves a structural property of the mathematical definition of FRB_period_at_rung. It does not prove that physical FRBs actually adhere to this equation in the real universe; that remains a testable HYPOTHESIS subject to falsification by radio astronomy catalogs. Furthermore, the declaration itself does not derive the underlying physical mechanisms (e.g., gap-45 or the fundamental BIT frequency); it simply inherits them from upstream definitions to prove the resulting sequence behaves geometrically.