defect_must_be_small
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.