decoy_magnitude_only_ne_mesh_geometricDeficit
plain-language theorem explainer
The absolute value of the signed mesh geometric deficit cannot equal that deficit on any punctured interval 0 < |h| < 1. Gravity analysts ruling out magnitude-only decoys when assembling the dual-entry DeficitSourceConstitutiveCoupling cite this. The proof shows the absolute-value map is even (via oddness of the deficit) and hands it to the banked even-function decoy.
Claim. It is not the case that for every real $h$ with $0 < |h| < 1$ one has $|\delta_{\mathrm{mesh}}(h)| = \delta_{\mathrm{mesh}}(h)$, where $\delta_{\mathrm{mesh}}$ is the signed mesh geometric deficit (Regge-convention star deficit).
background
Local setting is Wave B residual R4: assemble banked R1 (mesh geometric deficit), R2 (hinge kappa plus source domination), and R3 (dual-entry strain state) into an inhabited DeficitSourceConstitutiveCoupling on carrier $H = \mathbb{R}$, then apply the blocker's conditional recognition-ratio derivation. The module does not flip gap1_bridge_derived and keeps the carrier as reshaped $\mathbb{R}$, not an encoded Freudenthal triangulation.
The mesh geometric deficit $\delta_{\mathrm{mesh}} : \mathbb{R} \to \mathbb{R}$ is the banked signed Regge-convention star deficit built from squared-edge and dihedral geometry; no ratio or log appears in its definition. It is odd: $\delta_{\mathrm{mesh}}(-h) = -\delta_{\mathrm{mesh}}(h)$. Upstream, any even-in-$h$ candidate is already ruled out as equal to $\delta_{\mathrm{mesh}}$ on a punctured interval (the banked even-function decoy, alias even_cannot_match_starDeficit). Convention: deficit iff debit-leads ($0 < h$).
proof idea
First prove that $h \mapsto |\delta_{\mathrm{mesh}}(h)|$ is even: rewrite $|\delta_{\mathrm{mesh}}(-h)|$ by the oddness lemma $\delta_{\mathrm{mesh}}(-h) = -\delta_{\mathrm{mesh}}(h)$ and cancel the outer absolute value via abs_neg. Then apply the upstream even-function decoy theorem to the candidate $g(h) := |\delta_{\mathrm{mesh}}(h)|$ with that evenness witness. The decoy discharges the universal equality on $0 < |h| < 1$, yielding the desired negation. Short tactic proof: one local evenness fact plus a single application of the banked decoy.
why it matters
This is Decoy 2 in the dual-entry coupling package: the columnless magnitude-only extract $|\delta|$ is even in the deformation parameter and therefore cannot match the signed mesh geometric deficit. Downstream it is conjoined with the R3 swap-evenness decoy inside adversarial_decoys_mesh_dual_entry, which packages both adversarial non-identifications for the mesh dual-entry assembly.
In the Recognition Gravity stack this protects the signed deficit side of DeficitSourceConstitutiveCoupling against a natural ledger-style collapse to absolute magnitude. It sits under the Wave B attack on TypedResidual_DeficitSourceConstitutiveCoupling_from_enrichment and feeds the conditional mesh_recognition_ratio_derived theorem. It does not close gap1_bridge_derived, R0a/R0b name-bindings, or the Freudenthal-lift openness; those remain upstream scaffolding. Landmark contact is local to the gravity residual DAG rather than T0–T8 forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.