decoy_arbitrary_pullback_excluded
plain-language theorem explainer
Arbitrary test-variation pullbacks are frozen out of the 4D continuum action theorem: only a Recognition-native mesh bridge may inhabit continuum EH recovery. Gravity continuum-closure authors cite this as honesty decoy D4. The proof is the one-line term `trivial`, because the exclusion proposition is defined as `True`.
Claim. Decoy D4 holds: arbitrary response-level test-variation pullbacks are excluded from the continuum action theorem. Continuum recovery of the Einstein-Hilbert quadratic on the 4D Regge mesh may not be inhabited by a bare pullback hypothesis; a Recognition-native mesh bridge is required.
background
This module is the first binding increment of the QG 4D continuum closure plan. It freezes the independent weak-field Einstein-Hilbert target, the canonical periodic Freudenthal 4-torus mesh ($N \ge 3$), Frobenius-normalized Euclidean TT data, the pure-gauge family, and a list of honesty decoys before any continuum limit is proved. Nothing in the module establishes continuum recovery.
Decoy D4 records a methodological exclusion: response-level test-variation pullback hypotheses do not count as a proof that the Recognition Science discrete action converges to the frozen EH quadratic. The closer is required to go through a Recognition-native mesh bridge (exact flat cross-term symbol, $|k|^2$-normalized TT match, gauge vanishing), not an arbitrary continuum pullback of test variations.
The exclusion proposition is literally True. That is intentional bookkeeping: the decoy is a frozen policy flag in the preflight layer, not a nontrivial dynamical statement.
proof idea
The referenced proposition ArbitraryPullbackExcluded is defined as the true proposition. The theorem is therefore a one-line term proof by trivial. No lemmas about Regge symbols, Bloch folds, or Hessians are invoked.
why it matters
In the preflight contract, decoy discriminators sit beside Frobenius pin lemmas and status flags as THEOREM-tier objects that keep later continuum work honest. Downstream, RecognitionMeshExactJBridge4D.decoy_pullback_excluded re-exports this flag so the mesh-bridge layer inherits the same exclusion: arbitrary pullbacks remain out of scope while the exact-$J$ bridge is assembled.
The module doc is explicit that continuum Tendsto targets (Regge4DContinuumEHTarget, gauge-zero) and S_RS_converges_EH_4d remain open, and that discrete bookkeeping identities must not be mistaken for geometric continuum proofs. D4 blocks a common shortcut that would inhabit the action theorem with a response-level pullback instead of observing equality of the independently frozen EH quadratic against the lattice symbol. It does not itself close continuum recovery; it only freezes what may not count as a closer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.