feat: add optional enhancements for Ramanujan Problem 2.8
- Positive-cone transport certificates (p28_positive_cone.py, POSITIVE_CONE_CERTIFICATE.md, POSITIVE_CONE_MANUSCRIPT_SECTION.tex) - Optimized differential gauge (p28_optimized_gauge.py, OPTIMIZED_GAUGE_CERTIFICATE.md) - Adversarial provenance supplements (p28_mutation_sensitivity.py, solution_pre_positive_cone.tex) - FAMM SCARS advisory records (FAMM_SCARS.md, p28_famm_scars.json, p28_famm_scars_validator.py) - Overview documentation (OPTIONAL_IMPROVEMENTS.md, ADVERSARIAL_AUDIT.md) These are independent, replayable supplements developed after the original exact closure. They can be verified independently with 'bash run_checks.sh' in the certificates directory.
This commit is contained in:
parent
39806d4423
commit
1d5273264d
20 changed files with 5373 additions and 0 deletions
127
optional/ADVERSARIAL_AUDIT.md
Normal file
127
optional/ADVERSARIAL_AUDIT.md
Normal file
|
|
@ -0,0 +1,127 @@
|
||||||
|
# Adversarial Audit — Ramanujan Challenge Problem 2.8
|
||||||
|
|
||||||
|
## Verdict
|
||||||
|
|
||||||
|
The recurrence-specific proof path passes the repaired adversarial audit.
|
||||||
|
Every Ore, differential-gauge, terminating-induction, valuation, convergence,
|
||||||
|
and all-four-column obligation is now displayed as an equation and replayed
|
||||||
|
without a computer-algebra decision procedure. The active all-column proof is
|
||||||
|
an elementary positive-cone contraction; the earlier spectral/stable-graph
|
||||||
|
route remains in the package as a replayed legacy alternative.
|
||||||
|
|
||||||
|
The exact trust boundary is important:
|
||||||
|
|
||||||
|
- The proof imports the classical Chudnovsky formula as one explicitly named
|
||||||
|
theorem, with a precise citation to a complete modular/CM derivation.
|
||||||
|
- It also uses foundational results stated with their hypotheses: absolute
|
||||||
|
convergence of power series, the maximum modulus principle, and completeness
|
||||||
|
of bounded monotone real sequences.
|
||||||
|
- It does **not** claim to be axiom-free or to reconstruct those foundational
|
||||||
|
theorems from set theory.
|
||||||
|
|
||||||
|
Relative to that explicit boundary, no recurrence-specific assumption,
|
||||||
|
vacuous implication, numerical-equality inference, or hidden CAS remainder
|
||||||
|
remains.
|
||||||
|
|
||||||
|
## Defects found and repaired
|
||||||
|
|
||||||
|
| Initial defect | Why it failed | Equation-level repair |
|
||||||
|
|---|---|---|
|
||||||
|
| The deformed transfer was under-defined | Only one substituted coefficient was shown; later notation changed the meaning of the first argument | Displayed all sixteen entries of \(\mathcal M(u,x)\), defined \(M_N(x)=\mathcal M(2N+3,x)\), and displayed both official seed rows |
|
||||||
|
| Three matrix terms lost a plus sign during the first repair | The manuscript matrix then differed from the certified matrix | Restored the three sums in \(c_1,c_2,c_3\); hostile replay caught this before release |
|
||||||
|
| Ore divisions used `quo_rem` | A zero remainder was trusted rather than exhibited | Replaced every division with four direct cleared factorizations \(D_r=q_rL_+\), including the fourth companion closure |
|
||||||
|
| “Standard ascension identity” and transformed ODE were named but not derived | The coefficient mechanism was hidden | Added initial coefficient and consecutive-ratio equations; expanded the \({}_3F_2\) Euler operator explicitly |
|
||||||
|
| ODE normalization was claimed to determine the terminating \({}_4F_3\) uniquely | False: the exponent \(2n\) supplies an additional analytic branch | Replaced uniqueness with base, generic, and top coefficient induction for the actual one-step operator |
|
||||||
|
| The scalar one-step operator was not tied to the challenge matrix | Hard-coded \(d_0,d_1\) could have described a surrogate | Added horizontal reconstruction, all sixteen differential-gauge equations, and the exact matrix contraction producing \(d_0+zd_1\) |
|
||||||
|
| Only the first base component was initially checked | The actual compact seed row was not yet known to be horizontal | Added all four base-row reconstruction equations, the base terminating-operator equation, and all four base adjoint residuals |
|
||||||
|
| Two DVR-lemma hypotheses were only implicit | The induction had not displayed the \(k_{N+1}\) leading direction or \(J_N(0)e_1\ne0\) | Added both expansions and cited them explicitly at the induction step |
|
||||||
|
| A transfer norm inequality used an upper bound with exponent \(-1\) | The inequality direction was invalid for column four | Split \(j\le3\) and \(j=4\), then used coupled row factors to obtain \(\|\mathcal B_m\|_\infty\le4981375/512<10000\) |
|
||||||
|
| The maximum-modulus step omitted holomorphy of the quotient | Formal divisibility only supplied a local removable germ | Proved holomorphy on \(|x|\le1/4\), identified the only possible pole, and removed it with the \(2n\)-valuation |
|
||||||
|
| Birkhoff–Poincaré was used as a black box for three columns | It hid the exceptional hyperplane, dominant functional, decay, and denominator nonvanishing | First replaced it with an explicit stable graph; the optimized proof now eliminates the spectral layer entirely via \(T_m=\mathcal P\mathcal B_m\mathcal P^{-1}>0\) and a four-weight min/max contraction |
|
||||||
|
| The spectral route required a quartic root count, eigenvector, and exceptional-hyperplane analysis | Although repaired, it created unnecessary proof surface | Verified all 285 positive numerator coefficients, the positive limiting transfer, and both positive seeds; all four quotients are now convex averages with uniformly positive weights |
|
||||||
|
| Division in columns \(2,3,4\) preceded an eventual-nonzero proof | The displayed quotients were not yet justified | The positive-cone seed and transfer identities now give \(Q_{m,j}>0\) for every \(m\ge1\), before any quotient is formed |
|
||||||
|
| The direct rational differential gauge produced large unreduced intermediates | Correct but slow replay increased resource and serialization risk | Added a separately reconstructed \(J_0+xJ_1+x^2J_2\) decomposition and checked the denominator-cleared polynomial gauge in 176 scalar coefficient obligations |
|
||||||
|
| The terminating step polynomial obscured its structure with 21 expanded terms | Large coefficients made transcription review difficult | Rewrote it in \(u=2n+1,\ q=2n-t\), then added a direct coefficient identity against the former expansion |
|
||||||
|
| A FAMM `SoftScar` was initially linked with `DerivedFrom` | It did not follow the repository’s calibrated `Supports` parent pattern | Corrected every parent role and added a fail-closed FAMM interchange validator; all scars remain advisory |
|
||||||
|
| The checker could succeed while Wolfram/Sage were absent | A stored transcript was being treated as proof evidence | Made standard-library rational-polynomial verifiers mandatory; Wolfram and Sage are now optional independent cross-checks |
|
||||||
|
| Metadata called \(Q/P\) the requested orientation | The official challenge asks for \(P/Q\) | Corrected every release document to state \(P/Q\to\sqrt{10005}/\pi\) as the official orientation |
|
||||||
|
|
||||||
|
## Mandatory replay
|
||||||
|
|
||||||
|
Run:
|
||||||
|
|
||||||
|
```sh
|
||||||
|
./run_checks.sh
|
||||||
|
```
|
||||||
|
|
||||||
|
The mandatory path executes:
|
||||||
|
|
||||||
|
1. `p28_rank_ode_bound_verifier.py`
|
||||||
|
2. `p28_convergence_constants.py`
|
||||||
|
3. `p28_standalone_equations.py`
|
||||||
|
4. `p28_optimized_gauge.py`
|
||||||
|
5. `p28_positive_cone.py`
|
||||||
|
6. `p28_mutation_sensitivity.py`
|
||||||
|
7. `p28_famm_scars_validator.py`
|
||||||
|
|
||||||
|
It then replays `p28_dominant_product_algebra.py` as a preserved legacy
|
||||||
|
cross-check; that quartic/spectral route is not required by the active proof.
|
||||||
|
|
||||||
|
The third verifier checks:
|
||||||
|
|
||||||
|
- four cleared tail factorizations;
|
||||||
|
- lowest and generic tail coefficients;
|
||||||
|
- horizontal reconstruction;
|
||||||
|
- the terminating-operator closure;
|
||||||
|
- all sixteen differential-gauge entries;
|
||||||
|
- the authoritative matrix-to-scalar contraction;
|
||||||
|
- the base polynomial and four base-row components;
|
||||||
|
- the base terminating equation and four base adjoint residuals;
|
||||||
|
- constant, generic, and top terminating induction;
|
||||||
|
- ascension and the \({}_3F_2\) Euler equation.
|
||||||
|
|
||||||
|
The positive-cone verifier checks:
|
||||||
|
|
||||||
|
- the authoritative \(M_m\), balanced \(\mathcal B_m\), and
|
||||||
|
\(T_m=\mathcal P\mathcal B_m\mathcal P^{-1}\);
|
||||||
|
- all sixteen rational identities \(T_{m,ij}=N_{ij}/D_{ij}\);
|
||||||
|
- all 285 strictly positive coefficients of the \(N_{ij}(m-1,R-4)\);
|
||||||
|
- the exact positive limiting matrix;
|
||||||
|
- all eight positive coordinates of the two official transformed seeds.
|
||||||
|
|
||||||
|
The optimized gauge separately checks 176 scalar coefficients while the
|
||||||
|
original sixteen-entry gauge remains in the standalone checker. These
|
||||||
|
verifiers use `fractions.Fraction` and explicit coefficient dictionaries. None
|
||||||
|
uses polynomial division, factorization, a simplifier, Gröbner bases,
|
||||||
|
irreducibility, GCD, a root finder, a special-function package, sampling, or
|
||||||
|
a stored transcript.
|
||||||
|
|
||||||
|
## Forbidden-shortcut search
|
||||||
|
|
||||||
|
The mandatory runner rejects these constructs in the proof path:
|
||||||
|
|
||||||
|
- `quo_rem`
|
||||||
|
- `is_irreducible`
|
||||||
|
- polynomial `gcd`
|
||||||
|
- Birkhoff/Poincaré delegation
|
||||||
|
- “standard ascension”
|
||||||
|
- ODE-normalization uniqueness
|
||||||
|
- the former dominant-product lemma in the active manuscript
|
||||||
|
|
||||||
|
No occurrence of `native_decide`, `axiom`, `sorry`, or `admit` was found.
|
||||||
|
|
||||||
|
## Independent hostile replays
|
||||||
|
|
||||||
|
Independent reviews and mutation replays targeted:
|
||||||
|
|
||||||
|
- logical validity, indexing, vacuity, and denominator domains;
|
||||||
|
- Ore/special-function and matrix-to-scalar algebra;
|
||||||
|
- convergence and all-column division;
|
||||||
|
- one-coefficient corruption of the positive-cone numerator table;
|
||||||
|
- one-coefficient corruption of the optimized \(J\)-decomposition.
|
||||||
|
|
||||||
|
The defects in the table above were discovered during those loops. The final
|
||||||
|
Ore, gauge, positive-cone, convergence, and logic/vacuity replays return PASS,
|
||||||
|
and both corrupted checkers fail at their intended identities. Release
|
||||||
|
engineering then repeats the mandatory checks in a clean extraction, rebuilds
|
||||||
|
the PDF, and performs page-by-page visual inspection.
|
||||||
BIN
optional/Archive.tar.gz
Normal file
BIN
optional/Archive.tar.gz
Normal file
Binary file not shown.
203
optional/FAMM_SCARS.md
Normal file
203
optional/FAMM_SCARS.md
Normal file
|
|
@ -0,0 +1,203 @@
|
||||||
|
# FAMM scars for Ramanujan Challenge Problem 2.8
|
||||||
|
|
||||||
|
## Status
|
||||||
|
|
||||||
|
This file and `certificates/p28_famm_scars.json` are advisory discovery
|
||||||
|
artifacts. They do not alter the proof, authorize pruning, or assert membership
|
||||||
|
in a canonical `DiscoveryStore`.
|
||||||
|
|
||||||
|
The formula-optimization rebuild is finalized. SHA-256 pins for the rank/ODE,
|
||||||
|
convergence, standalone-equation, denominator-cleared-gauge, positive-cone,
|
||||||
|
FAMM-interchange, and package-runner checkers are recorded in the JSON, along
|
||||||
|
with the final `solution.tex` and `solution.pdf` hashes. The older solution
|
||||||
|
hashes are retained solely as provenance for baseline commit `492c8ab`.
|
||||||
|
|
||||||
|
The bundle records defects found during the adversarial proof loop so later
|
||||||
|
searches can prioritize equation-level checks without mistaking past failures
|
||||||
|
for universal impossibility results.
|
||||||
|
|
||||||
|
The governing rule is:
|
||||||
|
|
||||||
|
> An observation, failure signature, SoftScar, or blocked promotion idea may
|
||||||
|
> change route priority. It may not remove a proof candidate.
|
||||||
|
|
||||||
|
The JSON therefore contains no `AuthorizedHardScar`.
|
||||||
|
|
||||||
|
## Authoritative FAMM sources
|
||||||
|
|
||||||
|
The schema and authority policy were read from
|
||||||
|
`allaunthefox/MathPunch-FiniteState` at commit
|
||||||
|
`9df0f48576aefce91eb1fc13ff876bec1007162d`:
|
||||||
|
|
||||||
|
| File | Relevant rule |
|
||||||
|
|---|---|
|
||||||
|
| `docs/specs/FAMM_REFINED.md` | Exact and advisory memory are separate; only exact/formal, replayed, in-scope, instance-matched, version-matched scars may hard-apply. |
|
||||||
|
| `docs/specs/FAMM_TOPOLOGY_ESCALATION_V1.md` | Machine layout and physical observations never change mathematical authority; advisory or unreplayed scars never hard-prune. |
|
||||||
|
| `src/discovery/node.rs` | Defines `Observation`, `FailureSignature`, `Certificate`, `SoftScar`, `ProposedHardScar`, `AuthorizationCertificate`, and `AuthorizedHardScar`, along with typed parent roles. |
|
||||||
|
| `src/discovery/authorization.rs` | The implemented hard-scar gate requires a typed Boolean linear formula, complete failed assignment, deletion-minimized cube, exact linear-constraint certificate, `linear-cube-interval` authorization, and replay/reauthorization. |
|
||||||
|
| `src/discovery/canonical.rs` | Canonical bytes sort parents and field payloads and bind kind, payload, parents, scope, and checker version under a domain-separated hash. |
|
||||||
|
|
||||||
|
The Problem 2.8 failures are polynomial, analytic, asymptotic, and
|
||||||
|
proof-engineering failures. They are not instances of the current Boolean
|
||||||
|
linear `TypedFormula`/`CubeRegion` authorization language. Consequently, no
|
||||||
|
entry in this package is promoted to `AuthorizedHardScar`, even when an exact
|
||||||
|
standalone checker supports the underlying equation.
|
||||||
|
|
||||||
|
## JSON schema choices
|
||||||
|
|
||||||
|
`p28_famm_scars.json` uses the new interchange identifier
|
||||||
|
`mathpunch.p28-famm-scar-bundle.v1`.
|
||||||
|
|
||||||
|
It mirrors the Rust discovery vocabulary without pretending to be a Rust
|
||||||
|
serialization:
|
||||||
|
|
||||||
|
- `kind` uses exact `DiscoveryKind` names.
|
||||||
|
- `parents` use exact `ParentRole` names and bundle-local integer node IDs.
|
||||||
|
- A SoftScar's advisory relationship to its FailureSignature uses
|
||||||
|
`ParentRole::Supports`, never `DerivedFrom`; `CheckedBy` separately links a
|
||||||
|
replay certificate when one exists.
|
||||||
|
- `scope` is a bundle-local unsigned integer resolved through
|
||||||
|
`scope_registry`.
|
||||||
|
- `payload` uses the `Fields` variant as ordered key/value pairs; a future
|
||||||
|
importer must sort them as `canonical.rs` requires.
|
||||||
|
- `checker_version` is an unsigned schema/checker generation.
|
||||||
|
- replay commands, runtimes, artifact paths, and SHA-256 hashes are declared
|
||||||
|
separately in `checker_registry`.
|
||||||
|
|
||||||
|
The bundle intentionally sets these fields to non-authoritative values:
|
||||||
|
|
||||||
|
```text
|
||||||
|
ingested_into_discovery_store = false
|
||||||
|
canonical_node_hashes = null
|
||||||
|
mmr_commitment = null
|
||||||
|
pruning_authority = false
|
||||||
|
```
|
||||||
|
|
||||||
|
Local node and scope IDs must be remapped by an importer. Canonical discovery
|
||||||
|
hashes may be assigned only after the nodes are constructed through the
|
||||||
|
repository's canonical Rust path.
|
||||||
|
|
||||||
|
## Scar catalogue
|
||||||
|
|
||||||
|
Every row below corresponds to an
|
||||||
|
`Observation -> FailureSignature -> SoftScar` chain in the JSON.
|
||||||
|
|
||||||
|
| SoftScar | Exact scope | Failure signature | Assumption avoided | Replay support |
|
||||||
|
|---|---|---|---|---|
|
||||||
|
| `12` | Pinned transfer and package | An under-defined or transcription-divergent matrix is used by later identities | Omitted coefficients are harmless | Dependency-free equation replay |
|
||||||
|
| `22` | Tail contiguity for the displayed \(M_N(x)\) and shifted \({}_4F_3\) jet | CAS Ore division is cited without four cleared residual identities | A zero-remainder routine is itself an inspectable certificate | Dependency-free equation replay |
|
||||||
|
| `32` | Terminating denominator, \(n\ge1\), \(0\le k\le n\) | Fourth-order uniqueness is inferred from normalization at \(z=0\) | One datum determines a fourth-order analytic solution | Base/generic/top coefficient replay |
|
||||||
|
| `42` | Official matrix-to-scalar bridge | A scalar recurrence is accepted without an exact intertwiner | Sample agreement identifies the official module | Sixteen gauge entries and contraction replay |
|
||||||
|
| `52` | Official \(R,x_0\), \(|x|=1/4\), \(m\ge1\) | An inequality is inverted without reversing its direction | Integer powers preserve order for negative exponents | Exact rational convergence checker |
|
||||||
|
| `62` | Official seed rows, four columns, and positive cone | A named transport theorem hides the hypotheses or denominator conclusion | Spectral machinery is necessary for all-column transport | Exact Pascal-conjugated positive transfer and elementary min/max contraction |
|
||||||
|
| `72` | Historical characteristic quartic and displayed eigenvector | Native factor/GCD/root decisions are used as portable exact proof | CAS decisions carry proof authority by default | Exact coefficient homotopy and polynomial eigenvector replay for the retained legacy route |
|
||||||
|
| `82` | Official four columns in the proved positive cone | A quotient is formed before denominator positivity | Formal ratio notation guarantees a nonzero denominator | Exact cone entry and strictly positive transfer entries |
|
||||||
|
| `92` | Mandatory/optional checker split | A stored PASS transcript substitutes for live replay | A receipt proves the current bytes were executed | Mandatory standard-library runner |
|
||||||
|
| `102` | Release metadata | The reciprocal limit is labelled as the official orientation | Equivalent formulas have interchangeable submission labels | Boxed manuscript theorem and official-scope review |
|
||||||
|
| `112` | Wolfram source serialization | A line break terminates an assignment before leading-plus continuation terms | Printed multiline equality equals parsed equality | Parser round-trip is required; current Wolfram run is optional |
|
||||||
|
| `122` | Pinned rational gauge after denominator clearing | Raw rational expansion produces avoidable expression swell or resource failure | Raw rational normal form is required, or capacity failure falsifies the identity | 176 cleared polynomial obligations |
|
||||||
|
| `132` | Official Pascal-conjugated positive cone | Spectral machinery is introduced before testing an elementary positive transport | Eigenvalues and a stable graph are necessary for the official columns | 100 exact positive-cone obligations |
|
||||||
|
| `142` | Advisory FAMM interchange bundle | A SoftScar is linked as an exact derivation rather than advisory support | Advisory diagnosis has exact derivational authority | Structural validator requiring `Supports` and zero hard authority |
|
||||||
|
|
||||||
|
These scars are deliberately narrow:
|
||||||
|
|
||||||
|
- They apply only to the pinned Problem 2.8 objects and proof routes.
|
||||||
|
- They do not assert that Ore methods, scalar recurrences, asymptotic theorems,
|
||||||
|
CAS tools, or reciprocal formulations are invalid in general.
|
||||||
|
- They do not rule out a repaired candidate satisfying the missing equation or
|
||||||
|
hypothesis.
|
||||||
|
|
||||||
|
## Exact replay links
|
||||||
|
|
||||||
|
The advisory scars point to these replayable local artifacts:
|
||||||
|
|
||||||
|
```sh
|
||||||
|
python3 certificates/p28_rank_ode_bound_verifier.py
|
||||||
|
python3 certificates/p28_convergence_constants.py
|
||||||
|
python3 certificates/p28_standalone_equations.py
|
||||||
|
python3 certificates/p28_dominant_product_algebra.py
|
||||||
|
python3 certificates/p28_optimized_gauge.py
|
||||||
|
python3 certificates/p28_positive_cone.py
|
||||||
|
python3 certificates/p28_famm_scars_validator.py
|
||||||
|
```
|
||||||
|
|
||||||
|
The complete mandatory path is:
|
||||||
|
|
||||||
|
```sh
|
||||||
|
bash run_checks.sh
|
||||||
|
```
|
||||||
|
|
||||||
|
Sage and Wolfram files remain optional independent cross-checks. Their absence
|
||||||
|
does not convert a stored transcript into proof evidence.
|
||||||
|
|
||||||
|
Finalized artifact hashes and checker identifiers are in the JSON. Changing a
|
||||||
|
finalized checker, manuscript source, or PDF requires a new replay and a new
|
||||||
|
bundle version.
|
||||||
|
|
||||||
|
## Formula-optimization loop
|
||||||
|
|
||||||
|
Two optimization results change route priority without changing mathematical
|
||||||
|
authority:
|
||||||
|
|
||||||
|
1. The rational gauge is replayed after the diagonal scaling
|
||||||
|
\(D=\operatorname{diag}(x,1,1,1)\) and common clearing by \((1-z)^2\).
|
||||||
|
The resulting companion matrices have bounded polynomial degree, and the
|
||||||
|
checker expands the claim into 176 scalar polynomial obligations. A timeout,
|
||||||
|
capacity rejection, or expression explosion in the unreduced route is a
|
||||||
|
proof-engineering failure, not evidence that the rational identity is false.
|
||||||
|
2. The current all-column proof conjugates the balanced transfer by the exact
|
||||||
|
Pascal matrix, places both official seed rows in a strictly positive cone,
|
||||||
|
and uses the elementary min/max contraction of positive weighted averages.
|
||||||
|
The earlier spectral and stable-graph argument remains an audited historical
|
||||||
|
route, but it is no longer an active prerequisite for the four-column
|
||||||
|
transport or denominator nonvanishing.
|
||||||
|
|
||||||
|
The interchange validator records the corresponding route scars and checks
|
||||||
|
that each SoftScar is advisory: it must have a `Supports` edge from a
|
||||||
|
FailureSignature, may have a separate `CheckedBy` certificate, has no hard
|
||||||
|
authority, and cannot prune.
|
||||||
|
|
||||||
|
## Why no hard scars were emitted
|
||||||
|
|
||||||
|
Three exact-certificate-linked promotion ideas are recorded under
|
||||||
|
`blocked_promotion_ideas`:
|
||||||
|
|
||||||
|
1. nonzero cleared Ore residuals;
|
||||||
|
2. reversed negative-exponent inequalities;
|
||||||
|
3. nonzero matrix-to-scalar intertwiner residuals.
|
||||||
|
|
||||||
|
They are not `ProposedHardScar` or `AuthorizedHardScar` nodes. The present
|
||||||
|
authorizer cannot express their formula domain, region semantics, or
|
||||||
|
minimization rule. Promoting any of them requires all of:
|
||||||
|
|
||||||
|
1. a versioned typed proof-domain formula;
|
||||||
|
2. canonical coefficient or inequality encoding;
|
||||||
|
3. exact applicability-scope semantics;
|
||||||
|
4. a replayable witness;
|
||||||
|
5. a sound minimization rule;
|
||||||
|
6. an authorization certificate;
|
||||||
|
7. reauthorization after persistence;
|
||||||
|
8. hostile tests for forged witness, broadened scope, stale version, altered
|
||||||
|
parent, and valid-candidate pruning attacks.
|
||||||
|
|
||||||
|
Until that machinery exists, the exact certificates support diagnosis and
|
||||||
|
priority only.
|
||||||
|
|
||||||
|
## Import requirements
|
||||||
|
|
||||||
|
A future importer into `DiscoveryStore` must:
|
||||||
|
|
||||||
|
1. register canonical problem, instance, and scope objects;
|
||||||
|
2. run `certificates/p28_famm_scars_validator.py` and reject a malformed role,
|
||||||
|
scope, count, hash pin, or hard-authority claim;
|
||||||
|
3. verify every declared artifact hash;
|
||||||
|
4. execute the mandatory checker commands against those exact bytes;
|
||||||
|
5. translate local IDs to store `NodeId` values;
|
||||||
|
6. construct nodes through the Rust API;
|
||||||
|
7. recompute canonical discovery hashes;
|
||||||
|
8. replay the resulting store and MMR;
|
||||||
|
9. retain every SoftScar as non-pruning;
|
||||||
|
10. leave `blocked_promotion_ideas` outside `HardIndex`.
|
||||||
|
|
||||||
|
Failure at any step is a typed import or replay failure, not evidence that a
|
||||||
|
mathematical proof candidate is impossible.
|
||||||
42
optional/OPTIONAL_IMPROVEMENTS.md
Normal file
42
optional/OPTIONAL_IMPROVEMENTS.md
Normal file
|
|
@ -0,0 +1,42 @@
|
||||||
|
# Problem 2.8 formula-optimization supplements
|
||||||
|
|
||||||
|
These files isolate the formula optimizations developed after the original
|
||||||
|
exact closure. They can be reviewed or replayed independently of the
|
||||||
|
manuscript build.
|
||||||
|
|
||||||
|
## Positive-cone transport
|
||||||
|
|
||||||
|
- `certificates/p28_positive_cone.py`
|
||||||
|
- `certificates/POSITIVE_CONE_CERTIFICATE.md`
|
||||||
|
- `certificates/POSITIVE_CONE_MANUSCRIPT_SECTION.tex`
|
||||||
|
|
||||||
|
The checker reconstructs the authoritative transfer, applies the exact Pascal
|
||||||
|
conjugation, and verifies 100 grouped obligations: all 16 transfer identities,
|
||||||
|
all 285 strictly positive numerator coefficients, positive denominators and
|
||||||
|
limit entries, and both transformed seed rows. In the revised manuscript this
|
||||||
|
elementary contraction is the active all-four-column proof.
|
||||||
|
|
||||||
|
## Optimized differential gauge
|
||||||
|
|
||||||
|
- `certificates/p28_optimized_gauge.py`
|
||||||
|
- `certificates/OPTIMIZED_GAUGE_CERTIFICATE.md`
|
||||||
|
|
||||||
|
The checker clears the rational gauge before expansion and verifies 176 scalar
|
||||||
|
polynomial obligations. It is an optional independent replay; the original
|
||||||
|
16-entry gauge remains in `certificates/p28_standalone_equations.py`.
|
||||||
|
|
||||||
|
## Adversarial and provenance supplements
|
||||||
|
|
||||||
|
- `certificates/p28_mutation_sensitivity.py` corrupts one coefficient in each
|
||||||
|
optimized certificate and requires both altered copies to fail.
|
||||||
|
- `certificates/solution_pre_positive_cone.tex` preserves the complete
|
||||||
|
pre-replacement manuscript.
|
||||||
|
- `FAMM_SCARS.md`, `certificates/p28_famm_scars.json`, and
|
||||||
|
`certificates/p28_famm_scars_validator.py` record scoped advisory failure
|
||||||
|
memory. They grant no hard-pruning authority.
|
||||||
|
|
||||||
|
Replay the complete mandatory path with:
|
||||||
|
|
||||||
|
```sh
|
||||||
|
bash run_checks.sh
|
||||||
|
```
|
||||||
12
optional/Sha256.txt
Normal file
12
optional/Sha256.txt
Normal file
|
|
@ -0,0 +1,12 @@
|
||||||
|
Ramanujan Machine Challenge Problem 2.8
|
||||||
|
Adversarially audited release
|
||||||
|
|
||||||
|
Git commit:
|
||||||
|
492c8ab8717f2e470151330158a8037a4b5f70f1
|
||||||
|
|
||||||
|
SHA-256:
|
||||||
|
a1c11c5f62aad9e1c9eacae54c5f3d8ea4f98de67c6b46cee1354d382df4a60a solution.tex
|
||||||
|
e85d7bf975185905d2b4ba6e3427c4b92735954dd8328589e67a04acab064ae2 solution.pdf
|
||||||
|
a8730d4937b1b4f7811e0b5bcff16163c866e1d24a730dbc70a0e9f00ea11f17 ramanujan_challenge_problem_2_8.zip
|
||||||
|
04394883244d8ba80cea180e9167bcdad4280f80fd6d39df23326621db0ea9dd ramanujan_problem_2_8_adversarially_audited.bundle
|
||||||
|
507124828c056fea30ac87b6206147f14a7fa9fd401338c3f0010311c30f612f ADVERSARIAL_AUDIT.md
|
||||||
235
optional/certificates/OPTIMIZED_GAUGE_CERTIFICATE.md
Normal file
235
optional/certificates/OPTIMIZED_GAUGE_CERTIFICATE.md
Normal file
|
|
@ -0,0 +1,235 @@
|
||||||
|
# Optimized Denominator-Cleared Gauge Certificate
|
||||||
|
|
||||||
|
This note accompanies `p28_optimized_gauge.py`. It is an additive
|
||||||
|
certificate: the original sixteen-entry gauge check in
|
||||||
|
`p28_standalone_equations.py` remains unchanged.
|
||||||
|
|
||||||
|
The optimization removes large temporary rational denominators before the
|
||||||
|
matrix products are formed. It does not remove any gauge entry or replace an
|
||||||
|
exact equality by sampling.
|
||||||
|
|
||||||
|
## 1. Regularized transfer
|
||||||
|
|
||||||
|
Let
|
||||||
|
|
||||||
|
\[
|
||||||
|
D=\operatorname{diag}(x,1,1,1),\qquad
|
||||||
|
J(u,x)=D\mathcal M(u,x),\qquad
|
||||||
|
w=u(3u-2)(3u+2).
|
||||||
|
\]
|
||||||
|
|
||||||
|
Put
|
||||||
|
|
||||||
|
\[
|
||||||
|
v=(u^3,3u^2,3u,1),\qquad
|
||||||
|
\alpha=\frac{144(u-1)^2}{w},\qquad
|
||||||
|
\beta=\frac{2u-9}{2}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
The checker verifies all sixteen entries of
|
||||||
|
|
||||||
|
\[
|
||||||
|
J(u,x)=J_0(u)+xJ_1(u)+x^2J_2(u),
|
||||||
|
\]
|
||||||
|
|
||||||
|
where
|
||||||
|
|
||||||
|
\[
|
||||||
|
J_0=
|
||||||
|
\begin{pmatrix}
|
||||||
|
\alpha\\-1\\-1\\-1
|
||||||
|
\end{pmatrix}v
|
||||||
|
\]
|
||||||
|
|
||||||
|
and
|
||||||
|
|
||||||
|
\[
|
||||||
|
J_1=
|
||||||
|
\begin{pmatrix}
|
||||||
|
\mathbf a/w\\
|
||||||
|
0\\
|
||||||
|
\mathbf b\\
|
||||||
|
\mathbf c
|
||||||
|
\end{pmatrix}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Here
|
||||||
|
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
\mathbf a={}&\bigl(
|
||||||
|
-99u^5+333u^4-229u^3-114u^2+40u+64,\\
|
||||||
|
&-243u^4+909u^3-868u^2-80u+272,\\
|
||||||
|
&-153u^3+648u^2-860u+360,\ 0\bigr),
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
\mathbf b=\left(
|
||||||
|
\frac{(u+1)(u+2)(3u+4)(3u+8)}{144},
|
||||||
|
\frac{-36u^3+189u^2+316u+168}{72},
|
||||||
|
\frac{-54u^2+189u+158}{36},
|
||||||
|
\frac{7-2u}{2}
|
||||||
|
\right),
|
||||||
|
\]
|
||||||
|
|
||||||
|
and
|
||||||
|
|
||||||
|
\[
|
||||||
|
\mathbf c=\left(
|
||||||
|
\frac{(u+1)(u+2)(3u+4)(3u+8)}{48},
|
||||||
|
\frac{153u^4-657u^3+1292u^2+2064u+1072}{144},
|
||||||
|
\frac{180u^3-891u^2+1450u+1116}{72},
|
||||||
|
\frac{54u^2-297u+536}{36}
|
||||||
|
\right).
|
||||||
|
\]
|
||||||
|
|
||||||
|
The matrix \(J_2\) is entered independently from the finite parts of the
|
||||||
|
four authoritative \(c_i\). The checker then verifies, entry by entry,
|
||||||
|
|
||||||
|
\[
|
||||||
|
J_2=e_4\,\beta\mathbf b.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Thus the useful proportionality is proved rather than built into both sides
|
||||||
|
of the check.
|
||||||
|
|
||||||
|
## 2. Common denominator in the \(z\)-gauge
|
||||||
|
|
||||||
|
Set
|
||||||
|
|
||||||
|
\[
|
||||||
|
x=-\frac{z}{1-z},\qquad u=2n+1,
|
||||||
|
\]
|
||||||
|
|
||||||
|
and
|
||||||
|
|
||||||
|
\[
|
||||||
|
G_n(z)=-z\mathcal M\left(2n+1,-\frac{z}{1-z}\right).
|
||||||
|
\]
|
||||||
|
|
||||||
|
Since
|
||||||
|
|
||||||
|
\[
|
||||||
|
-zD^{-1}
|
||||||
|
=\operatorname{diag}(1-z,-z,-z,-z),
|
||||||
|
\]
|
||||||
|
|
||||||
|
the common-denominator-cleared matrix is
|
||||||
|
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
\overline G_n
|
||||||
|
&=(1-z)^2G_n\\
|
||||||
|
&=\operatorname{diag}(1-z,-z,-z,-z)
|
||||||
|
\left[
|
||||||
|
(1-z)^2J_0-z(1-z)J_1+z^2J_2
|
||||||
|
\right]_{u=2n+1}.
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
|
||||||
|
The checker independently substitutes into the original displayed matrix
|
||||||
|
and verifies all sixteen entries of
|
||||||
|
|
||||||
|
\[
|
||||||
|
\overline G_n=(1-z)^2G_n.
|
||||||
|
\]
|
||||||
|
|
||||||
|
## 3. Cleared companion matrices
|
||||||
|
|
||||||
|
For
|
||||||
|
|
||||||
|
\[
|
||||||
|
\mathcal L_n(t)=
|
||||||
|
t(t+2n-1)^3
|
||||||
|
-z(t+n)(t+n+\tfrac16)(t+n+\tfrac12)(t+n+\tfrac56),
|
||||||
|
\]
|
||||||
|
|
||||||
|
let \(\mathcal C_n\) be its companion matrix. The leading coefficient of
|
||||||
|
\(\mathcal L_n\) is \(1-z\). Define
|
||||||
|
|
||||||
|
\[
|
||||||
|
\overline{\mathcal C}_n=(1-z)\mathcal C_n.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Both identities
|
||||||
|
|
||||||
|
\[
|
||||||
|
\overline{\mathcal C}_n=(1-z)\mathcal C_n,\qquad
|
||||||
|
\overline{\mathcal C}_{n+1}=(1-z)\mathcal C_{n+1}
|
||||||
|
\]
|
||||||
|
|
||||||
|
are checked in all sixteen entries.
|
||||||
|
|
||||||
|
## 4. Quotient-rule conversion
|
||||||
|
|
||||||
|
Put \(d=(1-z)^2\). For every actual entry of \(\overline G_n\), the checker
|
||||||
|
verifies
|
||||||
|
|
||||||
|
\[
|
||||||
|
d(1-z)\,\theta\left(\frac{\overline G_{n,ij}}d\right)
|
||||||
|
=(1-z)z\,\partial_z\overline G_{n,ij}
|
||||||
|
+2z\overline G_{n,ij},
|
||||||
|
\qquad \theta=z\partial_z.
|
||||||
|
\]
|
||||||
|
|
||||||
|
This is the exact product/quotient-rule step used to pass from the original
|
||||||
|
rational gauge to the cleared polynomial gauge.
|
||||||
|
|
||||||
|
Multiplying
|
||||||
|
|
||||||
|
\[
|
||||||
|
\mathcal C_nG_n-\theta G_n-G_n\mathcal C_{n+1}=0
|
||||||
|
\]
|
||||||
|
|
||||||
|
by \(d(1-z)\) therefore gives
|
||||||
|
|
||||||
|
\[
|
||||||
|
\boxed{
|
||||||
|
\overline{\mathcal C}_n\overline G_n
|
||||||
|
-(1-z)z\,\partial_z\overline G_n
|
||||||
|
-2z\overline G_n
|
||||||
|
-\overline G_n\overline{\mathcal C}_{n+1}=0.
|
||||||
|
}
|
||||||
|
\]
|
||||||
|
|
||||||
|
Every entry of \(\overline G_n\) has \(z\)-degree at most three, and every
|
||||||
|
entry of \(\overline{\mathcal C}_n\) has degree at most one. Consequently
|
||||||
|
each boxed residual has degree at most four. The checker tests the
|
||||||
|
coefficients of \(z^0,\ldots,z^4\) separately in every one of the sixteen
|
||||||
|
entries.
|
||||||
|
|
||||||
|
## 5. Exact obligations
|
||||||
|
|
||||||
|
| Obligation | Scalar equalities |
|
||||||
|
|---|---:|
|
||||||
|
| \(J_2=e_4\beta\mathbf b\) | 16 |
|
||||||
|
| \(D\mathcal M=J_0+xJ_1+x^2J_2\) | 16 |
|
||||||
|
| \(\overline G=(1-z)^2G\) | 16 |
|
||||||
|
| \(\overline{\mathcal C}_n=(1-z)\mathcal C_n\) | 16 |
|
||||||
|
| \(\overline{\mathcal C}_{n+1}=(1-z)\mathcal C_{n+1}\) | 16 |
|
||||||
|
| Entrywise quotient-rule conversion | 16 |
|
||||||
|
| Five \(z\)-coefficients in each of sixteen gauge entries | 80 |
|
||||||
|
| **Total** | **176** |
|
||||||
|
|
||||||
|
All 176 obligations are sparse-polynomial equalities over
|
||||||
|
\(\mathbb Q(u,x,n,z,t)\). A check passes only when the expanded numerator
|
||||||
|
has an empty coefficient dictionary.
|
||||||
|
|
||||||
|
The verifier implements rational addition, multiplication, integer powers,
|
||||||
|
formal differentiation, substitution, and coefficient extraction itself.
|
||||||
|
It does not use a CAS simplifier, polynomial division, factorization,
|
||||||
|
Gröbner bases, special-function evaluation, a root finder, or numerical
|
||||||
|
sampling.
|
||||||
|
|
||||||
|
## 6. Replay
|
||||||
|
|
||||||
|
From the submission directory:
|
||||||
|
|
||||||
|
```sh
|
||||||
|
python3 certificates/p28_optimized_gauge.py
|
||||||
|
```
|
||||||
|
|
||||||
|
A reference run in the proof workspace completed all 176 exact obligations
|
||||||
|
in approximately \(1.22\) seconds. Runtime is informational; correctness
|
||||||
|
depends only on the exact zero-coefficient checks.
|
||||||
331
optional/certificates/POSITIVE_CONE_CERTIFICATE.md
Normal file
331
optional/certificates/POSITIVE_CONE_CERTIFICATE.md
Normal file
|
|
@ -0,0 +1,331 @@
|
||||||
|
# Positive-Cone Certificate for Problem 2.8
|
||||||
|
|
||||||
|
This sheet gives an exact alternative to the spectral/stable-graph reduction
|
||||||
|
for the four official columns. It does not replace any existing certificate.
|
||||||
|
|
||||||
|
Let
|
||||||
|
|
||||||
|
\[
|
||||||
|
\mathcal P=
|
||||||
|
\begin{pmatrix}
|
||||||
|
1&0&0&0\\
|
||||||
|
1&1&0&0\\
|
||||||
|
1&2&1&0\\
|
||||||
|
1&3&3&1
|
||||||
|
\end{pmatrix},
|
||||||
|
\qquad
|
||||||
|
\mathcal P^{-1}=
|
||||||
|
\begin{pmatrix}
|
||||||
|
1&0&0&0\\
|
||||||
|
-1&1&0&0\\
|
||||||
|
1&-2&1&0\\
|
||||||
|
-1&3&-3&1
|
||||||
|
\end{pmatrix}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
For
|
||||||
|
|
||||||
|
\[
|
||||||
|
D_m=\operatorname{diag}(1,m,m^2,m^3),\qquad
|
||||||
|
\mathcal B_m=D_m^{-1}M_mD_{m+1}/(m+1)^2,
|
||||||
|
\]
|
||||||
|
|
||||||
|
put
|
||||||
|
|
||||||
|
\[
|
||||||
|
T_m=\mathcal P\mathcal B_m\mathcal P^{-1}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
The accompanying dependency-free verifier constructs the authoritative
|
||||||
|
matrix \(M_m\) directly. It does not import a matrix-data module.
|
||||||
|
|
||||||
|
## 1. Positive rational form
|
||||||
|
|
||||||
|
Set
|
||||||
|
|
||||||
|
\[
|
||||||
|
k=m-1,\qquad s=R-4,\qquad
|
||||||
|
g_m=(2m+3)(6m+7)(6m+11).
|
||||||
|
\]
|
||||||
|
|
||||||
|
For each \(i,j\),
|
||||||
|
|
||||||
|
\[
|
||||||
|
(T_m)_{ij}=\frac{N_{ij}(k,s)}{D_{ij}(m,R)}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
The denominator matrix is
|
||||||
|
|
||||||
|
\[
|
||||||
|
(D_{ij})=
|
||||||
|
\begin{pmatrix}
|
||||||
|
(m+1)^2g_m&(m+1)g_m&g_m&g_m\\
|
||||||
|
mg_m&m(m+1)g_m&mg_m&mg_m\\
|
||||||
|
24m^2(m+1)^2g_mR&72m^2(m+1)g_mR&
|
||||||
|
36m^2g_mR&2m^2g_mR\\
|
||||||
|
48m^3(m+1)^2g_mR^2&144m^3(m+1)g_mR^2&
|
||||||
|
72m^3g_mR^2&36m^3g_mR^2
|
||||||
|
\end{pmatrix}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Every denominator is positive for \(m\ge1\) and \(R\ge4\).
|
||||||
|
|
||||||
|
To list the numerators compactly, if
|
||||||
|
|
||||||
|
\[
|
||||||
|
\mathcal C_{ij}=(c_{ab})_
|
||||||
|
{\substack{0\le a\le d_{ij}\\0\le b\le e_{ij}}},
|
||||||
|
\]
|
||||||
|
|
||||||
|
write
|
||||||
|
|
||||||
|
\[
|
||||||
|
[\mathcal C_{ij}]
|
||||||
|
=\sum_{a=0}^{d_{ij}}k^a
|
||||||
|
\sum_{b=0}^{e_{ij}}c_{ab}s^b.
|
||||||
|
\]
|
||||||
|
|
||||||
|
The complete coefficient arrays are:
|
||||||
|
|
||||||
|
```text
|
||||||
|
C11 = [[209067,62208],[409482,124416],[318165,98496],
|
||||||
|
[122806,38592],[23580,7488],[1800,576]]
|
||||||
|
C12 = [[216214,62208],[351120,103680],[210784,63936],
|
||||||
|
[55584,17280],[5472,1728]]
|
||||||
|
C13 = [[76079,20736],[98882,27648],[41796,12096],[5688,1728]]
|
||||||
|
C14 = [[18432,4608],[27648,6912],[13824,3456],[2304,576]]
|
||||||
|
|
||||||
|
C21 = [[44808,15552],[93312,31104],[62208,20736],
|
||||||
|
[17280,5760],[1728,576]]
|
||||||
|
C22 = [[186379,62208],[511210,165888],[519853,167616],
|
||||||
|
[250678,81216],[58140,19008],[5256,1728]]
|
||||||
|
C23 = [[66134,20736],[159568,48384],[131792,39744],
|
||||||
|
[45216,13824],[5472,1728]]
|
||||||
|
C24 = [[16222,4608],[42291,11520],[39050,10368],
|
||||||
|
[15444,4032],[2232,576]]
|
||||||
|
|
||||||
|
C31 = [[12995117,8841456,1492992],[58685630,37561608,5971968],
|
||||||
|
[103594644,64078200,9828864],[94855680,57551496,8640000],
|
||||||
|
[49440456,29668248,4396032],[14835888,8843664,1299456],
|
||||||
|
[2392416,1419552,207360],[160704,95040,13824]]
|
||||||
|
C32 = [[39423757,27038952,4478976],[166410214,105688080,16422912],
|
||||||
|
[262665540,160189416,24012288],[203963976,121854816,17915904],
|
||||||
|
[83704320,49549824,7216128],[17449344,10295424,1492992],
|
||||||
|
[1461888,860544,124416]]
|
||||||
|
C33 = [[6744221,4650768,746496],[26619818,16612236,2488320],
|
||||||
|
[37076724,21985452,3172608],[23503608,13602888,1928448],
|
||||||
|
[6902496,3967056,559872],[756864,438048,62208]]
|
||||||
|
C34 = [[87786,60468,9216],[369593,226474,32256],
|
||||||
|
[559242,320520,43776],[393892,216608,28800],
|
||||||
|
[131832,70560,9216],[16992,8928,1152]]
|
||||||
|
|
||||||
|
C41 = [[33051981,55702072,23898528,2985984],
|
||||||
|
[327240514,376865532,134112240,14929920],
|
||||||
|
[930970540,937602272,303903216,31601664],
|
||||||
|
[1279073232,1205376648,370469520,36937728],
|
||||||
|
[994303368,902431272,268543536,26072064],
|
||||||
|
[461588688,409453104,119369664,11390976],
|
||||||
|
[127105056,111089760,31948032,3013632],
|
||||||
|
[19185984,16597440,4727808,442368],
|
||||||
|
[1223424,1050624,297216,27648]]
|
||||||
|
C42 = [[124354341,177927470,72724752,8957952],
|
||||||
|
[1045995002,1120727784,383156784,41803776],
|
||||||
|
[2641611740,2536092136,794391552,80870400],
|
||||||
|
[3164847768,2875298832,858173328,83856384],
|
||||||
|
[2060023392,1815713424,527093136,50264064],
|
||||||
|
[748445184,648617760,185300064,17418240],
|
||||||
|
[142860672,122627520,34706880,3234816],
|
||||||
|
[11197440,9548928,2685312,248832]]
|
||||||
|
C43 = [[26276833,32297441,12409344,1492992],
|
||||||
|
[188851718,188046502,61107192,6469632],
|
||||||
|
[420585148,383136068,114774408,11321856],
|
||||||
|
[431847432,375502536,107664480,10202112],
|
||||||
|
[225990144,191691072,53691264,4976640],
|
||||||
|
[58320000,48926592,13561344,1244160],
|
||||||
|
[5847552,4904064,1358208,124416]]
|
||||||
|
C44 = [[3759202,4035454,1433736,165888],
|
||||||
|
[25198317,23609115,7287084,746496],
|
||||||
|
[57385334,50066438,14346252,1368576],
|
||||||
|
[62533980,52200252,14310108,1306368],
|
||||||
|
[35688168,28926216,7710120,684288],
|
||||||
|
[10310976,8188128,2142288,186624],
|
||||||
|
[1192320,933120,241056,20736]]
|
||||||
|
```
|
||||||
|
|
||||||
|
Here \(N_{ij}=[\mathcal C_{ij}]\). Every listed coefficient is strictly
|
||||||
|
positive. Therefore
|
||||||
|
|
||||||
|
\[
|
||||||
|
\boxed{T_m>0\quad(m\ge1,\ R\ge4).}
|
||||||
|
\]
|
||||||
|
|
||||||
|
This is a bivariate coefficient identity, not a finite test.
|
||||||
|
|
||||||
|
## 2. Positive limiting transfer
|
||||||
|
|
||||||
|
Exact leading-coefficient comparison gives
|
||||||
|
|
||||||
|
\[
|
||||||
|
\lim_{m\to\infty}T_m=
|
||||||
|
\begin{pmatrix}
|
||||||
|
8R-7&4(6R-5)&24R-17&8R\\
|
||||||
|
8(R-1)&24R-23&4(6R-5)&8R-1\\
|
||||||
|
\frac{(R-1)(8R-1)}R&
|
||||||
|
\frac{2(R-1)(12R-1)}R&
|
||||||
|
24R-23&
|
||||||
|
\frac{2(4R^2-R-1)}R\\
|
||||||
|
\frac{2(R-1)(4R^2-R-1)}{R^2}&
|
||||||
|
\frac{(R-1)(24R^2-5R-4)}{R^2}&
|
||||||
|
\frac{2(R-1)(12R-1)}R&
|
||||||
|
\frac{8R^3-3R^2-4}{R^2}
|
||||||
|
\end{pmatrix}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Every entry is positive for \(R\ge4\).
|
||||||
|
|
||||||
|
## 3. The official rows enter the cone
|
||||||
|
|
||||||
|
Let
|
||||||
|
|
||||||
|
\[
|
||||||
|
Y_m(a)=\frac{aG_mD_m}{(m!)^2}\mathcal P^{-1}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Since \(D_1=I\) and \(G_1=M_0\), put \(s=R-4\). Direct expansion gives
|
||||||
|
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
Y_1(A_1)=\bigg(&
|
||||||
|
\frac{320160}{77}(451657+259168s+36864s^2),\\
|
||||||
|
&
|
||||||
|
\frac{213440}{77}(1045771+591288s+82944s^2),\\
|
||||||
|
&
|
||||||
|
\frac{3841920}{77}(30075+16706s+2304s^2),\\
|
||||||
|
&
|
||||||
|
\frac{7683840}{77}(2612+1421s+192s^2)
|
||||||
|
\bigg)
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
|
||||||
|
and
|
||||||
|
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
Y_1(A_0)=\bigg(&
|
||||||
|
\frac{13563858344917+18828949838688s+4509303312384s^2}{924},\\
|
||||||
|
&
|
||||||
|
\frac{2(2606908232573+3613607517834s+845494371072s^2)}{231},\\
|
||||||
|
&
|
||||||
|
\frac{3584820267815+4955797147464s+1127325828096s^2}{308},\\
|
||||||
|
&
|
||||||
|
\frac{3(103400761441+142363659388s+31314606336s^2)}{154}
|
||||||
|
\bigg).
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
|
||||||
|
Thus both rows are strictly positive for \(R\ge4\), and positivity is
|
||||||
|
preserved by every subsequent \(T_m\).
|
||||||
|
|
||||||
|
## 4. Elementary projective contraction
|
||||||
|
|
||||||
|
Let
|
||||||
|
|
||||||
|
\[
|
||||||
|
p_m=Y_m(A_0),\qquad q_m=Y_m(A_1),\qquad
|
||||||
|
r_{m,i}=\frac{p_{m,i}}{q_{m,i}}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
The common recurrence \(p_{m+1}=p_mT_m\),
|
||||||
|
\(q_{m+1}=q_mT_m\) gives
|
||||||
|
|
||||||
|
\[
|
||||||
|
r_{m+1,j}
|
||||||
|
=\sum_{i=1}^4\omega^{(m)}_{ij}r_{m,i},
|
||||||
|
\qquad
|
||||||
|
\omega^{(m)}_{ij}
|
||||||
|
=\frac{q_{m,i}(T_m)_{ij}}
|
||||||
|
{\sum_hq_{m,h}(T_m)_{hj}},
|
||||||
|
\]
|
||||||
|
|
||||||
|
with
|
||||||
|
|
||||||
|
\[
|
||||||
|
\omega^{(m)}_{ij}>0,\qquad
|
||||||
|
\sum_i\omega^{(m)}_{ij}=1.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Because \(T_m\) converges to a strictly positive matrix, there are
|
||||||
|
\(0<a<b\) such that eventually
|
||||||
|
|
||||||
|
\[
|
||||||
|
a\le(T_m)_{ij}\le b.
|
||||||
|
\]
|
||||||
|
|
||||||
|
After one such step,
|
||||||
|
|
||||||
|
\[
|
||||||
|
\frac ab\le\frac{q_{m,i}}{q_{m,j}}\le\frac ba.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Hence every weight is bounded below by
|
||||||
|
|
||||||
|
\[
|
||||||
|
\omega^{(m)}_{ij}\ge
|
||||||
|
\delta:=\frac{a^2}{4b^2}>0.
|
||||||
|
\]
|
||||||
|
|
||||||
|
For
|
||||||
|
|
||||||
|
\[
|
||||||
|
\ell_m=\min_i r_{m,i},\qquad
|
||||||
|
u_m=\max_i r_{m,i},
|
||||||
|
\]
|
||||||
|
|
||||||
|
the weight on an index attaining each endpoint gives
|
||||||
|
|
||||||
|
\[
|
||||||
|
\ell_m+\delta(u_m-\ell_m)
|
||||||
|
\le r_{m+1,j}\le
|
||||||
|
u_m-\delta(u_m-\ell_m).
|
||||||
|
\]
|
||||||
|
|
||||||
|
Therefore
|
||||||
|
|
||||||
|
\[
|
||||||
|
u_{m+1}-\ell_{m+1}
|
||||||
|
\le(1-2\delta)(u_m-\ell_m),
|
||||||
|
\]
|
||||||
|
|
||||||
|
so all four \(r_{m,i}\) converge to one positive constant \(c\).
|
||||||
|
|
||||||
|
Finally,
|
||||||
|
|
||||||
|
\[
|
||||||
|
Z_m(a)=Y_m(a)\mathcal P.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Every column of \(\mathcal P\) is nonzero and nonnegative, so each quotient
|
||||||
|
|
||||||
|
\[
|
||||||
|
\frac{Z_m(A_0)_j}{Z_m(A_1)_j}
|
||||||
|
\]
|
||||||
|
|
||||||
|
is another weighted average of the four \(r_{m,i}\). It tends to \(c\).
|
||||||
|
The balancing factors cancel, and the already-proved first-column limit
|
||||||
|
identifies
|
||||||
|
|
||||||
|
\[
|
||||||
|
c=\frac{\sqrt{10005}}{\pi}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
## 5. Replay
|
||||||
|
|
||||||
|
From the submission directory:
|
||||||
|
|
||||||
|
```sh
|
||||||
|
python3 certificates/p28_positive_cone.py
|
||||||
|
```
|
||||||
|
|
||||||
|
The script uses rational coefficient dictionaries only. It performs no
|
||||||
|
sampling, polynomial division, factorization, simplification, root finding,
|
||||||
|
or eigenvalue computation.
|
||||||
192
optional/certificates/POSITIVE_CONE_MANUSCRIPT_SECTION.tex
Normal file
192
optional/certificates/POSITIVE_CONE_MANUSCRIPT_SECTION.tex
Normal file
|
|
@ -0,0 +1,192 @@
|
||||||
|
\section{The other three official columns}
|
||||||
|
|
||||||
|
All matrices in this section are evaluated at \(x=x_0=1/R\). For \(m\ge1\),
|
||||||
|
retain
|
||||||
|
\[
|
||||||
|
D_m=\diag(1,m,m^2,m^3),\qquad
|
||||||
|
\mathcal B_m=D_m^{-1}M_mD_{m+1}/(m+1)^2
|
||||||
|
\]
|
||||||
|
and put
|
||||||
|
\[
|
||||||
|
Z_m(a)=\frac{aG_mD_m}{(m!)^2},\qquad
|
||||||
|
Y_m(a)=Z_m(a)\mathcal P^{-1},\qquad
|
||||||
|
T_m=\mathcal P\mathcal B_m\mathcal P^{-1}.
|
||||||
|
\]
|
||||||
|
The balancing gives the exact row recurrence
|
||||||
|
\begin{equation}\label{eq:positive-row-recurrence}
|
||||||
|
Y_{m+1}(a)=Y_m(a)T_m.
|
||||||
|
\end{equation}
|
||||||
|
|
||||||
|
Set \(k=m-1\), \(s=R-4\), and
|
||||||
|
\[
|
||||||
|
g_m=(2m+3)(6m+7)(6m+11).
|
||||||
|
\]
|
||||||
|
Direct cross multiplication of the authoritative matrix gives
|
||||||
|
\begin{equation}\label{eq:positive-transfer}
|
||||||
|
(T_m)_{ij}=\frac{N_{ij}(k,s)}{D_{ij}(m,R)},
|
||||||
|
\end{equation}
|
||||||
|
where
|
||||||
|
\[
|
||||||
|
(D_{ij})=
|
||||||
|
\begin{pmatrix}
|
||||||
|
(m+1)^2g_m&(m+1)g_m&g_m&g_m\\
|
||||||
|
mg_m&m(m+1)g_m&mg_m&mg_m\\
|
||||||
|
24m^2(m+1)^2g_mR&72m^2(m+1)g_mR&
|
||||||
|
36m^2g_mR&2m^2g_mR\\
|
||||||
|
48m^3(m+1)^2g_mR^2&144m^3(m+1)g_mR^2&
|
||||||
|
72m^3g_mR^2&36m^3g_mR^2
|
||||||
|
\end{pmatrix}.
|
||||||
|
\]
|
||||||
|
Each numerator has the form
|
||||||
|
\[
|
||||||
|
N_{ij}(k,s)=\sum_{a,b}c^{(ij)}_{ab}k^as^b,
|
||||||
|
\qquad c^{(ij)}_{ab}>0.
|
||||||
|
\]
|
||||||
|
For example,
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
N_{11}={}&209067+62208s+(409482+124416s)k\\
|
||||||
|
&+(318165+98496s)k^2+(122806+38592s)k^3\\
|
||||||
|
&+(23580+7488s)k^4+(1800+576s)k^5.
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
The complete finite list of all \(285\) positive integers
|
||||||
|
\(c^{(ij)}_{ab}\) is printed in
|
||||||
|
\texttt{POSITIVE\_CONE\_CERTIFICATE.md}. The dependency-free verifier
|
||||||
|
\texttt{p28\_positive\_cone.py} reconstructs \(M_m,\mathcal B_m,T_m\),
|
||||||
|
cross-multiplies every one of the sixteen identities
|
||||||
|
\eqref{eq:positive-transfer}, and compares every coefficient with that
|
||||||
|
list. Thus, without sampling or a positivity oracle,
|
||||||
|
\begin{equation}\label{eq:T-positive}
|
||||||
|
\boxed{T_m>0\quad\text{entrywise for every }m\ge1,\ R\ge4.}
|
||||||
|
\end{equation}
|
||||||
|
|
||||||
|
Leading coefficients in \(k\), checked by the same exact arithmetic, give
|
||||||
|
\[
|
||||||
|
\widetilde{\mathcal S}:=\lim_{m\to\infty}T_m=
|
||||||
|
\begin{pmatrix}
|
||||||
|
8R-7&4(6R-5)&24R-17&8R\\
|
||||||
|
8(R-1)&24R-23&4(6R-5)&8R-1\\
|
||||||
|
\frac{(R-1)(8R-1)}R&
|
||||||
|
\frac{2(R-1)(12R-1)}R&
|
||||||
|
24R-23&
|
||||||
|
\frac{2(4R^2-R-1)}R\\
|
||||||
|
\frac{2(R-1)(4R^2-R-1)}{R^2}&
|
||||||
|
\frac{(R-1)(24R^2-5R-4)}{R^2}&
|
||||||
|
\frac{2(R-1)(12R-1)}R&
|
||||||
|
\frac{8R^3-3R^2-4}{R^2}
|
||||||
|
\end{pmatrix}.
|
||||||
|
\]
|
||||||
|
Every displayed entry is positive for \(R\ge4\).
|
||||||
|
|
||||||
|
Both official rows enter this cone after the first transfer. Indeed
|
||||||
|
\(D_1=I\), \(G_1=M_0\), and exact expansion gives
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
Y_1(A_1)=\bigg(&
|
||||||
|
\frac{320160}{77}(451657+259168s+36864s^2),\\
|
||||||
|
&\frac{213440}{77}(1045771+591288s+82944s^2),\\
|
||||||
|
&\frac{3841920}{77}(30075+16706s+2304s^2),\\
|
||||||
|
&\frac{7683840}{77}(2612+1421s+192s^2)\bigg)
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
and
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
Y_1(A_0)=\bigg(&
|
||||||
|
\frac{13563858344917+18828949838688s+4509303312384s^2}{924},\\
|
||||||
|
&\frac{2(2606908232573+3613607517834s+845494371072s^2)}{231},\\
|
||||||
|
&\frac{3584820267815+4955797147464s+1127325828096s^2}{308},\\
|
||||||
|
&\frac{3(103400761441+142363659388s+31314606336s^2)}{154}\bigg).
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
Hence
|
||||||
|
\begin{equation}\label{eq:positive-seeds}
|
||||||
|
Y_m(A_0)>0,\qquad Y_m(A_1)>0\qquad(m\ge1).
|
||||||
|
\end{equation}
|
||||||
|
|
||||||
|
\begin{lemma}[Elementary positive-cone contraction]
|
||||||
|
\label{lem:positive-cone}
|
||||||
|
For every \(j=1,2,3,4\), the quotient
|
||||||
|
\[
|
||||||
|
\frac{A_0G_m\e_j}{A_1G_m\e_j}
|
||||||
|
\]
|
||||||
|
is defined for \(m\ge1\), and all four quotients have one common limit.
|
||||||
|
\end{lemma}
|
||||||
|
|
||||||
|
\begin{proof}
|
||||||
|
Write
|
||||||
|
\[
|
||||||
|
p_m=Y_m(A_0),\qquad q_m=Y_m(A_1),\qquad
|
||||||
|
r_{m,i}=\frac{p_{m,i}}{q_{m,i}}.
|
||||||
|
\]
|
||||||
|
Equations \eqref{eq:positive-row-recurrence} and
|
||||||
|
\eqref{eq:positive-seeds} give
|
||||||
|
\[
|
||||||
|
r_{m+1,j}=\sum_{i=1}^4\omega^{(m)}_{ij}r_{m,i},
|
||||||
|
\qquad
|
||||||
|
\omega^{(m)}_{ij}
|
||||||
|
=\frac{q_{m,i}(T_m)_{ij}}
|
||||||
|
{\sum_{h=1}^4q_{m,h}(T_m)_{hj}},
|
||||||
|
\]
|
||||||
|
where
|
||||||
|
\[
|
||||||
|
\omega^{(m)}_{ij}>0,\qquad
|
||||||
|
\sum_{i=1}^4\omega^{(m)}_{ij}=1.
|
||||||
|
\]
|
||||||
|
Since \(T_m\to\widetilde{\mathcal S}>0\), there are \(m_0\) and
|
||||||
|
\(0<a<b\) such that
|
||||||
|
\[
|
||||||
|
a\le(T_m)_{ij}\le b\qquad(m\ge m_0;\ 1\le i,j\le4).
|
||||||
|
\]
|
||||||
|
One such positive step implies
|
||||||
|
\[
|
||||||
|
\frac ab\le\frac{q_{m+1,i}}{q_{m+1,j}}\le\frac ba.
|
||||||
|
\]
|
||||||
|
Consequently, for \(m\ge m_0+1\),
|
||||||
|
\[
|
||||||
|
\omega^{(m)}_{ij}\ge
|
||||||
|
\delta:=\frac{a^2}{4b^2}>0.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Let
|
||||||
|
\[
|
||||||
|
\ell_m=\min_i r_{m,i},\qquad u_m=\max_i r_{m,i}.
|
||||||
|
\]
|
||||||
|
Every \(r_{m+1,j}\) is a convex combination of the preceding four ratios,
|
||||||
|
so \(\ell_m\) is nondecreasing and \(u_m\) is nonincreasing. The weights
|
||||||
|
on indices attaining the two endpoints are at least \(\delta\), whence
|
||||||
|
\[
|
||||||
|
\ell_m+\delta(u_m-\ell_m)
|
||||||
|
\le r_{m+1,j}\le
|
||||||
|
u_m-\delta(u_m-\ell_m)
|
||||||
|
\]
|
||||||
|
and
|
||||||
|
\[
|
||||||
|
u_{m+1}-\ell_{m+1}
|
||||||
|
\le(1-2\delta)(u_m-\ell_m).
|
||||||
|
\]
|
||||||
|
Thus all four \(r_{m,i}\) tend to one positive constant \(c\).
|
||||||
|
|
||||||
|
Finally \(Z_m(a)=Y_m(a)\mathcal P\). Every column of \(\mathcal P\) is
|
||||||
|
nonzero and nonnegative, so
|
||||||
|
\[
|
||||||
|
\frac{Z_m(A_0)_j}{Z_m(A_1)_j}
|
||||||
|
=
|
||||||
|
\frac{\sum_iq_{m,i}(\mathcal P)_{ij}r_{m,i}}
|
||||||
|
{\sum_iq_{m,i}(\mathcal P)_{ij}}
|
||||||
|
\]
|
||||||
|
is defined and is another convex combination of the \(r_{m,i}\). It tends
|
||||||
|
to \(c\). Since
|
||||||
|
\[
|
||||||
|
Z_m(a)_j=\frac{m^{j-1}}{(m!)^2}aG_m\e_j,
|
||||||
|
\]
|
||||||
|
the same is true of the four official quotients.
|
||||||
|
\end{proof}
|
||||||
|
|
||||||
|
The first-column identity \eqref{eq:first-column} fixes their common value:
|
||||||
|
\[
|
||||||
|
\lim_{m\to\infty}\frac{P_{m,j}}{Q_{m,j}}
|
||||||
|
=\frac{\sqrt{10005}}{\pi}
|
||||||
|
\qquad(j=1,2,3,4).
|
||||||
|
\]
|
||||||
1131
optional/certificates/p28_famm_scars.json
Normal file
1131
optional/certificates/p28_famm_scars.json
Normal file
File diff suppressed because it is too large
Load diff
167
optional/certificates/p28_famm_scars_validator.py
Normal file
167
optional/certificates/p28_famm_scars_validator.py
Normal file
|
|
@ -0,0 +1,167 @@
|
||||||
|
#!/usr/bin/env python3
|
||||||
|
"""Fail-closed structural validation for the Problem 2.8 FAMM scar bundle.
|
||||||
|
|
||||||
|
The JSON bundle is advisory interchange data, not a canonical Rust
|
||||||
|
``DiscoveryStore`` serialization. This verifier checks the boundary it does
|
||||||
|
claim: typed node/parent vocabulary, acyclic local references, exact artifact
|
||||||
|
hashes when finalized, explicit pending status otherwise, declared counts,
|
||||||
|
and the complete absence of hard-pruning authority.
|
||||||
|
"""
|
||||||
|
|
||||||
|
from hashlib import sha256
|
||||||
|
import json
|
||||||
|
from pathlib import Path
|
||||||
|
|
||||||
|
|
||||||
|
ROOT = Path(__file__).resolve().parent.parent
|
||||||
|
BUNDLE = Path(__file__).with_name("p28_famm_scars.json")
|
||||||
|
|
||||||
|
DISCOVERY_KINDS = {
|
||||||
|
"Observation",
|
||||||
|
"FailureSignature",
|
||||||
|
"Certificate",
|
||||||
|
"MinimizationCertificate",
|
||||||
|
"ProposedHardScar",
|
||||||
|
"AuthorizationCertificate",
|
||||||
|
"AuthorizedHardScar",
|
||||||
|
"ProposedDerivedConstraint",
|
||||||
|
"CompositionCertificate",
|
||||||
|
"AuthorizedDerivedConstraint",
|
||||||
|
"ObjectiveBoundCertificate",
|
||||||
|
"ComparisonCertificate",
|
||||||
|
"HardScar",
|
||||||
|
"SoftScar",
|
||||||
|
"Coarsening",
|
||||||
|
"RepresentativeSet",
|
||||||
|
"PolicyUpdate",
|
||||||
|
"RayInteraction",
|
||||||
|
"Bridge",
|
||||||
|
}
|
||||||
|
PARENT_ROLES = {
|
||||||
|
"ObservedFailure",
|
||||||
|
"CheckedBy",
|
||||||
|
"Authorizes",
|
||||||
|
"Supports",
|
||||||
|
"DerivedFrom",
|
||||||
|
"Refines",
|
||||||
|
"Supersedes",
|
||||||
|
"InteractsWith",
|
||||||
|
"BridgesFrom",
|
||||||
|
"BridgesTo",
|
||||||
|
}
|
||||||
|
HARD_KINDS = {"ProposedHardScar", "AuthorizationCertificate",
|
||||||
|
"AuthorizedHardScar", "HardScar"}
|
||||||
|
|
||||||
|
|
||||||
|
def digest(path):
|
||||||
|
return sha256(path.read_bytes()).hexdigest()
|
||||||
|
|
||||||
|
|
||||||
|
data = json.loads(BUNDLE.read_text(encoding="utf-8"))
|
||||||
|
assert data["schema"] == "mathpunch.p28-famm-scar-bundle.v1"
|
||||||
|
assert data["interchange_contract"]["ingested_into_discovery_store"] is False
|
||||||
|
assert data["interchange_contract"]["pruning_authority"] is False
|
||||||
|
assert data["interchange_contract"]["canonical_node_hashes"] is None
|
||||||
|
assert data["interchange_contract"]["mmr_commitment"] is None
|
||||||
|
assert data["authorized_hard_scars"] == []
|
||||||
|
assert data["authority_policy"]["authorized_hard_scars_present"] is False
|
||||||
|
|
||||||
|
scopes = {entry["scope"] for entry in data["scope_registry"]}
|
||||||
|
assert scopes
|
||||||
|
assert all(isinstance(scope, int) and 0 <= scope < 2**32 for scope in scopes)
|
||||||
|
|
||||||
|
nodes = data["nodes"]
|
||||||
|
by_id = {}
|
||||||
|
for node in nodes:
|
||||||
|
node_id = node["id"]
|
||||||
|
assert isinstance(node_id, int) and 0 <= node_id < 2**32
|
||||||
|
assert node_id not in by_id
|
||||||
|
assert node["kind"] in DISCOVERY_KINDS
|
||||||
|
assert node["kind"] not in HARD_KINDS
|
||||||
|
assert node["scope"] in scopes
|
||||||
|
assert isinstance(node["checker_version"], int)
|
||||||
|
assert 0 <= node["checker_version"] < 2**32
|
||||||
|
|
||||||
|
payload = node["payload"]
|
||||||
|
assert payload["variant"] == "Fields"
|
||||||
|
fields = payload["fields"]
|
||||||
|
assert all(
|
||||||
|
isinstance(field, list)
|
||||||
|
and len(field) == 2
|
||||||
|
and all(isinstance(value, str) for value in field)
|
||||||
|
for field in fields
|
||||||
|
)
|
||||||
|
keys = [field[0] for field in fields]
|
||||||
|
assert len(keys) == len(set(keys))
|
||||||
|
field_map = dict(fields)
|
||||||
|
assert field_map.get("pruning_authority", "false") == "false"
|
||||||
|
|
||||||
|
for parent in node["parents"]:
|
||||||
|
assert parent["role"] in PARENT_ROLES
|
||||||
|
assert parent["node"] in by_id
|
||||||
|
assert parent["node"] < node_id
|
||||||
|
by_id[node_id] = node
|
||||||
|
|
||||||
|
for node in nodes:
|
||||||
|
if node["kind"] == "FailureSignature":
|
||||||
|
assert any(
|
||||||
|
parent["role"] == "ObservedFailure"
|
||||||
|
and by_id[parent["node"]]["kind"] in {"Observation", "RayInteraction"}
|
||||||
|
for parent in node["parents"]
|
||||||
|
)
|
||||||
|
if node["kind"] == "SoftScar":
|
||||||
|
assert any(
|
||||||
|
parent["role"] == "Supports"
|
||||||
|
and by_id[parent["node"]]["kind"] == "FailureSignature"
|
||||||
|
for parent in node["parents"]
|
||||||
|
)
|
||||||
|
|
||||||
|
counts = data["counts"]
|
||||||
|
assert counts["nodes"] == len(nodes)
|
||||||
|
assert counts["certificate_nodes"] == sum(
|
||||||
|
node["kind"] == "Certificate" for node in nodes
|
||||||
|
)
|
||||||
|
assert counts["observation_nodes"] == sum(
|
||||||
|
node["kind"] == "Observation" for node in nodes
|
||||||
|
)
|
||||||
|
assert counts["failure_signature_nodes"] == sum(
|
||||||
|
node["kind"] == "FailureSignature" for node in nodes
|
||||||
|
)
|
||||||
|
assert counts["soft_scar_nodes"] == sum(
|
||||||
|
node["kind"] == "SoftScar" for node in nodes
|
||||||
|
)
|
||||||
|
assert counts["authorized_hard_scar_nodes"] == 0
|
||||||
|
assert counts["blocked_promotion_ideas"] == len(data["blocked_promotion_ideas"])
|
||||||
|
assert all(
|
||||||
|
item["current_disposition"] == "NOT_A_HARD_SCAR"
|
||||||
|
and item["pruning_authority"] is False
|
||||||
|
for item in data["blocked_promotion_ideas"]
|
||||||
|
)
|
||||||
|
|
||||||
|
finalized = 0
|
||||||
|
pending = 0
|
||||||
|
for checker in data["checker_registry"]:
|
||||||
|
artifact = ROOT / checker["artifact"]
|
||||||
|
assert artifact.is_file(), artifact
|
||||||
|
expected = checker.get("sha256")
|
||||||
|
if expected is None:
|
||||||
|
assert checker.get("pin_status", "").startswith("PENDING_")
|
||||||
|
pending += 1
|
||||||
|
else:
|
||||||
|
assert len(expected) == 64
|
||||||
|
assert digest(artifact) == expected, artifact
|
||||||
|
finalized += 1
|
||||||
|
|
||||||
|
problem = data["problem"]
|
||||||
|
if problem["release_hash_status"] == "FINAL":
|
||||||
|
assert digest(ROOT / "solution.tex") == problem["final_solution_tex_sha256"]
|
||||||
|
assert digest(ROOT / "solution.pdf") == problem["final_solution_pdf_sha256"]
|
||||||
|
else:
|
||||||
|
assert problem["release_hash_status"].startswith("PENDING_")
|
||||||
|
assert problem["final_solution_tex_sha256"] is None
|
||||||
|
assert problem["final_solution_pdf_sha256"] is None
|
||||||
|
|
||||||
|
print("PASS: FAMM scar interchange structure")
|
||||||
|
print(f"PASS: {len(nodes)} typed nodes and {len(scopes)} declared scopes")
|
||||||
|
print("PASS: zero hard-scar or pruning-authority nodes")
|
||||||
|
print(f"PASS: {finalized} finalized artifact hashes; {pending} explicit pending pins")
|
||||||
60
optional/certificates/p28_mutation_sensitivity.py
Normal file
60
optional/certificates/p28_mutation_sensitivity.py
Normal file
|
|
@ -0,0 +1,60 @@
|
||||||
|
#!/usr/bin/env python3
|
||||||
|
"""Adversarial non-vacuity replay for the two optimized certificates.
|
||||||
|
|
||||||
|
Each valid checker is run separately by ``run_checks.sh``. Here one
|
||||||
|
authoritative coefficient is changed in an isolated temporary copy of each
|
||||||
|
checker. A PASS requires both corrupted copies to fail at the intended exact
|
||||||
|
identity, demonstrating that the coefficient tests are sensitive rather than
|
||||||
|
vacuous.
|
||||||
|
"""
|
||||||
|
|
||||||
|
from pathlib import Path
|
||||||
|
import subprocess
|
||||||
|
import sys
|
||||||
|
import tempfile
|
||||||
|
|
||||||
|
|
||||||
|
HERE = Path(__file__).resolve().parent
|
||||||
|
|
||||||
|
|
||||||
|
def rejected_mutant(filename, old, new, expected_failure):
|
||||||
|
source = (HERE / filename).read_text(encoding="utf-8")
|
||||||
|
assert old in source
|
||||||
|
mutant = source.replace(old, new, 1)
|
||||||
|
assert mutant != source
|
||||||
|
|
||||||
|
with tempfile.TemporaryDirectory(prefix="p28_mutation_") as directory:
|
||||||
|
target = Path(directory) / filename
|
||||||
|
target.write_text(mutant, encoding="utf-8")
|
||||||
|
completed = subprocess.run(
|
||||||
|
[sys.executable, str(target)],
|
||||||
|
capture_output=True,
|
||||||
|
text=True,
|
||||||
|
timeout=120,
|
||||||
|
check=False,
|
||||||
|
)
|
||||||
|
|
||||||
|
combined = completed.stdout + completed.stderr
|
||||||
|
assert completed.returncode != 0, f"mutant unexpectedly passed: {filename}"
|
||||||
|
assert expected_failure in combined, (
|
||||||
|
f"mutant failed outside the intended obligation: {filename}\n{combined}"
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
rejected_mutant(
|
||||||
|
"p28_positive_cone.py",
|
||||||
|
"[209067, 62208]",
|
||||||
|
"[209068, 62208]",
|
||||||
|
"failed obligation in group: 16 transfer identities",
|
||||||
|
)
|
||||||
|
print("PASS: positive-cone coefficient mutant rejected")
|
||||||
|
|
||||||
|
rejected_mutant(
|
||||||
|
"p28_optimized_gauge.py",
|
||||||
|
"-99*u**5 + 333*u**4",
|
||||||
|
"-98*u**5 + 333*u**4",
|
||||||
|
"D*M=J0+x*J1+x^2*J2, entry (1,1)",
|
||||||
|
)
|
||||||
|
print("PASS: optimized-gauge coefficient mutant rejected")
|
||||||
|
|
||||||
|
print("PASS: adversarial mutation sensitivity")
|
||||||
634
optional/certificates/p28_optimized_gauge.py
Normal file
634
optional/certificates/p28_optimized_gauge.py
Normal file
|
|
@ -0,0 +1,634 @@
|
||||||
|
#!/usr/bin/env python3
|
||||||
|
"""Optimized exact gauge certificate for Ramanujan Challenge Problem 2.8.
|
||||||
|
|
||||||
|
The existing all-purpose standalone checker intentionally leaves rational
|
||||||
|
functions unreduced. That is maximally transparent, but the direct
|
||||||
|
sixteen-entry differential-gauge calculation creates very large temporary
|
||||||
|
denominators.
|
||||||
|
|
||||||
|
This independent checker first proves the exact decomposition
|
||||||
|
|
||||||
|
D M(u,x) = J0(u) + x J1(u) + x^2 J2(u),
|
||||||
|
D = diag(x,1,1,1),
|
||||||
|
|
||||||
|
and the additional relation
|
||||||
|
|
||||||
|
J2 = e4 * ((2u-9)/2) * b.
|
||||||
|
|
||||||
|
It then clears the common z-denominators before forming the gauge residual.
|
||||||
|
Every assertion is an equality in a sparse polynomial ring over QQ. The
|
||||||
|
implementation provides only addition, multiplication, integer powers,
|
||||||
|
formal differentiation, substitution, and coefficient extraction. It does
|
||||||
|
not call a simplifier, polynomial division, factorizer, Groebner basis,
|
||||||
|
special-function library, root finder, or numerical sampler.
|
||||||
|
"""
|
||||||
|
|
||||||
|
from fractions import Fraction as F
|
||||||
|
from time import perf_counter
|
||||||
|
|
||||||
|
|
||||||
|
START_TIME = perf_counter()
|
||||||
|
|
||||||
|
VARIABLES = ("u", "x", "n", "z", "t")
|
||||||
|
NVARS = len(VARIABLES)
|
||||||
|
INDEX = {name: position for position, name in enumerate(VARIABLES)}
|
||||||
|
ZERO_EXPONENT = (0,) * NVARS
|
||||||
|
|
||||||
|
|
||||||
|
class Poly:
|
||||||
|
"""Sparse multivariate polynomial over QQ."""
|
||||||
|
|
||||||
|
def __init__(self, terms=None):
|
||||||
|
combined = {}
|
||||||
|
for exponent, coefficient in (terms or {}).items():
|
||||||
|
exponent = tuple(exponent)
|
||||||
|
coefficient = F(coefficient)
|
||||||
|
if coefficient:
|
||||||
|
combined[exponent] = (
|
||||||
|
combined.get(exponent, F(0)) + coefficient
|
||||||
|
)
|
||||||
|
self.terms = {
|
||||||
|
exponent: coefficient
|
||||||
|
for exponent, coefficient in combined.items()
|
||||||
|
if coefficient
|
||||||
|
}
|
||||||
|
|
||||||
|
@staticmethod
|
||||||
|
def constant(value):
|
||||||
|
value = F(value)
|
||||||
|
return Poly({ZERO_EXPONENT: value}) if value else Poly()
|
||||||
|
|
||||||
|
@staticmethod
|
||||||
|
def variable(name):
|
||||||
|
exponent = [0] * NVARS
|
||||||
|
exponent[INDEX[name]] = 1
|
||||||
|
return Poly({tuple(exponent): F(1)})
|
||||||
|
|
||||||
|
def __add__(self, other):
|
||||||
|
other = as_poly(other)
|
||||||
|
terms = dict(self.terms)
|
||||||
|
for exponent, coefficient in other.terms.items():
|
||||||
|
terms[exponent] = (
|
||||||
|
terms.get(exponent, F(0)) + coefficient
|
||||||
|
)
|
||||||
|
return Poly(terms)
|
||||||
|
|
||||||
|
__radd__ = __add__
|
||||||
|
|
||||||
|
def __neg__(self):
|
||||||
|
return Poly({
|
||||||
|
exponent: -coefficient
|
||||||
|
for exponent, coefficient in self.terms.items()
|
||||||
|
})
|
||||||
|
|
||||||
|
def __sub__(self, other):
|
||||||
|
return self + (-as_poly(other))
|
||||||
|
|
||||||
|
def __rsub__(self, other):
|
||||||
|
return as_poly(other) - self
|
||||||
|
|
||||||
|
def __mul__(self, other):
|
||||||
|
other = as_poly(other)
|
||||||
|
terms = {}
|
||||||
|
for left_exp, left_coefficient in self.terms.items():
|
||||||
|
for right_exp, right_coefficient in other.terms.items():
|
||||||
|
exponent = tuple(
|
||||||
|
left_exp[position] + right_exp[position]
|
||||||
|
for position in range(NVARS)
|
||||||
|
)
|
||||||
|
terms[exponent] = (
|
||||||
|
terms.get(exponent, F(0))
|
||||||
|
+ left_coefficient * right_coefficient
|
||||||
|
)
|
||||||
|
return Poly(terms)
|
||||||
|
|
||||||
|
__rmul__ = __mul__
|
||||||
|
|
||||||
|
def __pow__(self, exponent):
|
||||||
|
if exponent < 0:
|
||||||
|
raise ValueError("polynomial powers must be nonnegative")
|
||||||
|
result = Poly.constant(1)
|
||||||
|
base = self
|
||||||
|
power = exponent
|
||||||
|
while power:
|
||||||
|
if power & 1:
|
||||||
|
result = result * base
|
||||||
|
base = base * base
|
||||||
|
power //= 2
|
||||||
|
return result
|
||||||
|
|
||||||
|
def derivative(self, name):
|
||||||
|
position = INDEX[name]
|
||||||
|
terms = {}
|
||||||
|
for exponent, coefficient in self.terms.items():
|
||||||
|
degree = exponent[position]
|
||||||
|
if degree:
|
||||||
|
new_exponent = list(exponent)
|
||||||
|
new_exponent[position] -= 1
|
||||||
|
terms[tuple(new_exponent)] = coefficient * degree
|
||||||
|
return Poly(terms)
|
||||||
|
|
||||||
|
def is_zero(self):
|
||||||
|
return not self.terms
|
||||||
|
|
||||||
|
|
||||||
|
def as_poly(value):
|
||||||
|
if isinstance(value, Poly):
|
||||||
|
return value
|
||||||
|
return Poly.constant(value)
|
||||||
|
|
||||||
|
|
||||||
|
class Rat:
|
||||||
|
"""Unreduced rational function represented by two sparse polynomials."""
|
||||||
|
|
||||||
|
def __init__(self, numerator=0, denominator=1):
|
||||||
|
self.numerator = as_poly(numerator)
|
||||||
|
self.denominator = as_poly(denominator)
|
||||||
|
if self.denominator.is_zero():
|
||||||
|
raise ZeroDivisionError("zero polynomial denominator")
|
||||||
|
|
||||||
|
def __add__(self, other):
|
||||||
|
other = as_rat(other)
|
||||||
|
return Rat(
|
||||||
|
self.numerator * other.denominator
|
||||||
|
+ other.numerator * self.denominator,
|
||||||
|
self.denominator * other.denominator,
|
||||||
|
)
|
||||||
|
|
||||||
|
__radd__ = __add__
|
||||||
|
|
||||||
|
def __neg__(self):
|
||||||
|
return Rat(-self.numerator, self.denominator)
|
||||||
|
|
||||||
|
def __sub__(self, other):
|
||||||
|
return self + (-as_rat(other))
|
||||||
|
|
||||||
|
def __rsub__(self, other):
|
||||||
|
return as_rat(other) - self
|
||||||
|
|
||||||
|
def __mul__(self, other):
|
||||||
|
other = as_rat(other)
|
||||||
|
return Rat(
|
||||||
|
self.numerator * other.numerator,
|
||||||
|
self.denominator * other.denominator,
|
||||||
|
)
|
||||||
|
|
||||||
|
__rmul__ = __mul__
|
||||||
|
|
||||||
|
def __truediv__(self, other):
|
||||||
|
other = as_rat(other)
|
||||||
|
if other.numerator.is_zero():
|
||||||
|
raise ZeroDivisionError("division by the zero rational function")
|
||||||
|
return Rat(
|
||||||
|
self.numerator * other.denominator,
|
||||||
|
self.denominator * other.numerator,
|
||||||
|
)
|
||||||
|
|
||||||
|
def __rtruediv__(self, other):
|
||||||
|
return as_rat(other) / self
|
||||||
|
|
||||||
|
def __pow__(self, exponent):
|
||||||
|
if exponent >= 0:
|
||||||
|
return Rat(
|
||||||
|
self.numerator ** exponent,
|
||||||
|
self.denominator ** exponent,
|
||||||
|
)
|
||||||
|
return Rat(
|
||||||
|
self.denominator ** (-exponent),
|
||||||
|
self.numerator ** (-exponent),
|
||||||
|
)
|
||||||
|
|
||||||
|
def derivative(self, name):
|
||||||
|
return Rat(
|
||||||
|
self.numerator.derivative(name) * self.denominator
|
||||||
|
- self.numerator * self.denominator.derivative(name),
|
||||||
|
self.denominator ** 2,
|
||||||
|
)
|
||||||
|
|
||||||
|
def is_zero(self):
|
||||||
|
return self.numerator.is_zero()
|
||||||
|
|
||||||
|
|
||||||
|
def as_rat(value):
|
||||||
|
if isinstance(value, Rat):
|
||||||
|
return value
|
||||||
|
if isinstance(value, Poly):
|
||||||
|
return Rat(value)
|
||||||
|
return Rat(F(value))
|
||||||
|
|
||||||
|
|
||||||
|
u, x, n, z, t = [
|
||||||
|
Rat(Poly.variable(name)) for name in VARIABLES
|
||||||
|
]
|
||||||
|
SYMBOLS = dict(zip(VARIABLES, (u, x, n, z, t)))
|
||||||
|
|
||||||
|
|
||||||
|
def substitute_polynomial(polynomial, replacements):
|
||||||
|
result = Rat(0)
|
||||||
|
for exponent, coefficient in polynomial.terms.items():
|
||||||
|
term = Rat(coefficient)
|
||||||
|
for position, degree in enumerate(exponent):
|
||||||
|
if degree:
|
||||||
|
name = VARIABLES[position]
|
||||||
|
term *= replacements.get(name, SYMBOLS[name]) ** degree
|
||||||
|
result += term
|
||||||
|
return result
|
||||||
|
|
||||||
|
|
||||||
|
def substitute_rational(expression, replacements):
|
||||||
|
expression = as_rat(expression)
|
||||||
|
return (
|
||||||
|
substitute_polynomial(expression.numerator, replacements)
|
||||||
|
/ substitute_polynomial(expression.denominator, replacements)
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
def coefficient(expression, name, degree):
|
||||||
|
"""Extract a coefficient when the denominator omits ``name``."""
|
||||||
|
expression = as_rat(expression)
|
||||||
|
position = INDEX[name]
|
||||||
|
assert all(
|
||||||
|
exponent[position] == 0
|
||||||
|
for exponent in expression.denominator.terms
|
||||||
|
)
|
||||||
|
terms = {}
|
||||||
|
for exponent, value in expression.numerator.terms.items():
|
||||||
|
if exponent[position] == degree:
|
||||||
|
reduced = list(exponent)
|
||||||
|
reduced[position] = 0
|
||||||
|
terms[tuple(reduced)] = value
|
||||||
|
return Rat(Poly(terms), expression.denominator)
|
||||||
|
|
||||||
|
|
||||||
|
def matrix_multiply(left, right):
|
||||||
|
return [
|
||||||
|
[
|
||||||
|
sum(
|
||||||
|
left[row][middle] * right[middle][column]
|
||||||
|
for middle in range(len(right))
|
||||||
|
)
|
||||||
|
for column in range(len(right[0]))
|
||||||
|
]
|
||||||
|
for row in range(len(left))
|
||||||
|
]
|
||||||
|
|
||||||
|
|
||||||
|
OBLIGATIONS = 0
|
||||||
|
|
||||||
|
|
||||||
|
def check_zero(label, expression):
|
||||||
|
global OBLIGATIONS
|
||||||
|
assert as_rat(expression).is_zero(), label
|
||||||
|
OBLIGATIONS += 1
|
||||||
|
|
||||||
|
|
||||||
|
def check_matrix_entries(label, matrix):
|
||||||
|
for row in range(len(matrix)):
|
||||||
|
for column in range(len(matrix[0])):
|
||||||
|
check_zero(
|
||||||
|
f"{label}, entry ({row + 1},{column + 1})",
|
||||||
|
matrix[row][column],
|
||||||
|
)
|
||||||
|
print(f"PASS: {label} ({len(matrix) * len(matrix[0])} entries)")
|
||||||
|
|
||||||
|
|
||||||
|
def matrix_subtract(left, right):
|
||||||
|
return [
|
||||||
|
[
|
||||||
|
left[row][column] - right[row][column]
|
||||||
|
for column in range(len(left[0]))
|
||||||
|
]
|
||||||
|
for row in range(len(left))
|
||||||
|
]
|
||||||
|
|
||||||
|
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
# Authoritative matrix and the exact J0+xJ1+x^2J2 decomposition.
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
r = 1 / x
|
||||||
|
w = u * (3*u - 2) * (3*u + 2)
|
||||||
|
|
||||||
|
a1 = (
|
||||||
|
r * (144*u**5 - 288*u**4 + 144*u**3)
|
||||||
|
- 99*u**5 + 333*u**4 - 229*u**3 - 114*u**2 + 40*u + 64
|
||||||
|
)
|
||||||
|
a2 = (
|
||||||
|
r * (432*u**4 - 864*u**3 + 432*u**2)
|
||||||
|
- 243*u**4 + 909*u**3 - 868*u**2 - 80*u + 272
|
||||||
|
)
|
||||||
|
a3 = (
|
||||||
|
r * (432*u**3 - 864*u**2 + 432*u)
|
||||||
|
- 153*u**3 + 648*u**2 - 860*u + 360
|
||||||
|
)
|
||||||
|
a4 = r * 144 * (u - 1)**2
|
||||||
|
|
||||||
|
b1 = (
|
||||||
|
r * (-144*u**3)
|
||||||
|
+ 9*u**4 + 63*u**3 + 158*u**2 + 168*u + 64
|
||||||
|
)
|
||||||
|
b2 = (
|
||||||
|
r * (216*u**2)
|
||||||
|
+ 36*u**3 - 189*u**2 - 316*u - 168
|
||||||
|
)
|
||||||
|
b3 = (
|
||||||
|
r * (108*u)
|
||||||
|
+ 54*u**2 - 189*u - 158
|
||||||
|
)
|
||||||
|
|
||||||
|
c1 = (
|
||||||
|
r**2 * (-288*u**3)
|
||||||
|
+ r * (54*u**4 + 378*u**3 + 948*u**2 + 1008*u + 384)
|
||||||
|
+ 18*u**5 + 45*u**4 - 251*u**3 - 1086*u**2 - 1384*u - 576
|
||||||
|
)
|
||||||
|
c2 = (
|
||||||
|
r**2 * (-432*u**2)
|
||||||
|
+ r * (153*u**4 - 657*u**3 + 1292*u**2 + 2064*u + 1072)
|
||||||
|
- 72*u**4 + 702*u**3 - 1069*u**2 - 2508*u - 1512
|
||||||
|
)
|
||||||
|
c3 = (
|
||||||
|
r**2 * (-216*u)
|
||||||
|
+ r * (180*u**3 - 891*u**2 + 1450*u + 1116)
|
||||||
|
- 108*u**3 + 864*u**2 - 1385*u - 1422
|
||||||
|
)
|
||||||
|
c4 = (
|
||||||
|
r**2 * (-4)
|
||||||
|
+ r * (6*u**2 - 33*u + F(536, 9))
|
||||||
|
- 4*u**2 + 32*u - 63
|
||||||
|
)
|
||||||
|
|
||||||
|
matrix_m = [
|
||||||
|
[a1/w, a2/w, a3/w, a4/w],
|
||||||
|
[-u**3, -3*u**2, -3*u, -1],
|
||||||
|
[
|
||||||
|
x*b1/144,
|
||||||
|
-x*b2/72,
|
||||||
|
-x*b3/36,
|
||||||
|
x*(-2*r - (2*u - 7))/2,
|
||||||
|
],
|
||||||
|
[x**2*c1/288, x**2*c2/144, x**2*c3/72, x**2*c4/4],
|
||||||
|
]
|
||||||
|
|
||||||
|
v = [u**3, 3*u**2, 3*u, 1]
|
||||||
|
alpha = 144*(u - 1)**2 / w
|
||||||
|
j0 = (
|
||||||
|
[[alpha*v[column] for column in range(4)]]
|
||||||
|
+ [[-v[column] for column in range(4)] for _ in range(3)]
|
||||||
|
)
|
||||||
|
|
||||||
|
a_finite = [
|
||||||
|
-99*u**5 + 333*u**4 - 229*u**3 - 114*u**2 + 40*u + 64,
|
||||||
|
-243*u**4 + 909*u**3 - 868*u**2 - 80*u + 272,
|
||||||
|
-153*u**3 + 648*u**2 - 860*u + 360,
|
||||||
|
0,
|
||||||
|
]
|
||||||
|
b_row = [
|
||||||
|
(u + 1)*(u + 2)*(3*u + 4)*(3*u + 8)/144,
|
||||||
|
(-36*u**3 + 189*u**2 + 316*u + 168)/72,
|
||||||
|
(-54*u**2 + 189*u + 158)/36,
|
||||||
|
(7 - 2*u)/2,
|
||||||
|
]
|
||||||
|
c_row = [
|
||||||
|
(u + 1)*(u + 2)*(3*u + 4)*(3*u + 8)/48,
|
||||||
|
(153*u**4 - 657*u**3 + 1292*u**2 + 2064*u + 1072)/144,
|
||||||
|
(180*u**3 - 891*u**2 + 1450*u + 1116)/72,
|
||||||
|
(54*u**2 - 297*u + 536)/36,
|
||||||
|
]
|
||||||
|
j1 = [
|
||||||
|
[entry/w for entry in a_finite],
|
||||||
|
[0, 0, 0, 0],
|
||||||
|
b_row,
|
||||||
|
c_row,
|
||||||
|
]
|
||||||
|
|
||||||
|
# J2 is entered independently from the finite c_i terms. The subsequent
|
||||||
|
# check against e4*beta*b is therefore not true by construction.
|
||||||
|
j2 = [
|
||||||
|
[0, 0, 0, 0],
|
||||||
|
[0, 0, 0, 0],
|
||||||
|
[0, 0, 0, 0],
|
||||||
|
[
|
||||||
|
(
|
||||||
|
18*u**5 + 45*u**4 - 251*u**3
|
||||||
|
- 1086*u**2 - 1384*u - 576
|
||||||
|
)/288,
|
||||||
|
(
|
||||||
|
-72*u**4 + 702*u**3 - 1069*u**2
|
||||||
|
- 2508*u - 1512
|
||||||
|
)/144,
|
||||||
|
(-108*u**3 + 864*u**2 - 1385*u - 1422)/72,
|
||||||
|
(-4*u**2 + 32*u - 63)/4,
|
||||||
|
],
|
||||||
|
]
|
||||||
|
|
||||||
|
beta = (2*u - 9)/2
|
||||||
|
j2_rank_one = [
|
||||||
|
[0, 0, 0, 0],
|
||||||
|
[0, 0, 0, 0],
|
||||||
|
[0, 0, 0, 0],
|
||||||
|
[beta*entry for entry in b_row],
|
||||||
|
]
|
||||||
|
check_matrix_entries(
|
||||||
|
"J2=e4*beta*b proportionality",
|
||||||
|
matrix_subtract(j2, j2_rank_one),
|
||||||
|
)
|
||||||
|
|
||||||
|
d_times_m = [
|
||||||
|
[
|
||||||
|
x*matrix_m[row][column] if row == 0
|
||||||
|
else matrix_m[row][column]
|
||||||
|
for column in range(4)
|
||||||
|
]
|
||||||
|
for row in range(4)
|
||||||
|
]
|
||||||
|
j_decomposition = [
|
||||||
|
[
|
||||||
|
j0[row][column]
|
||||||
|
+ x*j1[row][column]
|
||||||
|
+ x**2*j2[row][column]
|
||||||
|
for column in range(4)
|
||||||
|
]
|
||||||
|
for row in range(4)
|
||||||
|
]
|
||||||
|
check_matrix_entries(
|
||||||
|
"D*M=J0+x*J1+x^2*J2",
|
||||||
|
matrix_subtract(d_times_m, j_decomposition),
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
# Common-denominator clearing after x=-z/(1-z), u=2n+1.
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
substitutions = {"u": 2*n + 1}
|
||||||
|
j0_n = [
|
||||||
|
[substitute_rational(entry, substitutions) for entry in row]
|
||||||
|
for row in j0
|
||||||
|
]
|
||||||
|
j1_n = [
|
||||||
|
[substitute_rational(entry, substitutions) for entry in row]
|
||||||
|
for row in j1
|
||||||
|
]
|
||||||
|
j2_n = [
|
||||||
|
[substitute_rational(entry, substitutions) for entry in row]
|
||||||
|
for row in j2
|
||||||
|
]
|
||||||
|
|
||||||
|
e_diagonal = [1 - z, -z, -z, -z]
|
||||||
|
d_z = (1 - z)**2
|
||||||
|
g_bar = [
|
||||||
|
[
|
||||||
|
e_diagonal[row] * (
|
||||||
|
(1 - z)**2*j0_n[row][column]
|
||||||
|
- z*(1 - z)*j1_n[row][column]
|
||||||
|
+ z**2*j2_n[row][column]
|
||||||
|
)
|
||||||
|
for column in range(4)
|
||||||
|
]
|
||||||
|
for row in range(4)
|
||||||
|
]
|
||||||
|
|
||||||
|
# Bind the cleared formula directly to the authoritative matrix, rather than
|
||||||
|
# relying only on the already-checked decomposition.
|
||||||
|
matrix_nz = [
|
||||||
|
[
|
||||||
|
substitute_rational(
|
||||||
|
entry,
|
||||||
|
{"u": 2*n + 1, "x": -z/(1 - z)},
|
||||||
|
)
|
||||||
|
for entry in row
|
||||||
|
]
|
||||||
|
for row in matrix_m
|
||||||
|
]
|
||||||
|
g_direct = [[-z*entry for entry in row] for row in matrix_nz]
|
||||||
|
check_matrix_entries(
|
||||||
|
"Gbar=(1-z)^2*(-z*M) after the exact substitution",
|
||||||
|
[
|
||||||
|
[
|
||||||
|
g_bar[row][column] - d_z*g_direct[row][column]
|
||||||
|
for column in range(4)
|
||||||
|
]
|
||||||
|
for row in range(4)
|
||||||
|
],
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
def tail_operator(parameter):
|
||||||
|
return (
|
||||||
|
t*(t + 2*parameter - 1)**3
|
||||||
|
- z*(t + parameter)
|
||||||
|
*(t + parameter + F(1, 6))
|
||||||
|
*(t + parameter + F(1, 2))
|
||||||
|
*(t + parameter + F(5, 6))
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
def companion_and_cleared(parameter):
|
||||||
|
coefficients = [
|
||||||
|
coefficient(tail_operator(parameter), "t", degree)
|
||||||
|
for degree in range(5)
|
||||||
|
]
|
||||||
|
companion = [
|
||||||
|
[0, 1, 0, 0],
|
||||||
|
[0, 0, 1, 0],
|
||||||
|
[0, 0, 0, 1],
|
||||||
|
[-coefficients[column]/coefficients[4] for column in range(4)],
|
||||||
|
]
|
||||||
|
cleared = [
|
||||||
|
[0, 1 - z, 0, 0],
|
||||||
|
[0, 0, 1 - z, 0],
|
||||||
|
[0, 0, 0, 1 - z],
|
||||||
|
[-coefficients[column] for column in range(4)],
|
||||||
|
]
|
||||||
|
return companion, cleared
|
||||||
|
|
||||||
|
|
||||||
|
companion_n, c_bar_n = companion_and_cleared(n)
|
||||||
|
companion_n1, c_bar_n1 = companion_and_cleared(n + 1)
|
||||||
|
|
||||||
|
check_matrix_entries(
|
||||||
|
"Cbar_n=(1-z)*C_n",
|
||||||
|
[
|
||||||
|
[
|
||||||
|
c_bar_n[row][column]
|
||||||
|
- (1 - z)*companion_n[row][column]
|
||||||
|
for column in range(4)
|
||||||
|
]
|
||||||
|
for row in range(4)
|
||||||
|
],
|
||||||
|
)
|
||||||
|
check_matrix_entries(
|
||||||
|
"Cbar_(n+1)=(1-z)*C_(n+1)",
|
||||||
|
[
|
||||||
|
[
|
||||||
|
c_bar_n1[row][column]
|
||||||
|
- (1 - z)*companion_n1[row][column]
|
||||||
|
for column in range(4)
|
||||||
|
]
|
||||||
|
for row in range(4)
|
||||||
|
],
|
||||||
|
)
|
||||||
|
|
||||||
|
# Verify the quotient-rule conversion on every actual Gbar entry:
|
||||||
|
#
|
||||||
|
# d(1-z) theta(Gbar/d)
|
||||||
|
# = (1-z) z Gbar' + 2z Gbar, d=(1-z)^2.
|
||||||
|
quotient_rule_residual = []
|
||||||
|
for row in range(4):
|
||||||
|
residual_row = []
|
||||||
|
for column in range(4):
|
||||||
|
rational_entry = g_bar[row][column] / d_z
|
||||||
|
left = d_z*(1 - z)*z*rational_entry.derivative("z")
|
||||||
|
right = (
|
||||||
|
(1 - z)*z*g_bar[row][column].derivative("z")
|
||||||
|
+ 2*z*g_bar[row][column]
|
||||||
|
)
|
||||||
|
residual_row.append(left - right)
|
||||||
|
quotient_rule_residual.append(residual_row)
|
||||||
|
check_matrix_entries(
|
||||||
|
"entrywise quotient-rule clearing",
|
||||||
|
quotient_rule_residual,
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
# Sixteen-entry cleared polynomial gauge, checked coefficient by coefficient.
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
left_gauge = matrix_multiply(c_bar_n, g_bar)
|
||||||
|
right_gauge = matrix_multiply(g_bar, c_bar_n1)
|
||||||
|
cleared_residual = [
|
||||||
|
[
|
||||||
|
left_gauge[row][column]
|
||||||
|
- (1 - z)*z*g_bar[row][column].derivative("z")
|
||||||
|
- 2*z*g_bar[row][column]
|
||||||
|
- right_gauge[row][column]
|
||||||
|
for column in range(4)
|
||||||
|
]
|
||||||
|
for row in range(4)
|
||||||
|
]
|
||||||
|
|
||||||
|
# Gbar has z-degree at most three and Cbar has z-degree at most one.
|
||||||
|
# Therefore every cleared residual has z-degree at most four. Checking all
|
||||||
|
# five coefficients of all sixteen entries is a complete polynomial check.
|
||||||
|
for row in range(4):
|
||||||
|
for column in range(4):
|
||||||
|
for degree in range(5):
|
||||||
|
check_zero(
|
||||||
|
(
|
||||||
|
"cleared gauge coefficient "
|
||||||
|
f"entry ({row + 1},{column + 1}), z^{degree}"
|
||||||
|
),
|
||||||
|
coefficient(cleared_residual[row][column], "z", degree),
|
||||||
|
)
|
||||||
|
print(
|
||||||
|
"PASS: cleared gauge entry "
|
||||||
|
f"({row + 1},{column + 1}) coefficients z^0,...,z^4"
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
ELAPSED = perf_counter() - START_TIME
|
||||||
|
print("PASS: optimized denominator-cleared differential gauge")
|
||||||
|
print(f"PASS: {OBLIGATIONS} exact scalar obligations")
|
||||||
|
print(f"Runtime: {ELAPSED:.6f} seconds")
|
||||||
|
print("No simplifier, division algorithm, factorizer, root finder, or sampling.")
|
||||||
663
optional/certificates/p28_positive_cone.py
Normal file
663
optional/certificates/p28_positive_cone.py
Normal file
|
|
@ -0,0 +1,663 @@
|
||||||
|
#!/usr/bin/env python3
|
||||||
|
"""Dependency-free positive-cone certificate for Problem 2.8.
|
||||||
|
|
||||||
|
This verifier constructs the authoritative deformed transfer matrix exactly
|
||||||
|
at x=1/R, balances it, and conjugates it by the Pascal matrix:
|
||||||
|
|
||||||
|
T_m = P * B_m * P^(-1).
|
||||||
|
|
||||||
|
With k=m-1 and s=R-4, every entry is checked coefficientwise against an
|
||||||
|
explicit rational function N_ij(k,s)/D_ij(m,R). Every coefficient of every
|
||||||
|
N_ij and D_ij is strictly positive, proving T_m>0 for m>=1 and R>=4.
|
||||||
|
|
||||||
|
The script also checks:
|
||||||
|
|
||||||
|
* both official seed rows enter this cone after the first transfer;
|
||||||
|
* the displayed positive limiting matrix is the exact limit of T_m; and
|
||||||
|
* specialization at the official R reproduces both official integer rows.
|
||||||
|
|
||||||
|
Only ``fractions.Fraction`` and sparse coefficient dictionaries are used.
|
||||||
|
There is no polynomial division, factorization, simplifier, root finder,
|
||||||
|
eigenvalue routine, numerical approximation, or finite sampling.
|
||||||
|
"""
|
||||||
|
|
||||||
|
from fractions import Fraction as F
|
||||||
|
|
||||||
|
|
||||||
|
class Poly:
|
||||||
|
"""Sparse polynomials in (k,s), represented by exponent pairs."""
|
||||||
|
|
||||||
|
__slots__ = ("terms",)
|
||||||
|
|
||||||
|
def __init__(self, terms=None):
|
||||||
|
normalized = {}
|
||||||
|
source = terms or {}
|
||||||
|
items = source.items() if hasattr(source, "items") else source
|
||||||
|
for exponent, coefficient in items:
|
||||||
|
coefficient = F(coefficient)
|
||||||
|
if coefficient:
|
||||||
|
normalized[tuple(exponent)] = (
|
||||||
|
normalized.get(tuple(exponent), F(0)) + coefficient
|
||||||
|
)
|
||||||
|
self.terms = {
|
||||||
|
exponent: coefficient
|
||||||
|
for exponent, coefficient in normalized.items()
|
||||||
|
if coefficient
|
||||||
|
}
|
||||||
|
|
||||||
|
@staticmethod
|
||||||
|
def constant(value):
|
||||||
|
value = F(value)
|
||||||
|
return Poly({(0, 0): value}) if value else Poly()
|
||||||
|
|
||||||
|
def __add__(self, other):
|
||||||
|
other = as_poly(other)
|
||||||
|
return Poly(list(self.terms.items()) + list(other.terms.items()))
|
||||||
|
|
||||||
|
__radd__ = __add__
|
||||||
|
|
||||||
|
def __neg__(self):
|
||||||
|
return Poly({exponent: -coefficient for exponent, coefficient in self.terms.items()})
|
||||||
|
|
||||||
|
def __sub__(self, other):
|
||||||
|
return self + (-as_poly(other))
|
||||||
|
|
||||||
|
def __rsub__(self, other):
|
||||||
|
return as_poly(other) - self
|
||||||
|
|
||||||
|
def __mul__(self, other):
|
||||||
|
if isinstance(other, Rat):
|
||||||
|
return other * self
|
||||||
|
other = as_poly(other)
|
||||||
|
terms = {}
|
||||||
|
for (ak, ass), ac in self.terms.items():
|
||||||
|
for (bk, bss), bc in other.terms.items():
|
||||||
|
exponent = (ak + bk, ass + bss)
|
||||||
|
terms[exponent] = terms.get(exponent, F(0)) + ac * bc
|
||||||
|
return Poly(terms)
|
||||||
|
|
||||||
|
__rmul__ = __mul__
|
||||||
|
|
||||||
|
def __pow__(self, exponent):
|
||||||
|
if exponent < 0:
|
||||||
|
return Rat(1, self ** (-exponent))
|
||||||
|
result = Poly.constant(1)
|
||||||
|
base = self
|
||||||
|
power = exponent
|
||||||
|
while power:
|
||||||
|
if power & 1:
|
||||||
|
result = result * base
|
||||||
|
base = base * base
|
||||||
|
power //= 2
|
||||||
|
return result
|
||||||
|
|
||||||
|
def __truediv__(self, other):
|
||||||
|
return Rat(self, as_poly(other))
|
||||||
|
|
||||||
|
def __rtruediv__(self, other):
|
||||||
|
return Rat(as_poly(other), self)
|
||||||
|
|
||||||
|
def __eq__(self, other):
|
||||||
|
return self.terms == as_poly(other).terms
|
||||||
|
|
||||||
|
def all_coefficients_positive(self):
|
||||||
|
return bool(self.terms) and all(value > 0 for value in self.terms.values())
|
||||||
|
|
||||||
|
def evaluate(self, k_value, s_value):
|
||||||
|
k_value = F(k_value)
|
||||||
|
s_value = F(s_value)
|
||||||
|
return sum(
|
||||||
|
coefficient * k_value**k_degree * s_value**s_degree
|
||||||
|
for (k_degree, s_degree), coefficient in self.terms.items()
|
||||||
|
)
|
||||||
|
|
||||||
|
def leading_in_k(self):
|
||||||
|
if not self.terms:
|
||||||
|
return -1, Poly()
|
||||||
|
degree = max(exponent[0] for exponent in self.terms)
|
||||||
|
coefficient = Poly(
|
||||||
|
{
|
||||||
|
(0, s_degree): value
|
||||||
|
for (k_degree, s_degree), value in self.terms.items()
|
||||||
|
if k_degree == degree
|
||||||
|
}
|
||||||
|
)
|
||||||
|
return degree, coefficient
|
||||||
|
|
||||||
|
|
||||||
|
def as_poly(value):
|
||||||
|
if isinstance(value, Poly):
|
||||||
|
return value
|
||||||
|
if isinstance(value, Rat):
|
||||||
|
if value.denominator == Poly.constant(1):
|
||||||
|
return value.numerator
|
||||||
|
raise TypeError("cannot coerce a non-polynomial rational function to Poly")
|
||||||
|
return Poly.constant(value)
|
||||||
|
|
||||||
|
|
||||||
|
class Rat:
|
||||||
|
"""Unsimplified rational functions; equality is by cross multiplication."""
|
||||||
|
|
||||||
|
__slots__ = ("numerator", "denominator")
|
||||||
|
|
||||||
|
def __init__(self, numerator=0, denominator=1):
|
||||||
|
if isinstance(numerator, Rat):
|
||||||
|
if denominator != 1:
|
||||||
|
raise TypeError("nested rational denominator")
|
||||||
|
self.numerator = numerator.numerator
|
||||||
|
self.denominator = numerator.denominator
|
||||||
|
return
|
||||||
|
self.numerator = as_poly(numerator)
|
||||||
|
self.denominator = as_poly(denominator)
|
||||||
|
if not self.denominator.terms:
|
||||||
|
raise ZeroDivisionError("zero polynomial denominator")
|
||||||
|
|
||||||
|
def __add__(self, other):
|
||||||
|
other = as_rat(other)
|
||||||
|
if self.denominator == other.denominator:
|
||||||
|
return Rat(self.numerator + other.numerator, self.denominator)
|
||||||
|
return Rat(
|
||||||
|
self.numerator * other.denominator
|
||||||
|
+ other.numerator * self.denominator,
|
||||||
|
self.denominator * other.denominator,
|
||||||
|
)
|
||||||
|
|
||||||
|
__radd__ = __add__
|
||||||
|
|
||||||
|
def __neg__(self):
|
||||||
|
return Rat(-self.numerator, self.denominator)
|
||||||
|
|
||||||
|
def __sub__(self, other):
|
||||||
|
return self + (-as_rat(other))
|
||||||
|
|
||||||
|
def __rsub__(self, other):
|
||||||
|
return as_rat(other) - self
|
||||||
|
|
||||||
|
def __mul__(self, other):
|
||||||
|
other = as_rat(other)
|
||||||
|
return Rat(
|
||||||
|
self.numerator * other.numerator,
|
||||||
|
self.denominator * other.denominator,
|
||||||
|
)
|
||||||
|
|
||||||
|
__rmul__ = __mul__
|
||||||
|
|
||||||
|
def __truediv__(self, other):
|
||||||
|
other = as_rat(other)
|
||||||
|
return Rat(
|
||||||
|
self.numerator * other.denominator,
|
||||||
|
self.denominator * other.numerator,
|
||||||
|
)
|
||||||
|
|
||||||
|
def __rtruediv__(self, other):
|
||||||
|
return as_rat(other) / self
|
||||||
|
|
||||||
|
def __pow__(self, exponent):
|
||||||
|
if exponent < 0:
|
||||||
|
return Rat(
|
||||||
|
self.denominator ** (-exponent),
|
||||||
|
self.numerator ** (-exponent),
|
||||||
|
)
|
||||||
|
return Rat(self.numerator**exponent, self.denominator**exponent)
|
||||||
|
|
||||||
|
def __eq__(self, other):
|
||||||
|
other = as_rat(other)
|
||||||
|
return (
|
||||||
|
self.numerator * other.denominator
|
||||||
|
== other.numerator * self.denominator
|
||||||
|
)
|
||||||
|
|
||||||
|
def evaluate(self, k_value, s_value):
|
||||||
|
denominator = self.denominator.evaluate(k_value, s_value)
|
||||||
|
if not denominator:
|
||||||
|
raise ZeroDivisionError("specialized denominator vanishes")
|
||||||
|
return self.numerator.evaluate(k_value, s_value) / denominator
|
||||||
|
|
||||||
|
def limit_in_k(self):
|
||||||
|
numerator_degree, numerator_lead = self.numerator.leading_in_k()
|
||||||
|
denominator_degree, denominator_lead = self.denominator.leading_in_k()
|
||||||
|
if numerator_degree < denominator_degree:
|
||||||
|
return Rat(0)
|
||||||
|
if numerator_degree > denominator_degree:
|
||||||
|
raise AssertionError("rational function diverges as k tends to infinity")
|
||||||
|
return Rat(numerator_lead, denominator_lead)
|
||||||
|
|
||||||
|
|
||||||
|
def as_rat(value):
|
||||||
|
return value if isinstance(value, Rat) else Rat(value)
|
||||||
|
|
||||||
|
|
||||||
|
def matrix_multiply(left, right):
|
||||||
|
rows = len(left)
|
||||||
|
inner = len(right)
|
||||||
|
columns = len(right[0])
|
||||||
|
assert all(len(row) == inner for row in left)
|
||||||
|
return [
|
||||||
|
[
|
||||||
|
sum(
|
||||||
|
(as_rat(left[i][h]) * as_rat(right[h][j]) for h in range(inner)),
|
||||||
|
Rat(0),
|
||||||
|
)
|
||||||
|
for j in range(columns)
|
||||||
|
]
|
||||||
|
for i in range(rows)
|
||||||
|
]
|
||||||
|
|
||||||
|
|
||||||
|
def row_matrix_multiply(row, matrix):
|
||||||
|
return matrix_multiply([row], matrix)[0]
|
||||||
|
|
||||||
|
|
||||||
|
def polynomial_from_coefficient_rows(rows):
|
||||||
|
"""Rows are indexed by k-degree; entries by s-degree."""
|
||||||
|
return Poly(
|
||||||
|
{
|
||||||
|
(k_degree, s_degree): coefficient
|
||||||
|
for k_degree, row in enumerate(rows)
|
||||||
|
for s_degree, coefficient in enumerate(row)
|
||||||
|
if coefficient
|
||||||
|
}
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
k = Poly({(1, 0): 1})
|
||||||
|
s = Poly({(0, 1): 1})
|
||||||
|
m = k + 1
|
||||||
|
R = s + 4
|
||||||
|
|
||||||
|
|
||||||
|
def authoritative_matrix(u, parameter_R):
|
||||||
|
"""The exact Problem 2.8 transfer at x=1/R."""
|
||||||
|
omega = u * (3 * u - 2) * (3 * u + 2)
|
||||||
|
|
||||||
|
a1 = parameter_R * (144*u**5 - 288*u**4 + 144*u**3) + (
|
||||||
|
-99*u**5 + 333*u**4 - 229*u**3 - 114*u**2 + 40*u + 64
|
||||||
|
)
|
||||||
|
a2 = parameter_R * (432*u**4 - 864*u**3 + 432*u**2) + (
|
||||||
|
-243*u**4 + 909*u**3 - 868*u**2 - 80*u + 272
|
||||||
|
)
|
||||||
|
a3 = parameter_R * (432*u**3 - 864*u**2 + 432*u) + (
|
||||||
|
-153*u**3 + 648*u**2 - 860*u + 360
|
||||||
|
)
|
||||||
|
a4 = parameter_R * 144 * (u - 1)**2
|
||||||
|
|
||||||
|
b1 = parameter_R * (-144*u**3) + (
|
||||||
|
9*u**4 + 63*u**3 + 158*u**2 + 168*u + 64
|
||||||
|
)
|
||||||
|
b2 = parameter_R * (216*u**2) + (
|
||||||
|
36*u**3 - 189*u**2 - 316*u - 168
|
||||||
|
)
|
||||||
|
b3 = parameter_R * (108*u) + (54*u**2 - 189*u - 158)
|
||||||
|
|
||||||
|
c1 = (
|
||||||
|
parameter_R**2 * (-288*u**3)
|
||||||
|
+ parameter_R * (54*u**4 + 378*u**3 + 948*u**2 + 1008*u + 384)
|
||||||
|
+ (18*u**5 + 45*u**4 - 251*u**3 - 1086*u**2 - 1384*u - 576)
|
||||||
|
)
|
||||||
|
c2 = (
|
||||||
|
parameter_R**2 * (-432*u**2)
|
||||||
|
+ parameter_R * (153*u**4 - 657*u**3 + 1292*u**2 + 2064*u + 1072)
|
||||||
|
+ (-72*u**4 + 702*u**3 - 1069*u**2 - 2508*u - 1512)
|
||||||
|
)
|
||||||
|
c3 = (
|
||||||
|
parameter_R**2 * (-216*u)
|
||||||
|
+ parameter_R * (180*u**3 - 891*u**2 + 1450*u + 1116)
|
||||||
|
+ (-108*u**3 + 864*u**2 - 1385*u - 1422)
|
||||||
|
)
|
||||||
|
c4 = (
|
||||||
|
parameter_R**2 * (-4)
|
||||||
|
+ parameter_R * (6*u**2 - 33*u + F(536, 9))
|
||||||
|
+ (-4*u**2 + 32*u - 63)
|
||||||
|
)
|
||||||
|
|
||||||
|
return [
|
||||||
|
[a1/omega, a2/omega, a3/omega, a4/omega],
|
||||||
|
[-u**3, -3*u**2, -3*u, -1],
|
||||||
|
[
|
||||||
|
b1/(144*parameter_R),
|
||||||
|
-b2/(72*parameter_R),
|
||||||
|
-b3/(36*parameter_R),
|
||||||
|
(-2*parameter_R-(2*u-7))/(2*parameter_R),
|
||||||
|
],
|
||||||
|
[
|
||||||
|
c1/(288*parameter_R**2),
|
||||||
|
c2/(144*parameter_R**2),
|
||||||
|
c3/(72*parameter_R**2),
|
||||||
|
c4/(4*parameter_R**2),
|
||||||
|
],
|
||||||
|
]
|
||||||
|
|
||||||
|
|
||||||
|
PASCAL = [
|
||||||
|
[1, 0, 0, 0],
|
||||||
|
[1, 1, 0, 0],
|
||||||
|
[1, 2, 1, 0],
|
||||||
|
[1, 3, 3, 1],
|
||||||
|
]
|
||||||
|
PASCAL_INVERSE = [
|
||||||
|
[1, 0, 0, 0],
|
||||||
|
[-1, 1, 0, 0],
|
||||||
|
[1, -2, 1, 0],
|
||||||
|
[-1, 3, -3, 1],
|
||||||
|
]
|
||||||
|
|
||||||
|
|
||||||
|
OBLIGATIONS = {}
|
||||||
|
|
||||||
|
|
||||||
|
def obligation(group, condition):
|
||||||
|
if not condition:
|
||||||
|
raise AssertionError("failed obligation in group: " + group)
|
||||||
|
OBLIGATIONS[group] = OBLIGATIONS.get(group, 0) + 1
|
||||||
|
|
||||||
|
|
||||||
|
obligation(
|
||||||
|
"Pascal inverse",
|
||||||
|
matrix_multiply(PASCAL, PASCAL_INVERSE)
|
||||||
|
== [[Rat(int(i == j)) for j in range(4)] for i in range(4)],
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
# Build B_m and T_m=P*B_m*P^(-1) exactly with m=k+1 and R=s+4.
|
||||||
|
M = authoritative_matrix(2*m + 3, R)
|
||||||
|
balanced = [
|
||||||
|
[
|
||||||
|
as_rat(M[i][j]) * (m+1)**j / m**i / (m+1)**2
|
||||||
|
for j in range(4)
|
||||||
|
]
|
||||||
|
for i in range(4)
|
||||||
|
]
|
||||||
|
T = matrix_multiply(matrix_multiply(PASCAL, balanced), PASCAL_INVERSE)
|
||||||
|
|
||||||
|
|
||||||
|
# Explicit coefficient arrays for N_ij(k,s). The outer list is indexed by
|
||||||
|
# k-degree and each inner list by s-degree.
|
||||||
|
NUMERATOR_COEFFICIENTS = [
|
||||||
|
[
|
||||||
|
[
|
||||||
|
[209067, 62208],
|
||||||
|
[409482, 124416],
|
||||||
|
[318165, 98496],
|
||||||
|
[122806, 38592],
|
||||||
|
[23580, 7488],
|
||||||
|
[1800, 576],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[216214, 62208],
|
||||||
|
[351120, 103680],
|
||||||
|
[210784, 63936],
|
||||||
|
[55584, 17280],
|
||||||
|
[5472, 1728],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[76079, 20736],
|
||||||
|
[98882, 27648],
|
||||||
|
[41796, 12096],
|
||||||
|
[5688, 1728],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[18432, 4608],
|
||||||
|
[27648, 6912],
|
||||||
|
[13824, 3456],
|
||||||
|
[2304, 576],
|
||||||
|
],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[
|
||||||
|
[44808, 15552],
|
||||||
|
[93312, 31104],
|
||||||
|
[62208, 20736],
|
||||||
|
[17280, 5760],
|
||||||
|
[1728, 576],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[186379, 62208],
|
||||||
|
[511210, 165888],
|
||||||
|
[519853, 167616],
|
||||||
|
[250678, 81216],
|
||||||
|
[58140, 19008],
|
||||||
|
[5256, 1728],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[66134, 20736],
|
||||||
|
[159568, 48384],
|
||||||
|
[131792, 39744],
|
||||||
|
[45216, 13824],
|
||||||
|
[5472, 1728],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[16222, 4608],
|
||||||
|
[42291, 11520],
|
||||||
|
[39050, 10368],
|
||||||
|
[15444, 4032],
|
||||||
|
[2232, 576],
|
||||||
|
],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[
|
||||||
|
[12995117, 8841456, 1492992],
|
||||||
|
[58685630, 37561608, 5971968],
|
||||||
|
[103594644, 64078200, 9828864],
|
||||||
|
[94855680, 57551496, 8640000],
|
||||||
|
[49440456, 29668248, 4396032],
|
||||||
|
[14835888, 8843664, 1299456],
|
||||||
|
[2392416, 1419552, 207360],
|
||||||
|
[160704, 95040, 13824],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[39423757, 27038952, 4478976],
|
||||||
|
[166410214, 105688080, 16422912],
|
||||||
|
[262665540, 160189416, 24012288],
|
||||||
|
[203963976, 121854816, 17915904],
|
||||||
|
[83704320, 49549824, 7216128],
|
||||||
|
[17449344, 10295424, 1492992],
|
||||||
|
[1461888, 860544, 124416],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[6744221, 4650768, 746496],
|
||||||
|
[26619818, 16612236, 2488320],
|
||||||
|
[37076724, 21985452, 3172608],
|
||||||
|
[23503608, 13602888, 1928448],
|
||||||
|
[6902496, 3967056, 559872],
|
||||||
|
[756864, 438048, 62208],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[87786, 60468, 9216],
|
||||||
|
[369593, 226474, 32256],
|
||||||
|
[559242, 320520, 43776],
|
||||||
|
[393892, 216608, 28800],
|
||||||
|
[131832, 70560, 9216],
|
||||||
|
[16992, 8928, 1152],
|
||||||
|
],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[
|
||||||
|
[33051981, 55702072, 23898528, 2985984],
|
||||||
|
[327240514, 376865532, 134112240, 14929920],
|
||||||
|
[930970540, 937602272, 303903216, 31601664],
|
||||||
|
[1279073232, 1205376648, 370469520, 36937728],
|
||||||
|
[994303368, 902431272, 268543536, 26072064],
|
||||||
|
[461588688, 409453104, 119369664, 11390976],
|
||||||
|
[127105056, 111089760, 31948032, 3013632],
|
||||||
|
[19185984, 16597440, 4727808, 442368],
|
||||||
|
[1223424, 1050624, 297216, 27648],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[124354341, 177927470, 72724752, 8957952],
|
||||||
|
[1045995002, 1120727784, 383156784, 41803776],
|
||||||
|
[2641611740, 2536092136, 794391552, 80870400],
|
||||||
|
[3164847768, 2875298832, 858173328, 83856384],
|
||||||
|
[2060023392, 1815713424, 527093136, 50264064],
|
||||||
|
[748445184, 648617760, 185300064, 17418240],
|
||||||
|
[142860672, 122627520, 34706880, 3234816],
|
||||||
|
[11197440, 9548928, 2685312, 248832],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[26276833, 32297441, 12409344, 1492992],
|
||||||
|
[188851718, 188046502, 61107192, 6469632],
|
||||||
|
[420585148, 383136068, 114774408, 11321856],
|
||||||
|
[431847432, 375502536, 107664480, 10202112],
|
||||||
|
[225990144, 191691072, 53691264, 4976640],
|
||||||
|
[58320000, 48926592, 13561344, 1244160],
|
||||||
|
[5847552, 4904064, 1358208, 124416],
|
||||||
|
],
|
||||||
|
[
|
||||||
|
[3759202, 4035454, 1433736, 165888],
|
||||||
|
[25198317, 23609115, 7287084, 746496],
|
||||||
|
[57385334, 50066438, 14346252, 1368576],
|
||||||
|
[62533980, 52200252, 14310108, 1306368],
|
||||||
|
[35688168, 28926216, 7710120, 684288],
|
||||||
|
[10310976, 8188128, 2142288, 186624],
|
||||||
|
[1192320, 933120, 241056, 20736],
|
||||||
|
],
|
||||||
|
],
|
||||||
|
]
|
||||||
|
|
||||||
|
N = [
|
||||||
|
[polynomial_from_coefficient_rows(NUMERATOR_COEFFICIENTS[i][j]) for j in range(4)]
|
||||||
|
for i in range(4)
|
||||||
|
]
|
||||||
|
|
||||||
|
g = (2*m+3) * (6*m+7) * (6*m+11)
|
||||||
|
D = [
|
||||||
|
[(m+1)**2*g, (m+1)*g, g, g],
|
||||||
|
[m*g, m*(m+1)*g, m*g, m*g],
|
||||||
|
[
|
||||||
|
24*m**2*(m+1)**2*g*R,
|
||||||
|
72*m**2*(m+1)*g*R,
|
||||||
|
36*m**2*g*R,
|
||||||
|
2*m**2*g*R,
|
||||||
|
],
|
||||||
|
[
|
||||||
|
48*m**3*(m+1)**2*g*R**2,
|
||||||
|
144*m**3*(m+1)*g*R**2,
|
||||||
|
72*m**3*g*R**2,
|
||||||
|
36*m**3*g*R**2,
|
||||||
|
],
|
||||||
|
]
|
||||||
|
|
||||||
|
for i in range(4):
|
||||||
|
for j in range(4):
|
||||||
|
obligation("16 transfer identities", T[i][j] == Rat(N[i][j], D[i][j]))
|
||||||
|
obligation("16 positive numerators", N[i][j].all_coefficients_positive())
|
||||||
|
obligation("16 positive denominators", D[i][j].all_coefficients_positive())
|
||||||
|
|
||||||
|
|
||||||
|
# Exact positive limiting matrix P*S*P^(-1).
|
||||||
|
LIMIT = [
|
||||||
|
[8*R-7, 4*(6*R-5), 24*R-17, 8*R],
|
||||||
|
[8*(R-1), 24*R-23, 4*(6*R-5), 8*R-1],
|
||||||
|
[
|
||||||
|
(R-1)*(8*R-1)/R,
|
||||||
|
2*(R-1)*(12*R-1)/R,
|
||||||
|
24*R-23,
|
||||||
|
2*(4*R**2-R-1)/R,
|
||||||
|
],
|
||||||
|
[
|
||||||
|
2*(R-1)*(4*R**2-R-1)/R**2,
|
||||||
|
(R-1)*(24*R**2-5*R-4)/R**2,
|
||||||
|
2*(R-1)*(12*R-1)/R,
|
||||||
|
(8*R**3-3*R**2-4)/R**2,
|
||||||
|
],
|
||||||
|
]
|
||||||
|
|
||||||
|
for i in range(4):
|
||||||
|
for j in range(4):
|
||||||
|
actual_limit = T[i][j].limit_in_k()
|
||||||
|
expected_limit = as_rat(LIMIT[i][j])
|
||||||
|
obligation("16 limiting-matrix identities", actual_limit == expected_limit)
|
||||||
|
obligation(
|
||||||
|
"16 positive limiting entries",
|
||||||
|
expected_limit.numerator.all_coefficients_positive()
|
||||||
|
and expected_limit.denominator.all_coefficients_positive(),
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
# Official seed rows and their first positive-cone states.
|
||||||
|
CHUD_A = 13_591_409
|
||||||
|
CHUD_B = 545_140_134
|
||||||
|
CHUD_S = 426_880
|
||||||
|
|
||||||
|
compact_denominator = [
|
||||||
|
18*R + F(159, 4),
|
||||||
|
54*R + F(131, 2),
|
||||||
|
54*R + 27,
|
||||||
|
18*R,
|
||||||
|
]
|
||||||
|
h0 = [CHUD_A+CHUD_B, CHUD_B, 0, 0]
|
||||||
|
seed_a1 = [CHUD_S*entry for entry in compact_denominator]
|
||||||
|
seed_a0 = [
|
||||||
|
CHUD_A*compact_denominator[index] - F(5, 4)*h0[index]
|
||||||
|
for index in range(4)
|
||||||
|
]
|
||||||
|
|
||||||
|
M0 = authoritative_matrix(Poly.constant(3), R)
|
||||||
|
cone_a1 = row_matrix_multiply(row_matrix_multiply(seed_a1, M0), PASCAL_INVERSE)
|
||||||
|
cone_a0 = row_matrix_multiply(row_matrix_multiply(seed_a0, M0), PASCAL_INVERSE)
|
||||||
|
|
||||||
|
EXPECTED_CONE_A1 = [
|
||||||
|
Rat(320160*polynomial_from_coefficient_rows([[451657, 259168, 36864]]), 77),
|
||||||
|
Rat(213440*polynomial_from_coefficient_rows([[1045771, 591288, 82944]]), 77),
|
||||||
|
Rat(3841920*polynomial_from_coefficient_rows([[30075, 16706, 2304]]), 77),
|
||||||
|
Rat(7683840*polynomial_from_coefficient_rows([[2612, 1421, 192]]), 77),
|
||||||
|
]
|
||||||
|
EXPECTED_CONE_A0 = [
|
||||||
|
Rat(polynomial_from_coefficient_rows([[13563858344917, 18828949838688, 4509303312384]]), 924),
|
||||||
|
Rat(2*polynomial_from_coefficient_rows([[2606908232573, 3613607517834, 845494371072]]), 231),
|
||||||
|
Rat(polynomial_from_coefficient_rows([[3584820267815, 4955797147464, 1127325828096]]), 308),
|
||||||
|
Rat(3*polynomial_from_coefficient_rows([[103400761441, 142363659388, 31314606336]]), 154),
|
||||||
|
]
|
||||||
|
|
||||||
|
for actual, expected in zip(cone_a1, EXPECTED_CONE_A1):
|
||||||
|
obligation("8 seed-cone identities", actual == expected)
|
||||||
|
obligation(
|
||||||
|
"8 positive seed coordinates",
|
||||||
|
expected.numerator.all_coefficients_positive()
|
||||||
|
and expected.denominator.all_coefficients_positive(),
|
||||||
|
)
|
||||||
|
for actual, expected in zip(cone_a0, EXPECTED_CONE_A0):
|
||||||
|
obligation("8 seed-cone identities", actual == expected)
|
||||||
|
obligation(
|
||||||
|
"8 positive seed coordinates",
|
||||||
|
expected.numerator.all_coefficients_positive()
|
||||||
|
and expected.denominator.all_coefficients_positive(),
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
R_OFFICIAL = 151_931_373_056_001
|
||||||
|
S_OFFICIAL = R_OFFICIAL - 4
|
||||||
|
OFFICIAL_A0 = [
|
||||||
|
37169305760442252761441,
|
||||||
|
111507917281327441564208,
|
||||||
|
111507917281327599720129,
|
||||||
|
37169305760442410917362,
|
||||||
|
]
|
||||||
|
OFFICIAL_A1 = [
|
||||||
|
1167416361542639692320,
|
||||||
|
3502249084627896132160,
|
||||||
|
3502249084627879697280,
|
||||||
|
1167416361542622723840,
|
||||||
|
]
|
||||||
|
|
||||||
|
obligation(
|
||||||
|
"official coefficient relation",
|
||||||
|
9*236_337_691_420_383 == 14*R_OFFICIAL - 567,
|
||||||
|
)
|
||||||
|
obligation(
|
||||||
|
"2 official seed specializations",
|
||||||
|
[as_rat(entry).evaluate(0, S_OFFICIAL) for entry in seed_a0] == OFFICIAL_A0,
|
||||||
|
)
|
||||||
|
obligation(
|
||||||
|
"2 official seed specializations",
|
||||||
|
[as_rat(entry).evaluate(0, S_OFFICIAL) for entry in seed_a1] == OFFICIAL_A1,
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
total = sum(OBLIGATIONS.values())
|
||||||
|
print("PASS: exact positive-cone certificate")
|
||||||
|
for group, count in OBLIGATIONS.items():
|
||||||
|
print(f"PASS: {group}: {count}")
|
||||||
|
print(f"PASS: {total} exact obligations")
|
||||||
|
print("T_m=P*B_m*P^(-1) is entrywise positive for every m>=1 and R>=4")
|
||||||
|
print("Both official seed rows enter the same positive cone after one transfer")
|
||||||
|
print("No sampling, factorizer, simplifier, root finder, or eigenvalue routine was used")
|
||||||
1246
optional/certificates/solution_pre_positive_cone.tex
Normal file
1246
optional/certificates/solution_pre_positive_cone.tex
Normal file
File diff suppressed because it is too large
Load diff
BIN
optional/ramanujan_challenge_problem_2_8_optimized.zip
Normal file
BIN
optional/ramanujan_challenge_problem_2_8_optimized.zip
Normal file
Binary file not shown.
203
optional/ramanujan_problem_2_8_FAMM_SCARS.md
Normal file
203
optional/ramanujan_problem_2_8_FAMM_SCARS.md
Normal file
|
|
@ -0,0 +1,203 @@
|
||||||
|
# FAMM scars for Ramanujan Challenge Problem 2.8
|
||||||
|
|
||||||
|
## Status
|
||||||
|
|
||||||
|
This file and `certificates/p28_famm_scars.json` are advisory discovery
|
||||||
|
artifacts. They do not alter the proof, authorize pruning, or assert membership
|
||||||
|
in a canonical `DiscoveryStore`.
|
||||||
|
|
||||||
|
The formula-optimization rebuild is finalized. SHA-256 pins for the rank/ODE,
|
||||||
|
convergence, standalone-equation, denominator-cleared-gauge, positive-cone,
|
||||||
|
FAMM-interchange, and package-runner checkers are recorded in the JSON, along
|
||||||
|
with the final `solution.tex` and `solution.pdf` hashes. The older solution
|
||||||
|
hashes are retained solely as provenance for baseline commit `492c8ab`.
|
||||||
|
|
||||||
|
The bundle records defects found during the adversarial proof loop so later
|
||||||
|
searches can prioritize equation-level checks without mistaking past failures
|
||||||
|
for universal impossibility results.
|
||||||
|
|
||||||
|
The governing rule is:
|
||||||
|
|
||||||
|
> An observation, failure signature, SoftScar, or blocked promotion idea may
|
||||||
|
> change route priority. It may not remove a proof candidate.
|
||||||
|
|
||||||
|
The JSON therefore contains no `AuthorizedHardScar`.
|
||||||
|
|
||||||
|
## Authoritative FAMM sources
|
||||||
|
|
||||||
|
The schema and authority policy were read from
|
||||||
|
`allaunthefox/MathPunch-FiniteState` at commit
|
||||||
|
`9df0f48576aefce91eb1fc13ff876bec1007162d`:
|
||||||
|
|
||||||
|
| File | Relevant rule |
|
||||||
|
|---|---|
|
||||||
|
| `docs/specs/FAMM_REFINED.md` | Exact and advisory memory are separate; only exact/formal, replayed, in-scope, instance-matched, version-matched scars may hard-apply. |
|
||||||
|
| `docs/specs/FAMM_TOPOLOGY_ESCALATION_V1.md` | Machine layout and physical observations never change mathematical authority; advisory or unreplayed scars never hard-prune. |
|
||||||
|
| `src/discovery/node.rs` | Defines `Observation`, `FailureSignature`, `Certificate`, `SoftScar`, `ProposedHardScar`, `AuthorizationCertificate`, and `AuthorizedHardScar`, along with typed parent roles. |
|
||||||
|
| `src/discovery/authorization.rs` | The implemented hard-scar gate requires a typed Boolean linear formula, complete failed assignment, deletion-minimized cube, exact linear-constraint certificate, `linear-cube-interval` authorization, and replay/reauthorization. |
|
||||||
|
| `src/discovery/canonical.rs` | Canonical bytes sort parents and field payloads and bind kind, payload, parents, scope, and checker version under a domain-separated hash. |
|
||||||
|
|
||||||
|
The Problem 2.8 failures are polynomial, analytic, asymptotic, and
|
||||||
|
proof-engineering failures. They are not instances of the current Boolean
|
||||||
|
linear `TypedFormula`/`CubeRegion` authorization language. Consequently, no
|
||||||
|
entry in this package is promoted to `AuthorizedHardScar`, even when an exact
|
||||||
|
standalone checker supports the underlying equation.
|
||||||
|
|
||||||
|
## JSON schema choices
|
||||||
|
|
||||||
|
`p28_famm_scars.json` uses the new interchange identifier
|
||||||
|
`mathpunch.p28-famm-scar-bundle.v1`.
|
||||||
|
|
||||||
|
It mirrors the Rust discovery vocabulary without pretending to be a Rust
|
||||||
|
serialization:
|
||||||
|
|
||||||
|
- `kind` uses exact `DiscoveryKind` names.
|
||||||
|
- `parents` use exact `ParentRole` names and bundle-local integer node IDs.
|
||||||
|
- A SoftScar's advisory relationship to its FailureSignature uses
|
||||||
|
`ParentRole::Supports`, never `DerivedFrom`; `CheckedBy` separately links a
|
||||||
|
replay certificate when one exists.
|
||||||
|
- `scope` is a bundle-local unsigned integer resolved through
|
||||||
|
`scope_registry`.
|
||||||
|
- `payload` uses the `Fields` variant as ordered key/value pairs; a future
|
||||||
|
importer must sort them as `canonical.rs` requires.
|
||||||
|
- `checker_version` is an unsigned schema/checker generation.
|
||||||
|
- replay commands, runtimes, artifact paths, and SHA-256 hashes are declared
|
||||||
|
separately in `checker_registry`.
|
||||||
|
|
||||||
|
The bundle intentionally sets these fields to non-authoritative values:
|
||||||
|
|
||||||
|
```text
|
||||||
|
ingested_into_discovery_store = false
|
||||||
|
canonical_node_hashes = null
|
||||||
|
mmr_commitment = null
|
||||||
|
pruning_authority = false
|
||||||
|
```
|
||||||
|
|
||||||
|
Local node and scope IDs must be remapped by an importer. Canonical discovery
|
||||||
|
hashes may be assigned only after the nodes are constructed through the
|
||||||
|
repository's canonical Rust path.
|
||||||
|
|
||||||
|
## Scar catalogue
|
||||||
|
|
||||||
|
Every row below corresponds to an
|
||||||
|
`Observation -> FailureSignature -> SoftScar` chain in the JSON.
|
||||||
|
|
||||||
|
| SoftScar | Exact scope | Failure signature | Assumption avoided | Replay support |
|
||||||
|
|---|---|---|---|---|
|
||||||
|
| `12` | Pinned transfer and package | An under-defined or transcription-divergent matrix is used by later identities | Omitted coefficients are harmless | Dependency-free equation replay |
|
||||||
|
| `22` | Tail contiguity for the displayed \(M_N(x)\) and shifted \({}_4F_3\) jet | CAS Ore division is cited without four cleared residual identities | A zero-remainder routine is itself an inspectable certificate | Dependency-free equation replay |
|
||||||
|
| `32` | Terminating denominator, \(n\ge1\), \(0\le k\le n\) | Fourth-order uniqueness is inferred from normalization at \(z=0\) | One datum determines a fourth-order analytic solution | Base/generic/top coefficient replay |
|
||||||
|
| `42` | Official matrix-to-scalar bridge | A scalar recurrence is accepted without an exact intertwiner | Sample agreement identifies the official module | Sixteen gauge entries and contraction replay |
|
||||||
|
| `52` | Official \(R,x_0\), \(|x|=1/4\), \(m\ge1\) | An inequality is inverted without reversing its direction | Integer powers preserve order for negative exponents | Exact rational convergence checker |
|
||||||
|
| `62` | Official seed rows, four columns, and positive cone | A named transport theorem hides the hypotheses or denominator conclusion | Spectral machinery is necessary for all-column transport | Exact Pascal-conjugated positive transfer and elementary min/max contraction |
|
||||||
|
| `72` | Historical characteristic quartic and displayed eigenvector | Native factor/GCD/root decisions are used as portable exact proof | CAS decisions carry proof authority by default | Exact coefficient homotopy and polynomial eigenvector replay for the retained legacy route |
|
||||||
|
| `82` | Official four columns in the proved positive cone | A quotient is formed before denominator positivity | Formal ratio notation guarantees a nonzero denominator | Exact cone entry and strictly positive transfer entries |
|
||||||
|
| `92` | Mandatory/optional checker split | A stored PASS transcript substitutes for live replay | A receipt proves the current bytes were executed | Mandatory standard-library runner |
|
||||||
|
| `102` | Release metadata | The reciprocal limit is labelled as the official orientation | Equivalent formulas have interchangeable submission labels | Boxed manuscript theorem and official-scope review |
|
||||||
|
| `112` | Wolfram source serialization | A line break terminates an assignment before leading-plus continuation terms | Printed multiline equality equals parsed equality | Parser round-trip is required; current Wolfram run is optional |
|
||||||
|
| `122` | Pinned rational gauge after denominator clearing | Raw rational expansion produces avoidable expression swell or resource failure | Raw rational normal form is required, or capacity failure falsifies the identity | 176 cleared polynomial obligations |
|
||||||
|
| `132` | Official Pascal-conjugated positive cone | Spectral machinery is introduced before testing an elementary positive transport | Eigenvalues and a stable graph are necessary for the official columns | 100 exact positive-cone obligations |
|
||||||
|
| `142` | Advisory FAMM interchange bundle | A SoftScar is linked as an exact derivation rather than advisory support | Advisory diagnosis has exact derivational authority | Structural validator requiring `Supports` and zero hard authority |
|
||||||
|
|
||||||
|
These scars are deliberately narrow:
|
||||||
|
|
||||||
|
- They apply only to the pinned Problem 2.8 objects and proof routes.
|
||||||
|
- They do not assert that Ore methods, scalar recurrences, asymptotic theorems,
|
||||||
|
CAS tools, or reciprocal formulations are invalid in general.
|
||||||
|
- They do not rule out a repaired candidate satisfying the missing equation or
|
||||||
|
hypothesis.
|
||||||
|
|
||||||
|
## Exact replay links
|
||||||
|
|
||||||
|
The advisory scars point to these replayable local artifacts:
|
||||||
|
|
||||||
|
```sh
|
||||||
|
python3 certificates/p28_rank_ode_bound_verifier.py
|
||||||
|
python3 certificates/p28_convergence_constants.py
|
||||||
|
python3 certificates/p28_standalone_equations.py
|
||||||
|
python3 certificates/p28_dominant_product_algebra.py
|
||||||
|
python3 certificates/p28_optimized_gauge.py
|
||||||
|
python3 certificates/p28_positive_cone.py
|
||||||
|
python3 certificates/p28_famm_scars_validator.py
|
||||||
|
```
|
||||||
|
|
||||||
|
The complete mandatory path is:
|
||||||
|
|
||||||
|
```sh
|
||||||
|
bash run_checks.sh
|
||||||
|
```
|
||||||
|
|
||||||
|
Sage and Wolfram files remain optional independent cross-checks. Their absence
|
||||||
|
does not convert a stored transcript into proof evidence.
|
||||||
|
|
||||||
|
Finalized artifact hashes and checker identifiers are in the JSON. Changing a
|
||||||
|
finalized checker, manuscript source, or PDF requires a new replay and a new
|
||||||
|
bundle version.
|
||||||
|
|
||||||
|
## Formula-optimization loop
|
||||||
|
|
||||||
|
Two optimization results change route priority without changing mathematical
|
||||||
|
authority:
|
||||||
|
|
||||||
|
1. The rational gauge is replayed after the diagonal scaling
|
||||||
|
\(D=\operatorname{diag}(x,1,1,1)\) and common clearing by \((1-z)^2\).
|
||||||
|
The resulting companion matrices have bounded polynomial degree, and the
|
||||||
|
checker expands the claim into 176 scalar polynomial obligations. A timeout,
|
||||||
|
capacity rejection, or expression explosion in the unreduced route is a
|
||||||
|
proof-engineering failure, not evidence that the rational identity is false.
|
||||||
|
2. The current all-column proof conjugates the balanced transfer by the exact
|
||||||
|
Pascal matrix, places both official seed rows in a strictly positive cone,
|
||||||
|
and uses the elementary min/max contraction of positive weighted averages.
|
||||||
|
The earlier spectral and stable-graph argument remains an audited historical
|
||||||
|
route, but it is no longer an active prerequisite for the four-column
|
||||||
|
transport or denominator nonvanishing.
|
||||||
|
|
||||||
|
The interchange validator records the corresponding route scars and checks
|
||||||
|
that each SoftScar is advisory: it must have a `Supports` edge from a
|
||||||
|
FailureSignature, may have a separate `CheckedBy` certificate, has no hard
|
||||||
|
authority, and cannot prune.
|
||||||
|
|
||||||
|
## Why no hard scars were emitted
|
||||||
|
|
||||||
|
Three exact-certificate-linked promotion ideas are recorded under
|
||||||
|
`blocked_promotion_ideas`:
|
||||||
|
|
||||||
|
1. nonzero cleared Ore residuals;
|
||||||
|
2. reversed negative-exponent inequalities;
|
||||||
|
3. nonzero matrix-to-scalar intertwiner residuals.
|
||||||
|
|
||||||
|
They are not `ProposedHardScar` or `AuthorizedHardScar` nodes. The present
|
||||||
|
authorizer cannot express their formula domain, region semantics, or
|
||||||
|
minimization rule. Promoting any of them requires all of:
|
||||||
|
|
||||||
|
1. a versioned typed proof-domain formula;
|
||||||
|
2. canonical coefficient or inequality encoding;
|
||||||
|
3. exact applicability-scope semantics;
|
||||||
|
4. a replayable witness;
|
||||||
|
5. a sound minimization rule;
|
||||||
|
6. an authorization certificate;
|
||||||
|
7. reauthorization after persistence;
|
||||||
|
8. hostile tests for forged witness, broadened scope, stale version, altered
|
||||||
|
parent, and valid-candidate pruning attacks.
|
||||||
|
|
||||||
|
Until that machinery exists, the exact certificates support diagnosis and
|
||||||
|
priority only.
|
||||||
|
|
||||||
|
## Import requirements
|
||||||
|
|
||||||
|
A future importer into `DiscoveryStore` must:
|
||||||
|
|
||||||
|
1. register canonical problem, instance, and scope objects;
|
||||||
|
2. run `certificates/p28_famm_scars_validator.py` and reject a malformed role,
|
||||||
|
scope, count, hash pin, or hard-authority claim;
|
||||||
|
3. verify every declared artifact hash;
|
||||||
|
4. execute the mandatory checker commands against those exact bytes;
|
||||||
|
5. translate local IDs to store `NodeId` values;
|
||||||
|
6. construct nodes through the Rust API;
|
||||||
|
7. recompute canonical discovery hashes;
|
||||||
|
8. replay the resulting store and MMR;
|
||||||
|
9. retain every SoftScar as non-pruning;
|
||||||
|
10. leave `blocked_promotion_ideas` outside `HardIndex`.
|
||||||
|
|
||||||
|
Failure at any step is a typed import or replay failure, not evidence that a
|
||||||
|
mathematical proof candidate is impossible.
|
||||||
127
optional/ramanujan_problem_2_8_adversarial_audit.md
Normal file
127
optional/ramanujan_problem_2_8_adversarial_audit.md
Normal file
|
|
@ -0,0 +1,127 @@
|
||||||
|
# Adversarial Audit — Ramanujan Challenge Problem 2.8
|
||||||
|
|
||||||
|
## Verdict
|
||||||
|
|
||||||
|
The recurrence-specific proof path passes the repaired adversarial audit.
|
||||||
|
Every Ore, differential-gauge, terminating-induction, valuation, convergence,
|
||||||
|
and all-four-column obligation is now displayed as an equation and replayed
|
||||||
|
without a computer-algebra decision procedure. The active all-column proof is
|
||||||
|
an elementary positive-cone contraction; the earlier spectral/stable-graph
|
||||||
|
route remains in the package as a replayed legacy alternative.
|
||||||
|
|
||||||
|
The exact trust boundary is important:
|
||||||
|
|
||||||
|
- The proof imports the classical Chudnovsky formula as one explicitly named
|
||||||
|
theorem, with a precise citation to a complete modular/CM derivation.
|
||||||
|
- It also uses foundational results stated with their hypotheses: absolute
|
||||||
|
convergence of power series, the maximum modulus principle, and completeness
|
||||||
|
of bounded monotone real sequences.
|
||||||
|
- It does **not** claim to be axiom-free or to reconstruct those foundational
|
||||||
|
theorems from set theory.
|
||||||
|
|
||||||
|
Relative to that explicit boundary, no recurrence-specific assumption,
|
||||||
|
vacuous implication, numerical-equality inference, or hidden CAS remainder
|
||||||
|
remains.
|
||||||
|
|
||||||
|
## Defects found and repaired
|
||||||
|
|
||||||
|
| Initial defect | Why it failed | Equation-level repair |
|
||||||
|
|---|---|---|
|
||||||
|
| The deformed transfer was under-defined | Only one substituted coefficient was shown; later notation changed the meaning of the first argument | Displayed all sixteen entries of \(\mathcal M(u,x)\), defined \(M_N(x)=\mathcal M(2N+3,x)\), and displayed both official seed rows |
|
||||||
|
| Three matrix terms lost a plus sign during the first repair | The manuscript matrix then differed from the certified matrix | Restored the three sums in \(c_1,c_2,c_3\); hostile replay caught this before release |
|
||||||
|
| Ore divisions used `quo_rem` | A zero remainder was trusted rather than exhibited | Replaced every division with four direct cleared factorizations \(D_r=q_rL_+\), including the fourth companion closure |
|
||||||
|
| “Standard ascension identity” and transformed ODE were named but not derived | The coefficient mechanism was hidden | Added initial coefficient and consecutive-ratio equations; expanded the \({}_3F_2\) Euler operator explicitly |
|
||||||
|
| ODE normalization was claimed to determine the terminating \({}_4F_3\) uniquely | False: the exponent \(2n\) supplies an additional analytic branch | Replaced uniqueness with base, generic, and top coefficient induction for the actual one-step operator |
|
||||||
|
| The scalar one-step operator was not tied to the challenge matrix | Hard-coded \(d_0,d_1\) could have described a surrogate | Added horizontal reconstruction, all sixteen differential-gauge equations, and the exact matrix contraction producing \(d_0+zd_1\) |
|
||||||
|
| Only the first base component was initially checked | The actual compact seed row was not yet known to be horizontal | Added all four base-row reconstruction equations, the base terminating-operator equation, and all four base adjoint residuals |
|
||||||
|
| Two DVR-lemma hypotheses were only implicit | The induction had not displayed the \(k_{N+1}\) leading direction or \(J_N(0)e_1\ne0\) | Added both expansions and cited them explicitly at the induction step |
|
||||||
|
| A transfer norm inequality used an upper bound with exponent \(-1\) | The inequality direction was invalid for column four | Split \(j\le3\) and \(j=4\), then used coupled row factors to obtain \(\|\mathcal B_m\|_\infty\le4981375/512<10000\) |
|
||||||
|
| The maximum-modulus step omitted holomorphy of the quotient | Formal divisibility only supplied a local removable germ | Proved holomorphy on \(|x|\le1/4\), identified the only possible pole, and removed it with the \(2n\)-valuation |
|
||||||
|
| Birkhoff–Poincaré was used as a black box for three columns | It hid the exceptional hyperplane, dominant functional, decay, and denominator nonvanishing | First replaced it with an explicit stable graph; the optimized proof now eliminates the spectral layer entirely via \(T_m=\mathcal P\mathcal B_m\mathcal P^{-1}>0\) and a four-weight min/max contraction |
|
||||||
|
| The spectral route required a quartic root count, eigenvector, and exceptional-hyperplane analysis | Although repaired, it created unnecessary proof surface | Verified all 285 positive numerator coefficients, the positive limiting transfer, and both positive seeds; all four quotients are now convex averages with uniformly positive weights |
|
||||||
|
| Division in columns \(2,3,4\) preceded an eventual-nonzero proof | The displayed quotients were not yet justified | The positive-cone seed and transfer identities now give \(Q_{m,j}>0\) for every \(m\ge1\), before any quotient is formed |
|
||||||
|
| The direct rational differential gauge produced large unreduced intermediates | Correct but slow replay increased resource and serialization risk | Added a separately reconstructed \(J_0+xJ_1+x^2J_2\) decomposition and checked the denominator-cleared polynomial gauge in 176 scalar coefficient obligations |
|
||||||
|
| The terminating step polynomial obscured its structure with 21 expanded terms | Large coefficients made transcription review difficult | Rewrote it in \(u=2n+1,\ q=2n-t\), then added a direct coefficient identity against the former expansion |
|
||||||
|
| A FAMM `SoftScar` was initially linked with `DerivedFrom` | It did not follow the repository’s calibrated `Supports` parent pattern | Corrected every parent role and added a fail-closed FAMM interchange validator; all scars remain advisory |
|
||||||
|
| The checker could succeed while Wolfram/Sage were absent | A stored transcript was being treated as proof evidence | Made standard-library rational-polynomial verifiers mandatory; Wolfram and Sage are now optional independent cross-checks |
|
||||||
|
| Metadata called \(Q/P\) the requested orientation | The official challenge asks for \(P/Q\) | Corrected every release document to state \(P/Q\to\sqrt{10005}/\pi\) as the official orientation |
|
||||||
|
|
||||||
|
## Mandatory replay
|
||||||
|
|
||||||
|
Run:
|
||||||
|
|
||||||
|
```sh
|
||||||
|
./run_checks.sh
|
||||||
|
```
|
||||||
|
|
||||||
|
The mandatory path executes:
|
||||||
|
|
||||||
|
1. `p28_rank_ode_bound_verifier.py`
|
||||||
|
2. `p28_convergence_constants.py`
|
||||||
|
3. `p28_standalone_equations.py`
|
||||||
|
4. `p28_optimized_gauge.py`
|
||||||
|
5. `p28_positive_cone.py`
|
||||||
|
6. `p28_mutation_sensitivity.py`
|
||||||
|
7. `p28_famm_scars_validator.py`
|
||||||
|
|
||||||
|
It then replays `p28_dominant_product_algebra.py` as a preserved legacy
|
||||||
|
cross-check; that quartic/spectral route is not required by the active proof.
|
||||||
|
|
||||||
|
The third verifier checks:
|
||||||
|
|
||||||
|
- four cleared tail factorizations;
|
||||||
|
- lowest and generic tail coefficients;
|
||||||
|
- horizontal reconstruction;
|
||||||
|
- the terminating-operator closure;
|
||||||
|
- all sixteen differential-gauge entries;
|
||||||
|
- the authoritative matrix-to-scalar contraction;
|
||||||
|
- the base polynomial and four base-row components;
|
||||||
|
- the base terminating equation and four base adjoint residuals;
|
||||||
|
- constant, generic, and top terminating induction;
|
||||||
|
- ascension and the \({}_3F_2\) Euler equation.
|
||||||
|
|
||||||
|
The positive-cone verifier checks:
|
||||||
|
|
||||||
|
- the authoritative \(M_m\), balanced \(\mathcal B_m\), and
|
||||||
|
\(T_m=\mathcal P\mathcal B_m\mathcal P^{-1}\);
|
||||||
|
- all sixteen rational identities \(T_{m,ij}=N_{ij}/D_{ij}\);
|
||||||
|
- all 285 strictly positive coefficients of the \(N_{ij}(m-1,R-4)\);
|
||||||
|
- the exact positive limiting matrix;
|
||||||
|
- all eight positive coordinates of the two official transformed seeds.
|
||||||
|
|
||||||
|
The optimized gauge separately checks 176 scalar coefficients while the
|
||||||
|
original sixteen-entry gauge remains in the standalone checker. These
|
||||||
|
verifiers use `fractions.Fraction` and explicit coefficient dictionaries. None
|
||||||
|
uses polynomial division, factorization, a simplifier, Gröbner bases,
|
||||||
|
irreducibility, GCD, a root finder, a special-function package, sampling, or
|
||||||
|
a stored transcript.
|
||||||
|
|
||||||
|
## Forbidden-shortcut search
|
||||||
|
|
||||||
|
The mandatory runner rejects these constructs in the proof path:
|
||||||
|
|
||||||
|
- `quo_rem`
|
||||||
|
- `is_irreducible`
|
||||||
|
- polynomial `gcd`
|
||||||
|
- Birkhoff/Poincaré delegation
|
||||||
|
- “standard ascension”
|
||||||
|
- ODE-normalization uniqueness
|
||||||
|
- the former dominant-product lemma in the active manuscript
|
||||||
|
|
||||||
|
No occurrence of `native_decide`, `axiom`, `sorry`, or `admit` was found.
|
||||||
|
|
||||||
|
## Independent hostile replays
|
||||||
|
|
||||||
|
Independent reviews and mutation replays targeted:
|
||||||
|
|
||||||
|
- logical validity, indexing, vacuity, and denominator domains;
|
||||||
|
- Ore/special-function and matrix-to-scalar algebra;
|
||||||
|
- convergence and all-column division;
|
||||||
|
- one-coefficient corruption of the positive-cone numerator table;
|
||||||
|
- one-coefficient corruption of the optimized \(J\)-decomposition.
|
||||||
|
|
||||||
|
The defects in the table above were discovered during those loops. The final
|
||||||
|
Ore, gauge, positive-cone, convergence, and logic/vacuity replays return PASS,
|
||||||
|
and both corrupted checkers fail at their intended identities. Release
|
||||||
|
engineering then repeats the mandatory checks in a clean extraction, rebuilds
|
||||||
|
the PDF, and performs page-by-page visual inspection.
|
||||||
BIN
optional/ramanujan_problem_2_8_optimized_proof_a00fe05.bundle
Normal file
BIN
optional/ramanujan_problem_2_8_optimized_proof_a00fe05.bundle
Normal file
Binary file not shown.
BIN
optional/ramanujan_problem_2_8_optimized_solution.pdf
Normal file
BIN
optional/ramanujan_problem_2_8_optimized_solution.pdf
Normal file
Binary file not shown.
BIN
optional/ramanujan_problem_2_8_optional_improvements.zip
Normal file
BIN
optional/ramanujan_problem_2_8_optional_improvements.zip
Normal file
Binary file not shown.
Loading…
Add table
Reference in a new issue