ballistic_bound
plain-language theorem explainer
Ballistic_bound supplies the explicit identity omega_max = k c / (2 pi a) for the maximum angular frequency of a mode whose physical wavelength is 2 pi a / k. Researchers on causal closure in the DIF papers cite it when bounding refresh rates inside scale-free structures. The proof is a direct algebraic simplification that unfolds the three let bindings and cancels via field_simp under the three positivity hypotheses.
Claim. For real numbers $k,a,c>0$, let $lambda_phys=2pi a/k$. Define $tau_min=lambda_phys/c$ and $omega_max=1/tau_min$. Then $omega_max=kc/(2pi a)$.
background
The declaration lives in Papers.DIF.CausalClosure, whose module-level comment describes a proposition-level interface for A7 on causal plus scale-free closure. Upstream, the scale definition from LargeScaleStructureFromRS supplies the phi-ladder lengths via noncomputable def scale (k : ℕ) : ℝ := phi ^ k. The for structure from UniversalForcingSelfReference records the meta-realization axioms that close self-referential forcing chains.
proof idea
Tactic proof. The script introduces the three let-bound identifiers, applies dsimp to expand lambda_phys, tau_min and omega_max, then invokes field_simp with the negated positivity hypotheses together with Real.pi_ne_zero to reach the target equality.
why it matters
The identity closes Gap 3 of the algebraic core for ballistic causality bounds on mode refresh frequency. It supports sibling results such as CausalClosureForced and scale_free_causal_closure inside the same module. In the Recognition framework it supplies the concrete frequency bound required by the T7 eight-tick octave and the scale-free part of A7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.