Pith. sign in
def

wrongMeshPowerWeight

definition
show as:
module
IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight
domain
Gravity
line
438 · github
papers citing
none yet

plain-language theorem explainer

Frozen decoy weight that assigns mesh side N the continuum-style factor N^{-2} instead of the 4-torus action-density factor N^{-4}. Continuum symbol normalization scales like 1/momentumNormSq ~ 1/N^2; quadrature density uses 1/N^4. Preflight and continuum-limit authors cite it as Decoy D3 so the two powers cannot be silently conflated. One-line real definition, no proof content.

Claim. For each natural number $N$, the wrong mesh-power weight is the real number $(N^{-1})^2 = N^{-2}$.

background

The Regge 4D continuum preflight module freezes the independent weak-field Einstein-Hilbert target, the canonical periodic Freudenthal 4-torus mesh of side $N \ge 3$, normalized TT data, pure-gauge family, and named honesty decoys before any continuum Tendsto argument. Nothing in the module proves continuum recovery of EH.

Two distinct $N$-scalings appear in the campaign. Continuum symbol normalization divides by momentum-norm squared, which on the torus family behaves like $1/N^2$. The 4-torus action-density quadrature instead carries weight $1/N^4$. Conflating those powers is a frozen error class (Decoy D3).

Sibling objects in the same file include the correct torus density weight, momentum-norm identities, and the canonical Freudenthal torus carrier against which later discriminators fire.

proof idea

Pure definition: cast $N$ to $\mathbb{R}$, take the multiplicative inverse, and square. No lemmas, tactics, or hypotheses. Downstream inequality theorems unfold this abbreviation and compare it to the correct $N^{-4}$ density weight by elementary arithmetic.

why it matters

Honesty decoy in the first binding increment of the 4D continuum closure plan. Parent theorems decoy_wrong_mesh_power and the concrete side-$N=3$ witness prove the weight differs from the correct torus density weight for all $N \ge 2$. torusDensityWeight_ne_wrong re-exports the same separation on the continuum-limit side. adversarial_decoys_still_hold keeps the decoy bank live while the still-open S_RS_converges_EH_4d and continuum Tendsto targets remain uninhabited.

The module contract forbids reverse-engineering lattice weights from the EH answer: the EH quadratic is frozen independently, and algebraic closers must observe equality rather than fit a scale. This decoy locks the mesh-power mistake so a later fitted $1/N^2$ cannot pass as continuum density weight. Framework role is local to the Regge gravity analysis stack (D=3 spatial plus time on the 4-torus), not a T0-T8 forcing step.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.