defect_must_be_small
The theorem establishes that the absolute curvature defect strength must satisfy |δκ| < 10^{-5}. Experimental physicists reviewing ANITA upgoing events in the Recognition Science framework would cite it to rule out detectable geometric anomalies. The proof is a term-mode reduction that unfolds the defect strength definition and normalizes the resulting numerical inequality.
claim$ |δκ| < 10^{-5} $, where δκ is the hypothetical curvature defect strength.
background
The ANITA module examines four ultra-high-energy events detected by the balloon experiment that appear to originate below the Earth. Standard attenuation lengths at EeV energies render the Earth opaque, so the analysis considers systematic effects, rare Standard Model configurations, or speculative RS geometric defects. The Defect definition from CPM.LNALBridge supplies a toy functional that returns zero when structural checks pass and one otherwise. The curvature_defect_strength definition supplies the concrete numerical value 1e-6 for this hypothetical defect.
proof idea
The proof is a one-line term wrapper. It unfolds the curvature_defect_strength definition to expose the literal 1e-6 value, then applies norm_num with the abs_of_pos lemma to discharge the absolute-value inequality.
why it matters in Recognition Science
The result feeds directly into the ea004_certificate, which concludes that ANITA events are most likely systematic or rare atmospheric effects with BSM probability around 5 percent. It completes the EA-004.5 step that bounds any RS curvature defect below the threshold for detection in other experiments, consistent with the framework's requirement that geometric anomalies remain smaller than the phi-ladder spacing and the eight-tick octave constraints.
scope and limits
- Does not prove the physical existence of any curvature defect.
- Does not compute event probabilities or likelihood ratios.
- Does not model full Earth attenuation or shower development.
- Does not apply the bound to experiments other than ANITA.
formal statement (Lean)
109theorem defect_must_be_small : |curvature_defect_strength| < 1e-5 := by
proof body
Term-mode proof.
110 unfold curvature_defect_strength
111 norm_num [abs_of_pos]
112
113/-- **THEOREM EA-004.6**: Geometric effect requires specific Earth locations.
114 Defect sites must align with ANITA detection points. -/