From aac17e6e34455aaa6b06bfd498db9fe3989a4eb2 Mon Sep 17 00:00:00 2001 From: allaun Date: Fri, 31 Jul 2026 04:31:36 -0500 Subject: [PATCH] docs(p28): recast the method document as a route narrative Renames THE_ENCODER_APPROACH.md -> HOW_THE_SOLUTION_WAS_FOUND.md and rewrites it to answer the question a reader actually has -- why these moves -- rather than arguing for novelty. Removed: all self-assessment of distinctiveness. Replaced with a plain statement of the relevant standard practice (PSLQ/LLL, Inverse Symbolic Calculator; canonical numeration systems, base-k recognisable sets, Cobham) so a reader can place the work without being told what to think of it. The narrative now explains each move that looks arbitrary in isolation: - why the seed data was treated as generated rather than given - why a bijective codec was needed first, which is what the Radix framing and DFA canonicalisation work is for - why the Pascal basis was not a search: the matrix's own second row (-u^3, -3u^2, -3u, -1) is a signed Pascal row, visible before any fitting - what decoded (A, B, S) and why exact agreement makes it evidence - how A, B factor through s2(tau_163) to reduce the problem to one CM value - why the encoding is only a lead, with the proof built independently - why the deformation r = 1/x exists: without it there is no contour Adds a 'What did not work' section recording the three closed routes with their witnesses (t-line intertwiner impossibility, L_U monodromy exclusion, Sym^2 V set aside), since the indirectness of the final route is explained by them. Retains the honest limits: 3.54x is not compression, and the claim should be rejected. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01WY6SfRYvm8zFKMX9GcjS8u --- .../submission/HOW_THE_SOLUTION_WAS_FOUND.md | 207 ++++++++++++ .../submission/THE_ENCODER_APPROACH.md | 317 ------------------ .../all_four_columns_certificate.sage.py | 147 ++++++++ .../p28_kernel_contiguity_certificate.sage.py | 214 ++++++++++++ ...p28_lattice_hypotheses_certificate.sage.py | 130 +++++++ 5 files changed, 698 insertions(+), 317 deletions(-) create mode 100644 experiments/ramanujan_28/submission/HOW_THE_SOLUTION_WAS_FOUND.md delete mode 100644 experiments/ramanujan_28/submission/THE_ENCODER_APPROACH.md create mode 100644 experiments/ramanujan_28/submission/certificates/all_four_columns_certificate.sage.py create mode 100644 experiments/ramanujan_28/submission/certificates/p28_kernel_contiguity_certificate.sage.py create mode 100644 experiments/ramanujan_28/submission/certificates/p28_lattice_hypotheses_certificate.sage.py diff --git a/experiments/ramanujan_28/submission/HOW_THE_SOLUTION_WAS_FOUND.md b/experiments/ramanujan_28/submission/HOW_THE_SOLUTION_WAS_FOUND.md new file mode 100644 index 0000000..38a4a98 --- /dev/null +++ b/experiments/ramanujan_28/submission/HOW_THE_SOLUTION_WAS_FOUND.md @@ -0,0 +1,207 @@ +# How the solution was found + +## Why this document exists + +The finished proof takes an indirect route. Read cold, several of its moves look +arbitrary: why deform a fixed integer into a free variable, why re-express the +initial conditions in a Pascal basis, why there is machine-checked work on +leading zeros in positional notation sitting underneath a modular-forms problem. + +Each was forced by something. This document records the path so the choices can +be read as reasoning rather than guessed at. + +## The starting position + +The challenge supplies, for Problem 2.8: + +- a `4×4` matrix `M(n)` whose entries are degree-5 polynomials in `u = 2n+3` + over a constant `R = 151931373056001`; +- one entry containing the bare integer `236337691420383`, unexplained; +- two initial rows of eight integers of up to 77 bits; +- the conjecture `lim P_{N,j}/Q_{N,j} = √10005/π` for all four columns. + +`√10005/π` identifies the target immediately — it is the Chudnovsky constant. +What is not given is any link between *this recurrence* and that formula. The +recurrence came from machine search; nothing in its presentation records where +it came from. + +## Step 1 — treat the given data as generated, not as given + +The eight seed integers are not round, not obviously related, and too large to +read. But they were *produced by something*. A search process emitted them, so a +generator exists, and a generator is usually much smaller than its output. + +That reframes the first task: not "prove a limit" but "recover the generator." +The rest follows from taking that seriously. + +## Step 2 — recovering a generator requires a codec, and radix notation is not one + +To hunt for structure by re-encoding data, encode and decode must be inverse. +That sounds automatic and is not. + +Ordinary positional notation is **not injective on digit strings**. Two +collisions, machine-checked in Coq and Lean +(`coq/MathPunchFiniteStateAudit/Radix.v`, `MathPunchFiniteState/Radix.lean`): + +```coq +eval_digits 8 [0; 1] = eval_digits 8 [1] (* both = 1: leading zero *) +eval_digits 8 [] = eval_digits 8 [0] (* both = 0: empty word *) +``` + +In base 8 over lengths 0–3, 585 distinct digit strings collapse onto 512 values. + +This is invisible in ordinary mathematics, where numerals exist only to *denote +numbers* — `[0,1]` and `[1]` denote the same number and there is nothing more to +say. It is fatal when digit strings encode objects, because the decode is then +not a function. + +Two repairs, both **bijections onto correctly stated codomains**: + +``` +framing: digit strings ⟷ ⋃ₙ {n} × [0, bⁿ) + framed_value b ds = (length ds, eval_digits b ds) + +DFA: canonical numerals ⟷ ℕ⁺ + three states start / body / dead; rejects leading zeros, + out-of-range digits, and the empty word +``` + +Bijectivity rather than injectivity is what is needed: injectivity says +encodings do not collide, bijectivity says **decoding is total**. A codec is +used in the decode direction. + +That is why numeration-system work sits under a modular-forms problem. It is the +correctness obligation for Step 3, not a digression. + +## Step 3 — the basis came from the matrix, not from a search + +Re-encoding is only evidence if the basis is fixed *before* looking. Otherwise +enough freedom makes any data look structured. + +The basis was not searched for. The second row of the challenge's own matrix is + +``` +(−u³, −3u², −3u, −1) +``` + +a signed Pascal row. That is a property of the given data, visible before any +fitting. So the candidate basis was the rows of the lower-triangular Pascal +matrix: + +``` +b₀ = (1,0,0,0) b₁ = (1,1,0,0) b₂ = (1,2,1,0) b₃ = (1,3,3,1) +``` + +One candidate, taken from the problem statement, tried once. + +## Step 4 — what came out + +In that basis, with `C(x) = (18/x)b₃ + (5/4)b₀ + (23/2)b₁ + 27b₂`, the two seed +rows are **exactly** + +``` +A₁ = S·C +A₀ = A·C − (5/4)·H₀, H₀ = A·b₀ + B·b₁ +``` + +with + +``` +A = 13591409 B = 545140134 S = 426880 +``` + +These were not solved for. They are the Chudnovsky constants, already fixed by a +classical formula in an unrelated context. They had to come out exactly right or +the encoding fails, which is what makes this evidence rather than coincidence. + +The unexplained integer resolved at the same time: +`236337691420383 = (14R − 567)/9`. + +Verified exactly in `p28_official_object_certificate.py`. + +## Step 5 — from constants to a single unknown + +The recovered constants keep factoring. With `s₂(τ₁₆₃) = 77265280/90856689`, the +weight-zero CM invariant: + +``` +A = den(s₂) − num(s₂) +B = 6·den(s₂) +A/B = (1 − s₂)/6 +``` + +So the arithmetic content of the problem is one CM value. The target became +"connect this recurrence to a known modular quantity" instead of "prove a limit +about an opaque recurrence" — a better-posed question. + +## Step 6 — the encoding proves nothing, and the proof was built separately + +A decode is a lead. It says where to look; it establishes nothing. The finished +argument does not cite the Pascal form as evidence and does not infer equality +from numerical agreement. It proceeds through the deformation, the Ore +factorisations, the terminating `₄F₃`, the discrete-valuation induction, and an +explicit stable-graph contraction, importing exactly one external theorem: the +classical Chudnovsky identity, cited to Milla's derivation. + +The deformation `r = 1/x` is the other move that looks strange cold. Its purpose +is to make analytic methods available: replacing the fixed constant `R` by a free +variable gives a one-parameter family to which Cauchy's theorem applies, and +`x₀ = 1/R` specialises it back to the official object. Without the deformation +there is no contour to integrate around. + +## What did not work + +The route is indirect because the direct ones were closed, each with a witness +rather than an impression: + +- **The t-line intertwiner route** was proved impossible — `sing(L) = {0,∞}`, + and three disjoint fibres over `0,1,∞` cannot inject into two points. Recorded + with its ramification argument and scoped to the whole gauge-equivalence class. +- **The `L_U` variant** was excluded by monodromy: no regular-unipotent `3×3` + block exists anywhere in the relevant family. +- **The `Sym²V` construction** was set aside as disproportionate. It is a + research-scale object, and the Apéry-limit evaluation does not need an explicit + module isomorphism. + +Recording exclusions as first-class results, with witnesses, is what stopped the +search from cycling back through settled ground. + +## Limits of the method + +**The encoding is not compression.** Measured: + +| | bits | +|---|---| +| raw seed data (8 integers) | 588 | +| encoder payload (`A, B, S, R` + 9 small Pascal coordinates) | 166 | +| ratio | 3.54× | + +3.54× is unremarkable, and the basis had to be known in advance. Any claim that +this compresses data should be rejected. The same conclusion was reached +elsewhere in this programme: characteristic-polynomial encoding of matrices adds +overhead against an entropy-coded baseline. + +The value is not the size of the encoding but *which* basis makes the +coordinates meaningful, which is a statement about where the data came from. + +**Relation to standard practice.** Recovering closed forms from numerical data +is established: integer-relation algorithms (PSLQ, LLL), the Inverse Symbolic +Calculator, and experimental mathematics generally — PSLQ is used directly here +to identify `s₂` across Heegner discriminants. The regular structure of valid +numerals is likewise classical: canonical numeration systems, base-`k` +recognisable sets, Cobham's theorem. What this work does is apply those to +structured integer arrays rather than single constants, and keep the result in +the proof as a provenance record rather than discarding it after discovery. + +## The path in one view + +``` +opaque official integers + → assume generated; hunt the generator + → build a bijective codec (radix framing / DFA canonicalisation) + → basis taken from the matrix's own Pascal row + → decode yields the Chudnovsky constants A, B, S + → constants factor through the CM invariant s₂(τ₁₆₃) + → problem reduces to one modular quantity + → prove that reduction independently; import Chudnovsky as a cited theorem +``` diff --git a/experiments/ramanujan_28/submission/THE_ENCODER_APPROACH.md b/experiments/ramanujan_28/submission/THE_ENCODER_APPROACH.md deleted file mode 100644 index 03eba41..0000000 --- a/experiments/ramanujan_28/submission/THE_ENCODER_APPROACH.md +++ /dev/null @@ -1,317 +0,0 @@ -# The encoder approach - -## What it is - -Given opaque numerical data — here, the eight large integers the challenge -supplies as initial conditions — re-express them **exactly** in a fixed, -structured basis chosen in advance. Then read the coordinates. - -If the coordinates turn out to be small, or turn out to be constants with -independent meaning, that is evidence about where the data came from. The -encoding is treated as a **receipt of provenance**, not as a compression scheme. - -## The concrete instance in this submission - -The challenge states Problem 2.8's initial conditions as two rows of large -integers: - -``` -A = (37169305760442252761441, 111507917281327441564208, - 111507917281327599720129, 37169305760442410917362) -B = (1167416361542639692320, 3502249084627896132160, - 3502249084627879697280, 1167416361542622723840) -``` - -Nothing about these suggests structure. They are 8 integers of up to 77 bits. - -Fix the four rows of the lower-triangular Pascal matrix - -``` -b0 = (1,0,0,0) b1 = (1,1,0,0) b2 = (1,2,1,0) b3 = (1,3,3,1) -``` - -and the single row - -``` -C(x) = (18/x)·b3 + (5/4)·b0 + (23/2)·b1 + 27·b2 - = (18/x + 159/4, 54/x + 131/2, 54/x + 27, 18/x). -``` - -Then, at `x_0 = 1/R`, **exactly**: - -``` -A_1 = S·C -A_0 = A·C − (5/4)·H_0, H_0 = A·b0 + B·b1 = (A+B, B, 0, 0) -``` - -with - -``` -A = 13591409, B = 545140134, S = 426880. -``` - -These are not fitted parameters. They are **the Chudnovsky constants** — the -same `A`, `B`, `S` appearing in - -``` -1/π = (12 / 640320^{3/2}) · Σ_k (6k)!/((3k)!(k!)^3) · (A + Bk) · (−640320^{−3})^k. -``` - -Verified exactly in `p28_official_object_certificate.py`. - -## What the encoding revealed - -The coordinates are not merely small — they are arithmetically meaningful, and -they continue to factor: - -``` -s_2(τ_163) = 77265280 / 90856689 (the weight-zero CM invariant) - -A = 90856689 − 77265280 = den(s_2) − num(s_2) -B = 6 · 90856689 = 6 · den(s_2) -A/B = (1 − s_2)/6 -``` - -All three verified exactly. So the chain runs - -``` -opaque official integers - → Pascal-basis coordinates - → Chudnovsky constants A, B, S - → the CM invariant s_2(τ_163) - → the modular origin of the problem -``` - -The encoder did not *prove* anything here. It **located** the structure, which -then told the proof where to go. That is its actual function. - -## What it is NOT: an honest accounting - -**It is not a compressor.** Measured directly: - -| | bits | -|---|---| -| raw official seed data (8 integers) | 588 | -| encoder payload (`A, B, S, R` + 9 small Pascal coordinates) | 166 | -| ratio | **3.54×** | - -3.54× is unremarkable. A general-purpose entropy coder would do comparably on -data this small, and the Pascal basis had to be known in advance. **Any claim -that this approach compresses data should be rejected**, including by the -author. The same conclusion was reached independently elsewhere in this -programme: characteristic-polynomial encoding of matrices *adds* overhead -relative to an entropy-coded baseline. It is a receipt, not a compressor. - -The value is entirely in *which* basis makes the coordinates meaningful — and -that is a statement about the data's origin, not about its entropy. - -## Why it is falsifiable rather than numerology - -The obvious objection is that with enough freedom, any basis can be tuned to -make any data look structured. Three constraints prevent that here: - -1. **The basis is fixed before looking.** Pascal rows are a canonical choice, - not searched over. -2. **The encoding is exact, not approximate.** No tolerance, no fitting; the - identities hold in `Fraction` arithmetic and fail if any coefficient is - perturbed by one unit. -3. **The recovered coordinates have independent meaning.** `A`, `B`, `S` were - not free parameters to be solved for — they were already known constants from - a different context (Chudnovsky's series), and they had to come out *exactly - right* or the encoding fails. - -Criterion 3 is what separates this from numerology. A coincidence is cheap when -the target is unconstrained; here the target was pinned in advance by an -unrelated classical formula. - -## How distinctive is this, honestly - -The user's sense that this is unusual is **partly right, and worth stating -precisely rather than overclaiming.** - -**Established precedent.** Recovering closed forms from numerical data is a -mature field: integer-relation algorithms (PSLQ, LLL), the Inverse Symbolic -Calculator, and experimental-mathematics practice generally. Finding that a -constant equals a combination of known constants is routine. This work uses PSLQ -directly elsewhere (e.g. to identify `s_2` across Heegner discriminants). - -**What is less standard here:** - -- The target is **structured integer data** (seed rows, matrix entries) rather - than a single real constant. Integer-relation tools are usually pointed at one - number at a time; here an entire row must decode simultaneously in one basis. -- The encoding is used as a **provenance argument** feeding a proof, not as a - discovery heuristic to be discarded once the answer is known. The compact form - survives into the manuscript because it is what makes the seed rows tractable. -- The basis is chosen for **structural** reasons (Pascal ↔ the binomial structure - of the transfer matrix's second row `(−u³, −3u², −3u, −1)`), not by search. - That second row *is* a signed Pascal row, which is why the Pascal basis was the - natural guess and not a lucky one. - -**Fair summary:** the technique is a disciplined, exact-arithmetic variant of -established inverse-symbolic practice, distinguished mainly by being applied to -structured integer arrays and by being carried into the proof as a provenance -receipt rather than dropped after discovery. Calling it "unique" would be too -strong; calling it a recognisable method used unusually systematically is -defensible. - -## The radix layer: why a codec needs more than positional notation - -Everything above assumes objects can be written as digit strings and read back. -That assumption fails for ordinary positional notation, and repairing it is the -part of this approach with the strongest claim to being non-standard. - -**Formulation, from MathPunch-FiniteState** (`coq/MathPunchFiniteStateAudit/Radix.v`, -mirrored in `MathPunchFiniteState/Radix.lean`): - -```coq -Fixpoint eval_digits (base : nat) (digits : list nat) : nat := - match digits with - | [] => 0 - | digit :: rest => digit * Nat.pow base (length rest) + eval_digits base rest - end. - -Definition framed_value (base : nat) (digits : list nat) : nat * nat := - (length digits, eval_digits base digits). -``` - -### The defect, proved rather than asserted - -Positional evaluation is **not injective on digit strings**. Two collisions are -machine-checked in both Coq and Lean: - -```coq -Example ordinary_radix_leading_zero_collision : - eval_digits 8 [0; 1] = eval_digits 8 [1]. (* both = 1 *) - -Example empty_word_and_zero_symbol_collide_unframed : - eval_digits 8 [] = eval_digits 8 [0]. (* both = 0 *) -``` - -This is invisible in ordinary mathematics, where radix notation exists only to -*denote numbers* — `[0,1]` and `[1]` denote the same number and there is nothing -more to say. It becomes fatal the moment digit strings are used as a **codec for -objects**, because distinct objects then encode to the same numeral. - -Quantified in base 8 over lengths 0–3: **585 distinct digit strings collapse -onto 512 distinct values.** 73 strings are destroyed. - -### Two repairs, both in the source - -**1. Framing** — adjoin the length: - -```coq -Example framing_repairs_leading_zero_collision : - framed_value 8 [0; 1] <> framed_value 8 [1]. (* (2,1) vs (1,1) *) - -Example framing_separates_empty_word_and_zero_symbol : - framed_value 8 [] <> framed_value 8 [0]. (* (0,0) vs (1,0) *) -``` - -Framing is not merely injective — it is a **bijection**, onto the correctly -stated codomain: - -``` -framed_value_b : { digit strings over base b } ⟶ ⋃_n {n} × [0, b^n) -``` - -Verified exhaustively in base 8 for every length `n = 0..4`: the image is -*exactly* `{n} × [0, 8^n)`, with sizes 1, 8, 64, 512, 4096 — no collisions and no -gaps. (It is of course **not** surjective onto all of `ℕ × ℕ`: the pair `(1,100)` -is unreachable in base 8, since a length-1 string has value `< 8`. Stating the -codomain as `ℕ × ℕ` would make the map merely injective; stating it correctly -makes it bijective.) - -Bijectivity, not injectivity, is the property a codec needs. Injectivity alone -says encodings do not collide; bijectivity says **decoding is total** on the -valid codomain — every admissible framed pair is the image of exactly one -string, so the inverse map exists everywhere it should. - -**2. Canonicalisation by finite automaton** — restrict to a canonical language -instead of enlarging the codomain. `Radix.lean` carries a three-state DFA -(`start`, `body`, `dead`) that rejects a leading zero at the `start` state, -rejects out-of-range digits, and rejects the empty word: - -```lean -def radixDfaStep (base : Nat) : RadixState → Nat → RadixState - | .start, 0 => .dead -- leading zero - | .start, d => if d < base then .body else .dead - | .body, d => if d < base then .body else .dead - | .dead, _ => .dead -``` - -This too is a **bijection**, and the classical one: - -``` -{ DFA-accepted canonical numerals in base b } ⟷ ℕ⁺ -``` - -Verified exhaustively in base 8 up to length 5: 32767 canonical strings, 32767 -distinct values, forming *exactly* the interval `[1, 8^5)`. Note the codomain is -`ℕ⁺`, not `ℕ` — the empty word is rejected, so `0` has no canonical -representation in this language. That is a deliberate choice, and it is the -price of the narrowing repair. - -This is what the repository name *FiniteState* refers to. Framing widens the -target so nothing collides; the DFA narrows the source so nothing ambiguous is -admitted. Both yield bijections — onto `⋃_n {n} × [0, b^n)` and onto `ℕ⁺` -respectively — so they solve the same obligation from opposite directions, with -different codomains and different edge-case costs. - -### Why this matters to the encoder - -The encoder in Part 1 reads coordinates out of exact data. For that to be a -*codec* rather than a lossy summary, the map from strings to objects must be a -**bijection onto a stated codomain**. Injectivity alone is not enough: it would -guarantee that no two objects share an encoding, but not that an encoding can be -decoded — leaving the inverse partial and the codec unusable in the direction -that matters. Bijectivity gives a total decode. - -Without it, a recovered encoding does not determine what it came from, and "the -coordinates are meaningful" becomes unfalsifiable. The radix layer is the -correctness obligation underneath the whole method, and it is discharged by -proof rather than by convention. - -### How distinctive is this, honestly - -**Precedent exists.** That the set of valid numerals is a regular language, and -that leading zeros must be excluded for canonical numeration, is standard in -automata theory and the theory of numeration systems (base-`k` recognisable -sets, Cobham's theorem, and the usual treatment of canonical numeration systems -all depend on exactly this). The observation itself is not new. - -**What is less usual:** - -- Treating non-injectivity of radix notation as a **proof obligation of a - mathematical encoding pipeline**, rather than as a background convention. -- Discharging it in **two proof assistants** with explicit collision witnesses — - stating the defect as a proved `Example` rather than a remark. -- Carrying both repairs (framing *and* the DFA) side by side, so the encoder can - choose whether to widen the codomain or restrict the domain. - -**Fair summary:** the mathematical content is classical numeration-system -material; the distinctive move is making it an explicitly proved prerequisite of -an encoding method, with the collisions exhibited as theorems. That is a -methodological contribution, not a new theorem about numeration. - -### Maintenance hazard - -The DFA (`RadixState`, `radixDfaStep`, `radixDfaAccepts`) and `toDigits` exist -**only in the Lean file**; `Radix.v` has `eval_digits` and `framed_value` alone. -In this repository Lean is regenerated from `coq/*.v`, so a regeneration would -silently erase the automaton. Either port the DFA to Coq or exempt `Radix.lean` -from regeneration. - -## The general recipe - -1. Take opaque exact data. -2. Choose a basis for structural reasons, and fix it before looking. -3. Solve for coordinates in exact arithmetic. No tolerances. -4. Ask whether the coordinates are small, or known, or both. -5. If they are known constants from another context, you have found a provenance - link — treat it as a lead requiring proof, never as a proof. -6. Report the compression ratio honestly, and expect it to be unimpressive. - -Step 5 is the discipline that keeps this from becoming numerology. In this -submission the lead was `A/B = (1 − s_2)/6`, which reduced the whole problem to a -single CM value — and that reduction then had to be proved separately. diff --git a/experiments/ramanujan_28/submission/certificates/all_four_columns_certificate.sage.py b/experiments/ramanujan_28/submission/certificates/all_four_columns_certificate.sage.py new file mode 100644 index 0000000..b549b22 --- /dev/null +++ b/experiments/ramanujan_28/submission/certificates/all_four_columns_certificate.sage.py @@ -0,0 +1,147 @@ +#!/usr/bin/env sage +""" +Standalone exact certificate for the four-column reduction in Ramanujan +Challenge Problem 2.8. + +It certifies the algebraic part of the cyclic-frame lemma: + +* the exact balanced limit S; +* charpoly(S)=Q_R/R^2; +* an explicit left eigenvector w_rho; +* every coordinate of w_rho is positive at the exterior root; and +* the limiting cyclic frame [e1,S e1,S^2 e1,S^3 e1] is invertible. + +The analytic stable-graph contraction is proved equation by equation in the +main solution. This file is only an independent exact algebra cross-check; +it performs no irreducibility, polynomial-GCD, or numerical root decision. +""" + + +# This file was *autogenerated* from the file all_four_columns_certificate.sage +from sage.all_cmdline import * # import sage library + +_sage_const_151931373056001 = Integer(151931373056001); _sage_const_3 = Integer(3); _sage_const_2 = Integer(2); _sage_const_144 = Integer(144); _sage_const_5 = Integer(5); _sage_const_288 = Integer(288); _sage_const_4 = Integer(4); _sage_const_99 = Integer(99); _sage_const_333 = Integer(333); _sage_const_229 = Integer(229); _sage_const_114 = Integer(114); _sage_const_40 = Integer(40); _sage_const_64 = Integer(64); _sage_const_432 = Integer(432); _sage_const_864 = Integer(864); _sage_const_243 = Integer(243); _sage_const_909 = Integer(909); _sage_const_868 = Integer(868); _sage_const_80 = Integer(80); _sage_const_272 = Integer(272); _sage_const_153 = Integer(153); _sage_const_648 = Integer(648); _sage_const_860 = Integer(860); _sage_const_360 = Integer(360); _sage_const_1 = Integer(1); _sage_const_9 = Integer(9); _sage_const_63 = Integer(63); _sage_const_158 = Integer(158); _sage_const_168 = Integer(168); _sage_const_216 = Integer(216); _sage_const_36 = Integer(36); _sage_const_189 = Integer(189); _sage_const_316 = Integer(316); _sage_const_108 = Integer(108); _sage_const_54 = Integer(54); _sage_const_378 = Integer(378); _sage_const_948 = Integer(948); _sage_const_1008 = Integer(1008); _sage_const_384 = Integer(384); _sage_const_18 = Integer(18); _sage_const_45 = Integer(45); _sage_const_251 = Integer(251); _sage_const_1086 = Integer(1086); _sage_const_1384 = Integer(1384); _sage_const_576 = Integer(576); _sage_const_657 = Integer(657); _sage_const_1292 = Integer(1292); _sage_const_2064 = Integer(2064); _sage_const_1072 = Integer(1072); _sage_const_72 = Integer(72); _sage_const_702 = Integer(702); _sage_const_1069 = Integer(1069); _sage_const_2508 = Integer(2508); _sage_const_1512 = Integer(1512); _sage_const_180 = Integer(180); _sage_const_891 = Integer(891); _sage_const_1450 = Integer(1450); _sage_const_1116 = Integer(1116); _sage_const_1385 = Integer(1385); _sage_const_1422 = Integer(1422); _sage_const_6 = Integer(6); _sage_const_33 = Integer(33); _sage_const_58 = Integer(58); _sage_const_14 = Integer(14); _sage_const_32 = Integer(32); _sage_const_7 = Integer(7); _sage_const_0 = Integer(0); _sage_const_44 = Integer(44); _sage_const_96 = Integer(96); _sage_const_48 = Integer(48); _sage_const_17 = Integer(17); _sage_const_8 = Integer(8); _sage_const_12 = Integer(12); _sage_const_56 = Integer(56); _sage_const_262 = Integer(262); _sage_const_220 = Integer(220); _sage_const_105 = Integer(105); _sage_const_250 = Integer(250); _sage_const_217 = Integer(217); _sage_const_274 = Integer(274); _sage_const_233 = Integer(233); _sage_const_10 = Integer(10); _sage_const_23 = Integer(23); _sage_const_194 = Integer(194); _sage_const_28 = Integer(28); _sage_const_27 = Integer(27); _sage_const_71 = Integer(71); _sage_const_68 = Integer(68); _sage_const_198 = Integer(198); _sage_const_11 = Integer(11); _sage_const_128 = Integer(128); _sage_const_149 = Integer(149); _sage_const_43 = Integer(43) +from sage.all import * + +Pn = PolynomialRing(QQ, names=('n',)); (n,) = Pn._first_ngens(1) +Fn = Pn.fraction_field() +R = QQ(_sage_const_151931373056001 ) + + +def authoritative_matrix(u, R): + """Problem 2.8 transfer after 236337691420383=(14R-567)/9.""" + w = u*(_sage_const_3 *u-_sage_const_2 )*(_sage_const_3 *u+_sage_const_2 ) + + a1 = R*(_sage_const_144 *u**_sage_const_5 -_sage_const_288 *u**_sage_const_4 +_sage_const_144 *u**_sage_const_3 ) + (-_sage_const_99 *u**_sage_const_5 +_sage_const_333 *u**_sage_const_4 -_sage_const_229 *u**_sage_const_3 -_sage_const_114 *u**_sage_const_2 +_sage_const_40 *u+_sage_const_64 ) + a2 = R*(_sage_const_432 *u**_sage_const_4 -_sage_const_864 *u**_sage_const_3 +_sage_const_432 *u**_sage_const_2 ) + (-_sage_const_243 *u**_sage_const_4 +_sage_const_909 *u**_sage_const_3 -_sage_const_868 *u**_sage_const_2 -_sage_const_80 *u+_sage_const_272 ) + a3 = R*(_sage_const_432 *u**_sage_const_3 -_sage_const_864 *u**_sage_const_2 +_sage_const_432 *u) + (-_sage_const_153 *u**_sage_const_3 +_sage_const_648 *u**_sage_const_2 -_sage_const_860 *u+_sage_const_360 ) + a4 = R*_sage_const_144 *(u-_sage_const_1 )**_sage_const_2 + + b1 = R*(-_sage_const_144 *u**_sage_const_3 ) + (_sage_const_9 *u**_sage_const_4 +_sage_const_63 *u**_sage_const_3 +_sage_const_158 *u**_sage_const_2 +_sage_const_168 *u+_sage_const_64 ) + b2 = R*(_sage_const_216 *u**_sage_const_2 ) + (_sage_const_36 *u**_sage_const_3 -_sage_const_189 *u**_sage_const_2 -_sage_const_316 *u-_sage_const_168 ) + b3 = R*(_sage_const_108 *u) + (_sage_const_54 *u**_sage_const_2 -_sage_const_189 *u-_sage_const_158 ) + + c1 = R**_sage_const_2 *(-_sage_const_288 *u**_sage_const_3 ) + R*(_sage_const_54 *u**_sage_const_4 +_sage_const_378 *u**_sage_const_3 +_sage_const_948 *u**_sage_const_2 +_sage_const_1008 *u+_sage_const_384 ) + (_sage_const_18 *u**_sage_const_5 +_sage_const_45 *u**_sage_const_4 -_sage_const_251 *u**_sage_const_3 -_sage_const_1086 *u**_sage_const_2 -_sage_const_1384 *u-_sage_const_576 ) + c2 = R**_sage_const_2 *(-_sage_const_432 *u**_sage_const_2 ) + R*(_sage_const_153 *u**_sage_const_4 -_sage_const_657 *u**_sage_const_3 +_sage_const_1292 *u**_sage_const_2 +_sage_const_2064 *u+_sage_const_1072 ) + (-_sage_const_72 *u**_sage_const_4 +_sage_const_702 *u**_sage_const_3 -_sage_const_1069 *u**_sage_const_2 -_sage_const_2508 *u-_sage_const_1512 ) + c3 = R**_sage_const_2 *(-_sage_const_216 *u) + R*(_sage_const_180 *u**_sage_const_3 -_sage_const_891 *u**_sage_const_2 +_sage_const_1450 *u+_sage_const_1116 ) + (-_sage_const_108 *u**_sage_const_3 +_sage_const_864 *u**_sage_const_2 -_sage_const_1385 *u-_sage_const_1422 ) + c4 = R**_sage_const_2 *(-_sage_const_4 ) + R*(_sage_const_6 *u**_sage_const_2 -_sage_const_33 *u+_sage_const_58 +QQ(_sage_const_14 )/_sage_const_9 ) + (-_sage_const_4 *u**_sage_const_2 +_sage_const_32 *u-_sage_const_63 ) + + return matrix(Fn, [ + [a1/w, a2/w, a3/w, a4/w], + [-u**_sage_const_3 , -_sage_const_3 *u**_sage_const_2 , -_sage_const_3 *u, -_sage_const_1 ], + [b1/(_sage_const_144 *R), -b2/(_sage_const_72 *R), -b3/(_sage_const_36 *R), + (-_sage_const_2 *R-(_sage_const_2 *u-_sage_const_7 ))/(_sage_const_2 *R)], + [c1/(_sage_const_288 *R**_sage_const_2 ), c2/(_sage_const_144 *R**_sage_const_2 ), c3/(_sage_const_72 *R**_sage_const_2 ), + c4/(_sage_const_4 *R**_sage_const_2 )], + ]) + + +def limit_at_infinity(ff): + ff = Fn(ff) + nu = ff.numerator() + de = ff.denominator() + dn = nu.degree() + dd = de.degree() + if dn < dd: + return QQ(_sage_const_0 ) + if dn == dd: + return QQ(nu[dn]) / QQ(de[dd]) + raise AssertionError("balanced entry still diverges at infinity: %s" % ff) + + +u = _sage_const_2 *n + _sage_const_3 +M = authoritative_matrix(u, Fn(R)) +D0 = diagonal_matrix(Fn, [_sage_const_1 , n, n**_sage_const_2 , n**_sage_const_3 ]) +D1 = diagonal_matrix(Fn, [_sage_const_1 , n+_sage_const_1 , (n+_sage_const_1 )**_sage_const_2 , (n+_sage_const_1 )**_sage_const_3 ]) +B = D0.inverse() * M * D1 / (n+_sage_const_1 )**_sage_const_2 +S = matrix(QQ, _sage_const_4 , _sage_const_4 , [ + limit_at_infinity(B[i, j]) for i in range(_sage_const_4 ) for j in range(_sage_const_4 ) +]) + +S_expected = matrix(QQ, [ + [_sage_const_64 *R-_sage_const_44 , _sage_const_96 *R-_sage_const_54 , _sage_const_48 *R-_sage_const_17 , _sage_const_8 *R], + [-_sage_const_8 , -_sage_const_12 , -_sage_const_6 , -_sage_const_1 ], + [_sage_const_1 /R, -_sage_const_4 /R, -_sage_const_6 /R, -_sage_const_2 /R], + [_sage_const_2 /R**_sage_const_2 , (_sage_const_17 *R-_sage_const_8 )/R**_sage_const_2 , _sage_const_4 *(_sage_const_5 *R-_sage_const_3 )/R**_sage_const_2 , (_sage_const_6 *R-_sage_const_4 )/R**_sage_const_2 ], +]) +assert S == S_expected + +Rx = PolynomialRing(QQ, names=('x',)); (x,) = Rx._first_ngens(1) +Q = ( + R**_sage_const_2 *x**_sage_const_4 + - (_sage_const_64 *R**_sage_const_3 - _sage_const_56 *R**_sage_const_2 - _sage_const_4 )*x**_sage_const_3 + + (_sage_const_48 *R**_sage_const_2 - _sage_const_262 *R + _sage_const_220 )*x**_sage_const_2 + - (_sage_const_12 *R - _sage_const_8 )*x + + _sage_const_1 +) +assert Rx(S.charpoly("x")) == Q/R**_sage_const_2 + +# On |x|=1 the cubic term strictly dominates all other terms. The homotopy +# written in the manuscript therefore has no boundary zero and keeps winding +# number three. +rouche_margin = ( + (_sage_const_64 *R**_sage_const_3 -_sage_const_56 *R**_sage_const_2 -_sage_const_4 ) + - (R**_sage_const_2 + (_sage_const_48 *R**_sage_const_2 -_sage_const_262 *R+_sage_const_220 ) + (_sage_const_12 *R-_sage_const_8 ) + _sage_const_1 ) +) +assert rouche_margin == _sage_const_64 *R**_sage_const_3 -_sage_const_105 *R**_sage_const_2 +_sage_const_250 *R-_sage_const_217 +assert rouche_margin > _sage_const_0 +assert Q(_sage_const_1 ) == -(_sage_const_64 *R**_sage_const_3 -_sage_const_105 *R**_sage_const_2 +_sage_const_274 *R-_sage_const_233 ) +assert Q(_sage_const_1 ) < _sage_const_0 + +# First row of R^2 adj(xI-S). At Q(x)=0 it is a left eigenvector. +w = vector(Rx, [ + _sage_const_10 + (_sage_const_44 -_sage_const_7 *R)*x + (_sage_const_4 +_sage_const_12 *R**_sage_const_2 )*x**_sage_const_2 + R**_sage_const_2 *x**_sage_const_3 , + _sage_const_2 *((-_sage_const_23 +_sage_const_40 *R) + (-_sage_const_108 +_sage_const_194 *R-_sage_const_28 *R**_sage_const_2 )*x + + (-_sage_const_27 *R**_sage_const_2 +_sage_const_48 *R**_sage_const_3 )*x**_sage_const_2 ), + (-_sage_const_32 +_sage_const_71 *R) + (-_sage_const_68 +_sage_const_198 *R-_sage_const_8 *R**_sage_const_2 )*x + + (-_sage_const_17 *R**_sage_const_2 +_sage_const_48 *R**_sage_const_3 )*x**_sage_const_2 , + _sage_const_2 *R*(_sage_const_8 + (_sage_const_17 +_sage_const_3 *R)*x + _sage_const_4 *R**_sage_const_2 *x**_sage_const_2 ), +]) +assert w * (x*identity_matrix(Rx, _sage_const_4 ) - S.change_ring(Rx)) == vector(Rx, [Q, _sage_const_0 , _sage_const_0 , _sage_const_0 ]) + +# These are the positive rewrites used at the unique exterior root rho>1. +w_positive = vector(Rx, [ + R*x*(R*x**_sage_const_2 -_sage_const_7 ) + _sage_const_12 *R**_sage_const_2 *x**_sage_const_2 + _sage_const_4 *x**_sage_const_2 + _sage_const_44 *x + _sage_const_10 , + _sage_const_2 *(R**_sage_const_2 *x*((_sage_const_48 *R-_sage_const_27 )*x-_sage_const_28 ) + + (_sage_const_194 *R-_sage_const_108 )*x + _sage_const_40 *R-_sage_const_23 ), + R**_sage_const_2 *x*((_sage_const_48 *R-_sage_const_17 )*x-_sage_const_8 ) + + (_sage_const_198 *R-_sage_const_68 )*x + _sage_const_71 *R-_sage_const_32 , + _sage_const_2 *R*(_sage_const_8 + (_sage_const_17 +_sage_const_3 *R)*x + _sage_const_4 *R**_sage_const_2 *x**_sage_const_2 ), +]) +assert w_positive == w +assert R > _sage_const_7 + +e1 = vector(QQ, [_sage_const_1 , _sage_const_0 , _sage_const_0 , _sage_const_0 ]) +C = matrix(QQ, _sage_const_4 , _sage_const_4 ) +for j in range(_sage_const_4 ): + C.set_column(j, S**j * e1) +detC_expected = -_sage_const_4 *(_sage_const_27 *R-_sage_const_11 )*(_sage_const_128 *R**_sage_const_2 -_sage_const_149 *R-_sage_const_43 )/R**_sage_const_6 +assert C.det() == detC_expected +assert C.det() != _sage_const_0 + +print("PASS: exact balanced limit and characteristic quartic") +print("PASS: boundary-free homotopy has winding number three") +print("PASS: explicit exterior-root eigenvector has four positive coordinates") +print("PASS: limiting e1 cyclic frame is invertible") +print("The analytic stable-graph contraction is proved in solution.tex.") + diff --git a/experiments/ramanujan_28/submission/certificates/p28_kernel_contiguity_certificate.sage.py b/experiments/ramanujan_28/submission/certificates/p28_kernel_contiguity_certificate.sage.py new file mode 100644 index 0000000..77a8f2d --- /dev/null +++ b/experiments/ramanujan_28/submission/certificates/p28_kernel_contiguity_certificate.sage.py @@ -0,0 +1,214 @@ +#!/usr/bin/env sage +""" +Exact all-N kernel/contiguity certificate for Ramanujan Challenge 2.8. + +This file works over QQ(u,x,j), so every assertion is a symbolic identity. +Put + + z = -x/(1-x), theta = z*d/dz = (1-x)*x*d/dx, + u = 2*N+3, m = N+1 = (u-1)/2. + +The scalar adjoint tail is, up to a nonzero normalization kappa_N, + + F_N(z) = kappa_N*z^m * + 4F3(m,m+1/6,m+1/2,m+5/6; 2m,2m,2m; z). + +Writing delta_N = theta-m, its four-component Euler jet is + + K_N = (F_N, delta_N F_N, delta_N^2 F_N, delta_N^3 F_N)^T. + +The assertions below prove symbolically that the parameterized official +transfer matrix satisfies + + M_N(x) K_{N+1}(x) = K_N(x) + +for every N >= 0. The first component is checked coefficientwise using the +hypergeometric coefficient ratios. The remaining three components are +checked as exact Ore-style polynomial congruences modulo the shifted 4F3 +differential equation. + +This uses the exact parameter identity + + 236337691420383 = (14*R-567)/9, R=1/x, + +which is valid at the official R=151931373056001. +""" + + +# This file was *autogenerated* from the file p28_kernel_contiguity_certificate.sage +from sage.all_cmdline import * # import sage library + +_sage_const_1 = Integer(1); _sage_const_2 = Integer(2); _sage_const_3 = Integer(3); _sage_const_144 = Integer(144); _sage_const_5 = Integer(5); _sage_const_288 = Integer(288); _sage_const_4 = Integer(4); _sage_const_99 = Integer(99); _sage_const_333 = Integer(333); _sage_const_229 = Integer(229); _sage_const_114 = Integer(114); _sage_const_40 = Integer(40); _sage_const_64 = Integer(64); _sage_const_432 = Integer(432); _sage_const_864 = Integer(864); _sage_const_243 = Integer(243); _sage_const_909 = Integer(909); _sage_const_868 = Integer(868); _sage_const_80 = Integer(80); _sage_const_272 = Integer(272); _sage_const_153 = Integer(153); _sage_const_648 = Integer(648); _sage_const_860 = Integer(860); _sage_const_360 = Integer(360); _sage_const_9 = Integer(9); _sage_const_63 = Integer(63); _sage_const_158 = Integer(158); _sage_const_168 = Integer(168); _sage_const_216 = Integer(216); _sage_const_36 = Integer(36); _sage_const_189 = Integer(189); _sage_const_316 = Integer(316); _sage_const_108 = Integer(108); _sage_const_54 = Integer(54); _sage_const_378 = Integer(378); _sage_const_948 = Integer(948); _sage_const_1008 = Integer(1008); _sage_const_384 = Integer(384); _sage_const_18 = Integer(18); _sage_const_45 = Integer(45); _sage_const_251 = Integer(251); _sage_const_1086 = Integer(1086); _sage_const_1384 = Integer(1384); _sage_const_576 = Integer(576); _sage_const_657 = Integer(657); _sage_const_1292 = Integer(1292); _sage_const_2064 = Integer(2064); _sage_const_1072 = Integer(1072); _sage_const_72 = Integer(72); _sage_const_702 = Integer(702); _sage_const_1069 = Integer(1069); _sage_const_2508 = Integer(2508); _sage_const_1512 = Integer(1512); _sage_const_180 = Integer(180); _sage_const_891 = Integer(891); _sage_const_1450 = Integer(1450); _sage_const_1116 = Integer(1116); _sage_const_1385 = Integer(1385); _sage_const_1422 = Integer(1422); _sage_const_6 = Integer(6); _sage_const_33 = Integer(33); _sage_const_58 = Integer(58); _sage_const_14 = Integer(14); _sage_const_32 = Integer(32); _sage_const_7 = Integer(7); _sage_const_11 = Integer(11); _sage_const_580 = Integer(580); _sage_const_872 = Integer(872); _sage_const_405 = Integer(405); _sage_const_436 = Integer(436); _sage_const_12 = Integer(12); _sage_const_0 = Integer(0); _sage_const_536 = Integer(536); _sage_const_297 = Integer(297); _sage_const_567 = Integer(567) +from sage.all import * + + +# Coefficient field and the Euler-operator polynomial variable. +A = PolynomialRing(QQ, names=("u", "x", "j")) +u, x, j = A.gens() +K = A.fraction_field() +u, x, j = map(K, (u, x, j)) +T = PolynomialRing(K, "t") +t = T.gen() + +m = (u - _sage_const_1 ) / _sage_const_2 +R = _sage_const_1 / x +w = u * (_sage_const_3 *u - _sage_const_2 ) * (_sage_const_3 *u + _sage_const_2 ) + + +# Exact parameterized official transfer matrix. +a1 = R*(_sage_const_144 *u**_sage_const_5 - _sage_const_288 *u**_sage_const_4 + _sage_const_144 *u**_sage_const_3 ) + (-_sage_const_99 *u**_sage_const_5 + _sage_const_333 *u**_sage_const_4 - _sage_const_229 *u**_sage_const_3 - _sage_const_114 *u**_sage_const_2 + _sage_const_40 *u + _sage_const_64 ) +a2 = R*(_sage_const_432 *u**_sage_const_4 - _sage_const_864 *u**_sage_const_3 + _sage_const_432 *u**_sage_const_2 ) + (-_sage_const_243 *u**_sage_const_4 + _sage_const_909 *u**_sage_const_3 - _sage_const_868 *u**_sage_const_2 - _sage_const_80 *u + _sage_const_272 ) +a3 = R*(_sage_const_432 *u**_sage_const_3 - _sage_const_864 *u**_sage_const_2 + _sage_const_432 *u) + (-_sage_const_153 *u**_sage_const_3 + _sage_const_648 *u**_sage_const_2 - _sage_const_860 *u + _sage_const_360 ) +a4 = R*_sage_const_144 *(u - _sage_const_1 )**_sage_const_2 + +b1 = R*(-_sage_const_144 *u**_sage_const_3 ) + (_sage_const_9 *u**_sage_const_4 + _sage_const_63 *u**_sage_const_3 + _sage_const_158 *u**_sage_const_2 + _sage_const_168 *u + _sage_const_64 ) +b2 = R*(_sage_const_216 *u**_sage_const_2 ) + (_sage_const_36 *u**_sage_const_3 - _sage_const_189 *u**_sage_const_2 - _sage_const_316 *u - _sage_const_168 ) +b3 = R*(_sage_const_108 *u) + (_sage_const_54 *u**_sage_const_2 - _sage_const_189 *u - _sage_const_158 ) + +c1 = R**_sage_const_2 *(-_sage_const_288 *u**_sage_const_3 ) + R*(_sage_const_54 *u**_sage_const_4 + _sage_const_378 *u**_sage_const_3 + _sage_const_948 *u**_sage_const_2 + _sage_const_1008 *u + _sage_const_384 ) + (_sage_const_18 *u**_sage_const_5 + _sage_const_45 *u**_sage_const_4 - _sage_const_251 *u**_sage_const_3 - _sage_const_1086 *u**_sage_const_2 - _sage_const_1384 *u - _sage_const_576 ) +c2 = R**_sage_const_2 *(-_sage_const_432 *u**_sage_const_2 ) + R*(_sage_const_153 *u**_sage_const_4 - _sage_const_657 *u**_sage_const_3 + _sage_const_1292 *u**_sage_const_2 + _sage_const_2064 *u + _sage_const_1072 ) + (-_sage_const_72 *u**_sage_const_4 + _sage_const_702 *u**_sage_const_3 - _sage_const_1069 *u**_sage_const_2 - _sage_const_2508 *u - _sage_const_1512 ) +c3 = R**_sage_const_2 *(-_sage_const_216 *u) + R*(_sage_const_180 *u**_sage_const_3 - _sage_const_891 *u**_sage_const_2 + _sage_const_1450 *u + _sage_const_1116 ) + (-_sage_const_108 *u**_sage_const_3 + _sage_const_864 *u**_sage_const_2 - _sage_const_1385 *u - _sage_const_1422 ) +c4 = R**_sage_const_2 *(-_sage_const_4 ) + R*(_sage_const_6 *u**_sage_const_2 - _sage_const_33 *u + _sage_const_58 + QQ(_sage_const_14 )/_sage_const_9 ) + (-_sage_const_4 *u**_sage_const_2 + _sage_const_32 *u - _sage_const_63 ) + +M = Matrix(K, [ + [a1/w, a2/w, a3/w, a4/w], + [-u**_sage_const_3 , -_sage_const_3 *u**_sage_const_2 , -_sage_const_3 *u, -_sage_const_1 ], + [x*b1/_sage_const_144 , -x*b2/_sage_const_72 , -x*b3/_sage_const_36 , x*(-_sage_const_2 *R-(_sage_const_2 *u-_sage_const_7 ))/_sage_const_2 ], + [x**_sage_const_2 *c1/_sage_const_288 , x**_sage_const_2 *c2/_sage_const_144 , x**_sage_const_2 *c3/_sage_const_72 , x**_sage_const_2 *c4/_sage_const_4 ], +]) + + +# P_r(t) is row r of M evaluated on the shifted Euler jet +# (1,t,t^2,t^3)^T of F_{N+1}. +P = [ + T(sum(M[r, s] * t**s for s in range(_sage_const_4 ))) + for r in range(_sage_const_4 ) +] + + +# F_{N+1} has exponent m+1 and parameters +# (m+1,m+7/6,m+3/2,m+11/6; 2m+2,2m+2,2m+2). +# With t=delta_{N+1}, its exact 4F3 differential equation is L(t)F=0. +L = T( + (_sage_const_1 -x)*t*(t+u)**_sage_const_3 + + x*(t+m+_sage_const_1 )*(t+m+QQ(_sage_const_7 )/_sage_const_6 )*(t+m+QQ(_sage_const_3 )/_sage_const_2 )*(t+m+QQ(_sage_const_11 )/_sage_const_6 ) +) + + +def theta_coefficients(poly): + """Apply theta=(1-x)x*d/dx only to the coefficients of poly(t).""" + return T(sum( + (_sage_const_1 -x)*x*K(poly[k]).derivative(x) * t**k + for k in range(poly.degree()+_sage_const_1 ) + )) + + +def shifted_derivative(poly): + """Operator induced by delta_N=theta-m=t+1 on poly(t)F_{N+1}.""" + return theta_coefficients(poly) + (t+_sage_const_1 )*poly + + +# Row 1 is the clean scalar contiguity relation +# +# delta_N F_N = -(t+u)^3 F_{N+1}. +assert P[_sage_const_1 ] == -(t+u)**_sage_const_3 + + +# Once row 0 gives F_N=P_0(t)F_{N+1}, the other rows must be its first, +# second and third delta_N derivatives. The following exact factorizations +# prove this directly. No polynomial division or remainder command is used. +expected_quotients = [ + _sage_const_144 *(u-_sage_const_1 )**_sage_const_2 / (u*(_sage_const_3 *u-_sage_const_2 )*(_sage_const_3 *u+_sage_const_2 )*x), + -_sage_const_1 , + (-_sage_const_2 + _sage_const_7 *x - _sage_const_2 *u*x) / _sage_const_2 , +] + +for r in range(_sage_const_3 ): + difference = T(shifted_derivative(P[r]) - P[r+_sage_const_1 ]) + quotient = T(expected_quotients[r]) + assert difference == quotient*L + + +# The fourth companion closure is the row omitted by a mere three-row +# derivative check. The preceding tail F_N satisfies +# +# L_minus(s)=s^4+l3*s^3+l2*s^2+l1*s+l0, +# +# with s=delta_N. Hence delta_N^4 F_N is the displayed linear combination +# of the first four jet entries. The last identity below completes the +# four-equation differential gauge. +l0 = (u-_sage_const_1 )*u*(_sage_const_3 *u-_sage_const_2 )*(_sage_const_3 *u+_sage_const_2 )*x/_sage_const_144 +l1 = ( + -_sage_const_576 + _sage_const_864 *u - _sage_const_432 *u**_sage_const_2 + _sage_const_72 *u**_sage_const_3 + + _sage_const_580 *x - _sage_const_872 *u*x + _sage_const_405 *u**_sage_const_2 *x - _sage_const_36 *u**_sage_const_3 *x +) / _sage_const_72 +l2 = ( + _sage_const_432 - _sage_const_432 *u + _sage_const_108 *u**_sage_const_2 + - _sage_const_436 *x + _sage_const_405 *u*x - _sage_const_54 *u**_sage_const_2 *x +) / _sage_const_36 +l3 = (-_sage_const_12 + _sage_const_6 *u + _sage_const_11 *x - _sage_const_2 *u*x) / _sage_const_2 + +difference4 = T( + shifted_derivative(P[_sage_const_3 ]) + + l3*P[_sage_const_3 ] + l2*P[_sage_const_2 ] + l1*P[_sage_const_1 ] + l0*P[_sage_const_0 ] +) +quotient4 = T( + ( + -_sage_const_36 + _sage_const_536 *x - _sage_const_297 *u*x + _sage_const_54 *u**_sage_const_2 *x + - _sage_const_567 *x**_sage_const_2 + _sage_const_288 *u*x**_sage_const_2 - _sage_const_36 *u**_sage_const_2 *x**_sage_const_2 + ) / _sage_const_36 +) +assert difference4 == quotient4*L + + +# It remains to certify row 0, i.e. F_N=P_0(t)F_{N+1}. +# Split P_0=A(t)/x+B(t). Since 1/x=-(1-z)/z=-1/z+1, +# the coefficient of z^(m+j) is a two-term expression involving the j-th +# and (j-1)-st coefficients of F_{N+1}. The identities below verify it +# for symbolic j. +AA = T(_sage_const_144 *(u-_sage_const_1 )**_sage_const_2 *(t+u)**_sage_const_3 / (u*(_sage_const_3 *u-_sage_const_2 )*(_sage_const_3 *u+_sage_const_2 ))) +BB = T(P[_sage_const_0 ] - AA/x) +assert P[_sage_const_0 ] == AA/x + BB + + +# kappa_{N+1}/kappa_N. In N-language this is +# -(6N+7)(6N+11)/(576(N+1)^2(2N+3)^2). +rho = -(_sage_const_3 *u-_sage_const_2 )*(_sage_const_3 *u+_sage_const_2 ) / (_sage_const_144 *(u-_sage_const_1 )**_sage_const_2 *u**_sage_const_2 ) + + +def b_over_a(q): + """Coefficient ratio b_q/a_q for F_{N+1} versus F_N.""" + return K( + ((m+q)*(m+QQ(_sage_const_1 )/_sage_const_6 +q)*(m+QQ(_sage_const_1 )/_sage_const_2 +q)*(m+QQ(_sage_const_5 )/_sage_const_6 +q)) + / (m*(m+QQ(_sage_const_1 )/_sage_const_6 )*(m+QQ(_sage_const_1 )/_sage_const_2 )*(m+QQ(_sage_const_5 )/_sage_const_6 )) + * (_sage_const_2 *m*(_sage_const_2 *m+_sage_const_1 ) / ((_sage_const_2 *m+q)*(_sage_const_2 *m+q+_sage_const_1 )))**_sage_const_3 + ) + + +def a_next_ratio(q): + """a_(q+1)/a_q for the normalized hypergeometric series in F_N.""" + return K( + (m+q)*(m+QQ(_sage_const_1 )/_sage_const_6 +q)*(m+QQ(_sage_const_1 )/_sage_const_2 +q)*(m+QQ(_sage_const_5 )/_sage_const_6 +q) + / ((_sage_const_2 *m+q)**_sage_const_3 *(q+_sage_const_1 )) + ) + + +# Lowest coefficient, j=0. +assert K(rho * (-AA(K(_sage_const_0 ))) - _sage_const_1 ) == _sage_const_0 + +# Generic coefficient, j>=1. This is an identity in QQ(u,j). +Rj = b_over_a(j) +Sj = b_over_a(j-_sage_const_1 ) / a_next_ratio(j-_sage_const_1 ) +generic_identity = K( + rho * ( + -AA(j)*Rj + + (AA(j-_sage_const_1 )+BB(j-_sage_const_1 ))*Sj + ) - _sage_const_1 +) +assert generic_identity == _sage_const_0 + + +print("PASS: exact all-N 4F3 kernel contiguity certificate") +print("M_N(x) K_{N+1}(x) = K_N(x) symbolically in QQ(u,x)") +print("theta convention: theta=z*d/dz=(1-x)*x*d/dx") + diff --git a/experiments/ramanujan_28/submission/certificates/p28_lattice_hypotheses_certificate.sage.py b/experiments/ramanujan_28/submission/certificates/p28_lattice_hypotheses_certificate.sage.py new file mode 100644 index 0000000..120a19c --- /dev/null +++ b/experiments/ramanujan_28/submission/certificates/p28_lattice_hypotheses_certificate.sage.py @@ -0,0 +1,130 @@ +#!/usr/bin/env sage +""" +Exact algebraic hypotheses for the Problem 2.8 tail-lattice induction. + +Run from the repository root with + + sage agent_outputs/tail_lattice/p28_lattice_hypotheses_certificate.sage + +The script loads the independent all-N kernel certificate, then verifies: + + * J_N = diag(x,1,1,1) M_N is regular at x=0; + * J_N(0) has the claimed rank-one factorization; + * its image direction is the leading direction of H k_N; + * the transformed 3F2 equation gives the exact row dependence. + +The only non-machine step in the lattice closure is then the two-line DVR +lemma proved in TAIL_LATTICE_CLOSURE_REPORT.md. +""" + + +# This file was *autogenerated* from the file certificates/p28_lattice_hypotheses_certificate.sage +from sage.all_cmdline import * # import sage library + +_sage_const_1 = Integer(1); _sage_const_0 = Integer(0); _sage_const_4 = Integer(4); _sage_const_144 = Integer(144); _sage_const_2 = Integer(2); _sage_const_3 = Integer(3); _sage_const_6 = Integer(6); _sage_const_5 = Integer(5); _sage_const_72 = Integer(72); _sage_const_108 = Integer(108); _sage_const_46 = Integer(46); _sage_const_18 = Integer(18); _sage_const_23 = Integer(23); _sage_const_27 = Integer(27); _sage_const_216 = Integer(216) +from sage.all import * +import os + + +HERE = os.path.dirname(os.path.abspath(__file__)) +KERNEL = os.path.join(HERE, "p28_kernel_contiguity_certificate.sage") +if not os.path.exists(KERNEL): + KERNEL = os.path.join( + HERE, "..", "special_functions", + "p28_kernel_contiguity_certificate.sage" + ) +load(KERNEL) + + +H = diagonal_matrix(K, [x, _sage_const_1 , _sage_const_1 , _sage_const_1 ]) +J = H*M + + +def value_at_zero(q): + """Evaluate a simplified rational function at x=0.""" + q = K(q) + numerator = q.numerator() + denominator = q.denominator() + value_denominator = denominator.subs({x: _sage_const_0 }) + assert value_denominator != _sage_const_0 + return K(numerator.subs({x: _sage_const_0 }) / value_denominator) + + +J0 = Matrix(K, _sage_const_4 , _sage_const_4 , [value_at_zero(q) for q in J.list()]) +a = _sage_const_144 *(u-_sage_const_1 )**_sage_const_2 / (u*(_sage_const_3 *u-_sage_const_2 )*(_sage_const_3 *u+_sage_const_2 )) +left = vector(K, [a, -_sage_const_1 , -_sage_const_1 , -_sage_const_1 ]) +right = vector(K, [u**_sage_const_3 , _sage_const_3 *u**_sage_const_2 , _sage_const_3 *u, _sage_const_1 ]) + +assert J0 == left.column()*right.row() +assert J0.rank() == _sage_const_1 +assert J0.column(_sage_const_0 ) != _sage_const_0 + + +# The x^(-1) coefficient of M controls the constant term of the transformed +# denominator. It is another rank-one matrix, now with only its first row +# nonzero. +Mminus1 = Matrix(K, _sage_const_4 , _sage_const_4 , [ + value_at_zero(x*q) for q in M.list() +]) +e0 = vector(K, [_sage_const_1 , _sage_const_0 , _sage_const_0 , _sage_const_0 ]) +assert Mminus1 == e0.column()*(a*right).row() + +# Therefore c_(N+1)/c_N is the first entry of a*right. +constant_ratio = a*u**_sage_const_3 +assert constant_ratio == ( + _sage_const_144 *(u-_sage_const_1 )**_sage_const_2 *u**_sage_const_2 / ((_sage_const_3 *u-_sage_const_2 )*(_sage_const_3 *u+_sage_const_2 )) +) + + +# The first coefficient of +# +# 4F3(m,m+1/6,m+1/2,m+5/6;2m,2m,2m;z) +# +# is c. Since z=-x+O(x^2), the leading direction of H*k_N is +# (1,-c,-c,-c)^T. +c = ( + m*(m+QQ(_sage_const_1 )/_sage_const_6 )*(m+QQ(_sage_const_1 )/_sage_const_2 )*(m+QQ(_sage_const_5 )/_sage_const_6 ) + / (_sage_const_2 *m)**_sage_const_3 +) +assert K(c - _sage_const_1 /a) == _sage_const_0 +tail_direction = vector(K, [_sage_const_1 , -c, -c, -c]) +assert left == a*tail_direction + + +# The row dependence is just the transformed 3F2 equation. It is recorded +# here as a formal coefficient identity in the four symbols +# (y-1, theta*y, theta^2*y, theta^3*y). +Y = PolynomialRing(K, names=("f0", "f1", "f2", "f3")) +f0, f1, f2, f3 = Y.gens() +y = f0 + _sage_const_1 +ode = _sage_const_72 *f3 + _sage_const_108 *x*f2 + _sage_const_46 *x*f1 + _sage_const_5 *x*y + +# C*k0 = -5/4 after B*k0=f. +Ck0 = _sage_const_18 *f3/x + QQ(_sage_const_5 )/_sage_const_4 *f0 + QQ(_sage_const_23 )/_sage_const_2 *f1 + _sage_const_27 *f2 +assert Y(x*(Ck0 + QQ(_sage_const_5 )/_sage_const_4 ) - ode/_sage_const_4 ) == _sage_const_0 + +# Therefore 72 E3 + 108 x E2 + 46 x E1 + 5 x E0 = 0. +# The B-part cancels independently. +b0 = vector(K, [_sage_const_1 , _sage_const_0 , _sage_const_0 , _sage_const_0 ]) +b1 = vector(K, [_sage_const_1 , _sage_const_1 , _sage_const_0 , _sage_const_0 ]) +b2 = vector(K, [_sage_const_1 , _sage_const_2 , _sage_const_1 , _sage_const_0 ]) +b3 = vector(K, [_sage_const_1 , _sage_const_3 , _sage_const_3 , _sage_const_1 ]) +assert _sage_const_72 *b3 + _sage_const_108 *x*b2 + _sage_const_46 *x*b1 + _sage_const_5 *x*b0 == vector( + K, [_sage_const_72 + _sage_const_108 *x + _sage_const_46 *x + _sage_const_5 *x, + _sage_const_216 + _sage_const_108 *x + _sage_const_46 *x, + _sage_const_216 + _sage_const_108 *x, + _sage_const_72 ] +) + +# In the full carrier the f*C contribution is killed by the ODE, and the +# displayed B combination equals -4*C after using the compact expression +# C=(18/x)b3+(5/4)b0+(23/2)b1+27b2. Verify this exact cancellation. +Crow = _sage_const_18 *b3/x + QQ(_sage_const_5 )/_sage_const_4 *b0 + QQ(_sage_const_23 )/_sage_const_2 *b1 + _sage_const_27 *b2 +Bcomb = _sage_const_72 *b3 + _sage_const_108 *x*b2 + _sage_const_46 *x*b1 + _sage_const_5 *x*b0 +assert Bcomb == _sage_const_4 *x*Crow + + +print("PASS: exact rank-one/DVR hypotheses for all N") +print("J_N(0) = (a,-1,-1,-1)^T (u^3,3u^2,3u,1)") +print("a^{-1} is the first shifted 4F3 coefficient") +