decoy_pullback_excluded
plain-language theorem explainer
Records that arbitrary test-variation pullbacks stay excluded from the 4D continuum action theorem. Anyone auditing the Recognition-mesh gate of the QG continuum campaign cites this as the local decoy flag. The proof is a one-line term wrapper of the preflight triviality.
Claim. The decoy proposition ``arbitrary test-variation pullbacks are excluded from the continuum action theorem'' holds. Equivalently, response-level pullback hypotheses are not admitted as premises for the Recognition-native mesh bridge that closes $S_{\mathrm{RS}}\to\mathrm{EH}$ in 4D.
background
This module builds the canonical Recognition mesh on the periodic Freudenthal 4-torus and attaches a value-level exact-$J$ action whose amplitude Hessian is the geometric Option-C midpoint Bloch symbol. Binding honesty requires that continuum closers use a Recognition-native mesh bridge, not response-level gadgets.
Upstream, the continuum preflight defines the decoy proposition ``ArbitraryPullbackExcluded'' as the constant true proposition, with the gloss that arbitrary test-variation pullbacks are excluded from the action theorem and do not inhabit the 4D Einstein-Hilbert convergence statement. The preferred limit shape is amplitude Hessian at fixed mesh, then $N\to\infty$.
Sibling material identifies the mesh carrier, the exact-$J$ action on that mesh, and equality of its Hessian with the true-Regge Hessian by construction. Elevating that Hessian to the full nonlinear Regge action via Schläfli remains open.
proof idea
One-line term wrapper: the goal is exactly the preflight proposition, discharged by applying the preflight theorem decoy_arbitrary_pullback_excluded, whose body is trivial because that proposition is defined as True.
why it matters
In the QG full-theory campaign this is the local copy of Decoy D4 under the Recognition gate of the 4D continuum closure. It freezes the hypothesis surface: continuum action theorems must route through the Recognition-native mesh and the Option-C midpoint Bloch symbol, not through arbitrary TestVariationPullback premises.
The module doc ties this to the proved amplitude-Hessian identity and the iterated $N\to\infty$ Tendsto to the scale-explicit Option-C Einstein-Hilbert face, while explicitly not flipping gap-action recovery and not inhabiting the full $S_{\mathrm{RS}}$ converges to EH in 4D. No downstream consumers are wired yet; the flag is bookkeeping for auditors of the continuum preflight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.