module module moderate

`IndisputableMonolith.Gravity.Analysis.FreudenthalEnergyLimit`

Module for the action-level continuum energy limit on the canonical Freudenthal family, using the fixed nonconstant C² witness f(p)=sin(2π p₀) on ℝ³. Gravity analysts cite it for the Phase 2b panel-locked Test G stage-2 companion to the stencil preflight. Argument structure pairs exact stencil identities with spectral-convergence estimates to identify the continuum quadratic energy density.

claimOn $\mathbb{R}^3$, fix the nonconstant $C^2$ witness field $f(p)=\sin(2\pi p_0)$. The module constructs the associated continuum energy target, proves positivity and sampling identities, and identifies the quadratic energy density of the frozen Freudenthal stencil action in the continuum limit.

background

Recognition Science gravity analysis treats discrete quadratic energies on the Freudenthal family and asks for their continuum limits as mesh parameters refine. The companion module FreudenthalStencilPreflight supplies the exact general-$N$ stencil identity and moment tensor for the frozen quadratic action (QG full-theory campaign, Phase 2b, panel-locked Test G stage 1, tensor-first anisotropic action continuum limit).

This module is the stage-2 companion: it introduces a concrete nonconstant $C^2$ witness $f(p)=\sin(2\pi p_0)$ on $\mathbb{R}^3$, samples it on the lattice, and compares discrete energy densities to a continuum target. SpectralConvergence supplies the quantitative eigenvalue-limit toolkit used to control the passage from discrete spectra to continuum quadratic forms.

Local objects include the witness field and its gradient sections, a continuum energy target with a positivity lemma, and an identity equating the witness energy density to an explicit trigonometric integral (e.g. integrals of $\cos^2(2\pi\cdot)$).

proof idea

Definition-heavy analysis module, not a single theorem. It fixes the witness $f(p)=\sin(2\pi p_0)$, proves sampling and nonconstancy lemmas, establishes sectionwise differentiability via standard derivative facts for $\sin$ of a linear form, defines the continuum energy target and shows it is positive, then equates the discrete witness energy density to that target by combining the Freudenthal stencil identity (from the preflight import) with explicit trigonometric integrals and spectral-convergence comparison lemmas.

why it matters in Recognition Science

Closes stage 2 of the panel-mandated continuum-limit campaign for the frozen quadratic Freudenthal energy: stencil preflight alone gives algebraic identities; this module supplies a concrete nonconstant witness and the energy-density identification needed to claim an action-level continuum limit. Downstream consumers are not yet wired in-tree (no used_by edges), but the module is scoped as the stage-2 companion to FreudenthalStencilPreflight inside the QG full-theory Phase 2b Test G track. It sits in the gravity analysis layer that underwrites continuum recovery of effective gravitational kinetics from discrete recognition structure, without yet claiming the full Einstein or Newtonian limit.

scope and limits

Does not prove a full continuum limit for arbitrary fields, only the fixed sinusoidal witness.
Does not derive Einstein or Newtonian gravity; scoped to frozen quadratic Freudenthal energy density.
Does not remove panel scope restrictions stated in the stencil preflight companion.
Does not assert spectral completeness beyond what SpectralConvergence already provides.
Does not wire downstream consumers; used_by is currently empty.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.FreudenthalStencilPreflight module_import
IndisputableMonolith.Gravity.Analysis.SpectralConvergence module_import

declarations in this module (28)

def witnessField L71
def sample L75
def witnessSample L79
theorem sample_witnessField L82
theorem witnessField_nonconstant L89
def witnessGrad L106
theorem hasDerivAt_sin_const_mul L109
theorem witnessField_section_hasDerivAt L116
def continuumTarget L132
theorem continuumTarget_pos L136
theorem witness_energy_density_eq L143
theorem integral_cos_sq_two_pi L153
theorem integral_witness_energy_density L187
theorem witnessSample_addBit_true L210
theorem stencil_inner_sum_witness L229
theorem sum_cos_shifted_vanishes L244
theorem sum_range_sq_sinDiff L300
theorem freudenthalStencilEnergy_witness L354
theorem scaledCanonicalEnergy_witness_closed_form L397
def rateConstant L411
theorem rateConstant_nonneg L413
theorem witness_closed_form_dist L423
theorem scaledCanonicalEnergy_witness_rate L449
theorem freudenthal_witness_energy_limit L468
theorem freudenthal_witness_energy_rate_integral_form L478
theorem witness_closed_form_tendsto L491
structure EnergyLimitStatus L511
def energyLimitStatus L528