OneD/JFunctionQuartic: full-line J-function asymptotic for K = w^4/24 (Tide E4)#18
Merged
Conversation
Tide step E4 (Grammar J-function for single-component blow-up,
Step 2 of the grammar paper precursor sequence). Two theorems:
- `quartic_jfunction_centered_tendsto_zero` (Candidate X, the DCT
core): for `prior : ℝ → ℝ` continuous and globally bounded,
Tendsto (fun t => t^(1/4) · ∫ exp(-tw^4/24) · (prior(w) − prior(0)) dw)
atTop (𝓝 0).
- `quartic_jfunction_asymptotic` (Candidate A, the user-facing
form, derived as a 2-line corollary):
Tendsto (fun t => t^(1/4) · ∫ exp(-tw^4/24) · prior(w) dw)
atTop (𝓝 (prior(0) · (1/2) · 24^(1/4) · Γ(1/4))).
Step-2 deliberation (with GPT-5.5 Pro) chose the centered form X
over the direct form A as the formalisation target — same DCT
core, less algebra in the statement, and the user-facing form
drops out by `quartic_partition` (Tide 7's closed form for the
no-prior partition).
Hypothesis class. The deliberation chose `AEMeasurable π` +
`ContinuousAt π 0` + global bound; the formalisation here uses
the slightly stronger `Continuous prior` + global bound for
tractability (avoids the AEMeasurable.comp_quasiMeasurePreserving
plumbing for ~50 lines saved). The mathematically-minimal hypothesis
weakening is recorded as a follow-up.
Proof structure. Substitute `u = t^(1/4) · w` via
`Measure.integral_comp_mul_right`; the Jacobian `|t^(-1/4)|`
cancels the `t^(1/4)` prefactor and the integrand becomes
`exp(-u^4/24) · (prior(u/t^(1/4)) - prior(0))` — t-independent
modulo the prior shift. DCT with envelope `2M · exp(-u^4/24)`
(integrable by `quartic_integrable_pow 0`) and pointwise limit
`0` (by `Continuous prior`) closes.
Numerical sanity: 3 priors verified against scipy.integrate.quad
to machine precision (π=1 exact, others convergent at O(t^(-1/4))).
Tide log: sri/projects/primer/tide-log/2026-05-07-tide-grammar-j-function.md
GPT consult: sri/projects/primer/tide-log/gpt55_tide_grammar_j_function_v1.md
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Narrative-LaTeX retrospective for today's E4 Tide step (J-function asymptotic for the quartic, Step 2 of the grammar paper precursor sequence). Seven mandatory sections per the per-tide template. Highlights: - The Step-2 deliberation (with GPT-5.5 Pro) reshaped the target from the direct form (Candidate A) to the centred form (X); this was load-bearing — same DCT core, cleaner statement, the user-facing form falls out by `quartic_partition`. - First Tide running fully under the K1 worktree-isolation discipline (landed earlier today). Zero collisions despite four other Tide branches active concurrently. Worktree pays off immediately. - Hypothesis weakened to `Continuous prior` from the deliberation's `AEMeasurable + ContinuousAt 0`; the AEMeasurable case adds ~50 lines of comp_quasiMeasurePreserving plumbing that's a separate follow-up. Both forms cover all paper applications. - Three new CLAUDE.md gotchas surfaced: π-as-binder issue, tendsto_rpow_atTop namespace inconsistency, and the ∀ᶠ.symm dot-notation gotcha. Tide log: sri/projects/primer/tide-log/2026-05-07-tide-grammar-j-function.md Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
# Conflicts: # Laplace.lean
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Tide E4 (Grammar paper J-function for single-component blow-up, Step 2 of the grammar precursor sequence). Two theorems committed in a new file
Laplace/OneD/JFunctionQuartic.lean:quartic_jfunction_centered_tendsto_zero(the centred DCT headline, GPT-reshaped from the direct form):quartic_jfunction_asymptotic(the user-facing form, derived as a 2-line corollary):Hypothesis class:
Continuous prior+ global bound (slightly stronger than the deliberation'sAEMeasurable + ContinuousAt 0; the weakening is a recorded follow-up that adds ~50 lines ofcomp_quasiMeasurePreservingplumbing).Proof structure:
u = t^(1/4) · wviaMeasure.integral_comp_mul_right.2M · exp(-u^4/24)(integrable by Tide 7'squartic_integrable_pow 0) and pointwise limit 0.prior = (prior - prior(0)) + prior(0); constant piece evaluated byquartic_partition.280 lines, 0 sorry / 0 axiom / 0 native_decide. Single-session formalisation, one GPT consult during deliberation, no GPT consults during proof.
Tide artefacts
sri/projects/primer/tide-log/2026-05-07-tide-grammar-j-function.mdsri/projects/primer/tide-log/gpt55_tide_grammar_j_function_v1.mdlean/laplace/retrospectives/2026-05-07-tide-grammar-j-function.texFirst Tide under K1 worktree isolation
This Tide ran fully under the just-landed
tide-worktreewrapper: dedicated worktree atsri/lean/laplace-tide-grammar-j-function/, branched offmainatf21a9cc. Zero collisions despite four other Tide branches active concurrently.Test plan
lake build Laplace.OneD.JFunctionQuarticcleanlake buildcleanscripts/sorriesreports 0 sorry / 0 axiom / 0 native_decide🤖 Generated with Claude Code