Gravity Seven Gaps Zq Shell Balance Blocker Exact Shell Amplitude Shell Constant

The shell constant obstruction

In the Recognition Science framework's work on gravity, the ledger (a discrete record of events) organizes paths into shells indexed by complexity. A phase assigns a real number to each path in each shell. The declaration exactShellAmplitude_shellConstant is a theorem about a special kind of phase: one that is constant inside each shell, meaning every path in a given shell gets the same phase value. The theorem states that for such a phase, the exact shell amplitude at complexity n equals the shell mass times a complex exponential of that shared phase.

This identity is a precise bookkeeping statement. The shell amplitude is the sum of complex contributions from all paths in a shell, each contribution weighted by the phase. When the phase is constant, that sum factors: the shell mass (the total weight of the shell) multiplies a single complex number determined by the common phase. The proof is a direct computation: it unfolds the definitions of shell amplitude and shell mass, then uses the constancy assumption to pull the common exponential out of the sum.

The theorem's importance is negative. A separate result, shellConstant_not_oscillatoryTail, shows that a phase constant inside each shell cannot satisfy the uniform tail condition OscillatoryTail, which requires the norm of shell amplitudes to tend to zero over contiguous blocks. The reason is that the norm of the shell amplitude for a constant phase is exactly the shell mass, and the shell mass is known to grow without bound. So the amplitude cannot vanish, no matter how the shared phase varies with complexity.

In Recognition Science, this theorem is a blocker certificate for a specific gap in the gravity program. It isolates what is missing to complete a phase-balance obligation: genuine asymptotic intra-shell balance, meaning amplitudes that tend to zero within each late shell. The theorem does not claim that such balance is impossible; it shows that a phase constant inside shells is too rigid to provide it. The framework's library proves this with no unproved assumptions, no added axioms, and no gaps in the formal proof.

/-- For a shell-constant phase, the full shell amplitude is its positive
shell mass times one common unit phase. No intra-shell cancellation occurs. -/
theorem exactShellAmplitude_shellConstant
    {phase : ∀ n : ℕ, ExactPathClass n → ℝ}
    (hconst : ShellConstant phase) (n : ℕ) :
    exactShellAmplitude phase n =
      (shellMass n : ℂ) *
        Complex.exp (Complex.I * (phase n (isolatedClass n) : ℂ)) := by
  unfold exactShellAmplitude shellMass
  rw [Complex.ofReal_sum, Finset.sum_mul]
  refine Finset.sum_congr rfl fun c _ => ?_
  rw [hconst n c]

/-- **COMPLEXITY-PHASE NO-GO.** Any phase that only sees shell complexity
fails `OscillatoryTail`, regardless of how its common shell phase varies. -/
theorem shellConstant_not_oscillatoryTail
    (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
    (hconst : ShellConstant phase) :
    ¬ OscillatoryTail phase := by
  intro htail
  exact shellConstant_not_shellAmplitudeVanishes phase hconst
    (oscillatoryTail_implies_shellAmplitudeVanishes phase htail)

/-- The norm of a shell-constant amplitude is exactly the shell mass. -/
theorem norm_exactShellAmplitude_shellConstant
    {phase : ∀ n : ℕ, ExactPathClass n → ℝ}
    (hconst : ShellConstant phase) (n : ℕ) :
    ‖exactShellAmplitude phase n‖ = shellMass n := by
  rw [exactShellAmplitude_shellConstant hconst n, norm_mul,
    Complex.norm_real, Real.norm_eq_abs, abs_of_pos (shellMass_pos n),
    Complex.norm_exp_I_mul_ofReal, mul_one]

What this page does not claim

The theorem does not claim that a phase constant inside each shell is the only obstruction to the uniform tail condition. The theorem does not claim that genuine asymptotic intra-shell balance is impossible or that the gravity gap is closed. The theorem makes no statement about mesh refinement or any geometric-continuum limit.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/ZqShellBalanceBlocker.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: