ArbitraryPullbackExcluded
plain-language theorem explainer
Decoy D4 records that arbitrary test-variation pullbacks stay outside the 4D continuum action closer. Anyone auditing the Regge weak-field EH recovery cites it to block response-level pullback hypotheses from counting as a mesh bridge. The declaration is definitionally True: an honesty marker, not a derived geometric claim.
Claim. The decoy proposition ``arbitrary test-variation pullbacks are excluded from the continuum action theorem'' is the constant true proposition. In particular, response-level pullback hypotheses do not inhabit the packaged open closer that weak-field quadratic Regge action converges to the Einstein-Hilbert target and vanishes on pure gauge.
background
This module is the first binding increment of the 4D continuum closure plan in the QG full-theory campaign. It freezes the independent continuum target, canonical mesh carrier, normalized TT data, pure-gauge family, and honesty decoys before further computation. Nothing in the module proves continuum recovery.
The packaged open closer is the conjunction of two Tendsto-style targets: weak-field quadratic action convergence to the independently frozen linearized Einstein-Hilbert functional (with kappa_einstein, not a free lattice scale) and vanishing on pure gauge. The canonical carrier is a periodic Freudenthal 4-torus of side $N \ge 3$, with Frobenius-normalized Euclidean TT polarizations.
Decoy D4 exists so that a response-level test-variation pullback cannot be smuggled in as inhabiting that closer. The frozen path demands a Recognition-native mesh bridge; arbitrary pullbacks are explicitly out of scope.
proof idea
Definitional abbreviation: the proposition is set equal to True. No lemmas, no tactics, no algebraic reduction. Downstream inhabitants are one-line trivial (or wrappers of that triviality).
why it matters
In the preflight contract, decoys are binding THEOREM-tier discriminators that keep the ledger honest while continuum Tendsto props remain OPEN and S_RS_converges_EH_4d uninhabited. This marker feeds decoy_arbitrary_pullback_excluded in the same module and decoy_pullback_excluded in the Recognition-mesh exact-$J$ bridge, both of which simply restate that arbitrary pullbacks remain excluded.
It protects the non-fitting rule stated in the module: the EH quadratic is frozen independently of the lattice symbol; later algebraic closers must observe equality, never reverse-engineer weights or accept an off-mesh pullback as a substitute bridge. No T0-T8 forcing step is discharged here; the declaration is local gravity-analysis hygiene for the 4D Regge continuum campaign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.