- 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.
203 lines
11 KiB
Markdown
203 lines
11 KiB
Markdown
# 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.
|