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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WY6SfRYvm8zFKMX9GcjS8u
This commit is contained in:
parent
3eded12fe1
commit
aac17e6e34
5 changed files with 698 additions and 317 deletions
|
|
@ -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
|
||||
```
|
||||
|
|
@ -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.
|
||||
|
|
@ -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.")
|
||||
|
||||
|
|
@ -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")
|
||||
|
||||
|
|
@ -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")
|
||||
|
||||
Loading…
Add table
Reference in a new issue