EXACT BYTES · EXPLICIT HYPOTHESES · CHECKED PROOFS
Formal proofs without inflated claims.
The original 27 September 2026 Lean lane covers 13 scalar companions recovered from GP-FOR-192. It adds machine-checkable logic to the existing provenance and review system. It does not formalize the entire research program.
Scientific effect: NONE. Independent statement-alignment review at this source snapshot: PENDING. This page is an explanation, not a live acceptance register.
Current research sources
Pinned source observation: . Compare this timestamp with the present time; observation is not scientific revalidation.
main cefdb56e87a1787be2874ec260a70a730bbbddd7 · Math- 6e502c1f8a5632eb90670fd9fc0d52e421c015a2
Current status source · Current research guide · Current proof index
Current mathematical atlas · Current static graph and complete source inventory · Exact current observation payload · Historical mathematical material (original pins and observation). Scientific effect: NONE.
History capacity: 2 of 512 mathematical archives; 25985735 of 805306368 conservative retained bytes (including registry and release-key allowances). Publication refuses additional versions at capacity; no history is pruned.
Four questions, four kinds of evidence.
Identity: Which exact source bytes and dependencies were used?
Logic: Does the pinned proof establish the displayed Lean statement, with only the allowed foundational axioms?
Alignment: Does that statement represent the intended informal claim and its hypotheses?
Acceptance: Have the existing source, analytic, dependency and independent-review requirements been met?
A successful build answers neither the alignment nor the acceptance question by itself.
Inspect the implementation.
Implementation and review discussion · Exact successor source · Actual execution outcome and artifacts
The linked run supplies its real outcome. The run record was read on 8 October 2026 through the GitHub API; GitHub workflow artifacts expire on the repository's retention schedule, and no in-repository copy of this run's receipt is recorded on this page. A PR's presence is not evidence that it has merged; Math #92 merged on 27 September 2026. The first failed build is retained; explicitly named successors repair three compiler issues without changing the theorem statements.
The gate requires source hashes, a fresh build, kernel recheck, all 13 transitive axiom reports, and five deliberately invalid or extra-axiom variants at that successor commit. Missing evidence does not earn a checked label. The current Math- gate covers a larger inventory; see Since this snapshot.
What the 13 companions cover.
This is the original source snapshot, not a current formalization inventory. These scalar identities and conditional implications retain their supplied hypotheses. Each recorded conclusion is paired with the broader claim it does not establish.
Inspect all 13 scalar declarations and their limits
| Targets | Exact coverage | Not established |
|---|---|---|
ec005_fold_gap | Canonical polynomial foldPotential gap for every real s | Random-field normal-form construction or persistence pairing |
ec008_factor_expansion | Scalar polynomial factor identity in real c,s | Construction/positivity of the actual conditional covariance matrix |
ec010_generic, ec010_transverse | Polynomial identities for arbitrary real parameters | Validity/coverage of the underlying geometric charts |
ec011_scalar_cancellation | Commutative real scalar cancellation | An ODE, matrix adjoint transport or Hessian symmetry |
ec014_contact_power | Scalar inverse-power cancellation for r nonzero | Six-pin determinant, change of variables or Kac–Rice density |
p02_lm008_r2_cancel | Quotient cancellation when r,cZ are nonzero | A probabilistic conditioning argument |
p02_lm008_cross_multiplied, p02_lm008_quotient_bound | Implications from supplied numerator and lower-normalizer bounds and displayed sign assumptions | Conditional Cauchy–Schwarz, moment estimates, existence or uniformity of the lower normalizer |
p02_lm009_bad_event_threshold, p02_lm009_power40_identity | Deterministic threshold and exponent algebra | Markov/moment hypotheses or tail-event measurability |
p02_lm009_r4_le_r3, p02_lm009_palm_r4_to_r3 | Polynomial comparison on 0 <= r <= 1 and conditional bound with C >= 0 | Existence of a uniform C, all-small-r stochastic theorem or parent closure |
Source: Open the immutable scope record. Git blob e5094ac386b72668b7dc42805bf8e6e64a731fac; 3,832 UTF-8 bytes; SHA-256 350732d7a501fd37d15632b13bd2ac30b8a6d87259b9a3b0931639041a1cfb84. The table is a reading view of those bytes, not a new alignment review or acceptance decision.
In particular, an upper normalizer bound cannot supply the required lower bound. The quotient-transfer bounds remain supplied hypotheses. Open the complete source for its definitions, review contract and retained limits.
What these companions do not prove.
They do not establish the SIDE24 coefficient enclosure, the Gaussian/Palm construction, the elder-rule selection theorem, a six-pin Jacobian theorem, or the full lifetime law. In the quotient-transfer companion, the numerator estimate and lower-normalizer bound are supplied hypotheses.
Read the target-by-target scope. Blueprint links help navigation; independent review must still check meaning.
Since this snapshot.
This page does not track later formal work. As read on 7 October 2026 at Math- 390a2f0 and main 4ff9e92:
- The Math- formal package lists 63 declarations, including these 13. Its manifest still records alignment as pending independent review. Dated delegated-AI statement-alignment records for its 20-, 29- and 36-target stages carry zero organizational-independence credit; read each record's scope, performer and errata. The same read also holds two statement reads of the merged 40-target Math #279 package, in directories dated 5 October: an xAI scoped PASS, which calls itself “a statement comparison for the four new declarations and a byte check of the retained proof modules and execution controls” and states that it “is not a 40-target alignment acceptance, and no alignment.json is published”, and an Anthropic “PASS on all 40 targets, scoped to their displayed hypotheses” whose alignment.candidate.json is withheld and is not an accepted alignment.json; each directory carries its own erratum file. Neither changes the manifest's pending alignment status.
- main has a separate 31-target SIDE24 arithmetic package. It does not formalize the coefficient enclosure.
- Math- has a separate cap first-exit Lean packet with its own gate and alignment map.
As read on 12 October 2026 at Math- b45512e, Math- specifications/ also holds a statement-only Lean register and a proof packet whose inventoried theorems are each typed as one of the registered statements (a theorem there is evidence about its Lean statement only; the packet does not establish the parent theorems and carries zero organizational-independence credit, and no claim changes status because of it); alignment of each statement to its mathematical source is pending independent review, and this page does not track that work.
None of these records changes scientific status. For the newest state, open the current Math- formal README and, for the statement register and proof packet, the current Math- specifications directory.
Investigate the next layer.
The original rollout, alignment questions and subsequent implementation discussions are recorded in the formal-verification work item, main #95 (closed 27 September 2026; historical rollout context). For later formal packets and their source PRs, start with the 7 October cap-formalization card; the 3 October reading cut keeps the v1.4 record.