ballistic_bound
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assume any relation between k and the phi-ladder rung index.
- Does not incorporate discreteness or quantum corrections from the mass formula.
- Does not address Berry creation thresholds or dream-fraction bounds.
- Does not extend the bound to curved or expanding backgrounds.
formal statement (Lean)
13theorem ballistic_bound (k a c : ℝ) (hk : 0 < k) (ha : 0 < a) (hc : 0 < c) :
14 let lambda_phys := 2 * Real.pi * a / k
proof body
Tactic-mode proof.
15 let tau_min := lambda_phys / c
16 let omega_max := 1 / tau_min
17 omega_max = k * c / (2 * Real.pi * a) := by
18 intro lambda_phys tau_min omega_max
19 dsimp [lambda_phys, tau_min, omega_max]
20 field_simp [hk.ne', ha.ne', hc.ne', Real.pi_ne_zero]
21
22/-- Proposition-level interface for A7: causal + scale-free closure. -/