```
```

Good Math

Specify.
Prove. Check.

Start with a mathematical specification, prove what follows from it, verify the encoded theorem where formal checking is useful, compute concrete cases, and state the resulting reading point clearly.

\[ \text{specification} \longrightarrow \text{proof} \longrightarrow \text{formal verification} \longrightarrow \text{computation} \longrightarrow \text{reading point} \]

The General Divisor Theorem

Residue conditions and divisibility constraints interact in a precise way. The theorem identifies the exact admissibility condition, the minimal repeating period, and the exact density correction.

Featured result

The General Divisor Theorem

Exact Density Correction under Residue Conditioning

\[ d=\mathrm{rad}(\gcd(m,N)), \qquad R=\frac{\mathrm{rad}(N)}{d} \]
\[ \gcd(a,d)=1 \quad\Longrightarrow\quad T_{\min} = mR = \mathrm{lcm}(m,\mathrm{rad}(N)) \]
\[ \#\text{ accepted values per period} = \varphi(R), \qquad C(N,m) = \frac{d}{\varphi(d)} \]

In plain language: the prime factors shared by the residue condition and the divisibility condition determine the correction. The remaining prime factors determine the repeating structure.

Read the paper Mathematical Basis

Machine-checked formalization

The General Divisor Theorem has been formalized in Lean 4. The formal statement and proof provide a machine-checked counterpart to the written theorem and proof.

\[ \text{divisor.pdf} \longleftrightarrow \text{Lean theorem} \longrightarrow \text{kernel check} \]

Reproduce the formal verification with lake build.

Lean proof Lean source

Two ways to see it

A familiar case shows where mod 30 fits. A second case shows why the general theorem needs the sharper admissibility condition.

Familiar specialization

Modulo 30

With \(N=m=30\), the theorem reduces to the eight residue classes coprime to 30.

{ 1, 7, 11, 13, 17, 19, 23, 29 }

These are exactly the candidate residue classes for primes greater than 5.

Try the mod 30 demo

Distinguishing example

\(N=5,\ m=6,\ a=2\)

Here \(a\) shares a factor with \(m\), but that shared factor is irrelevant to coprimality with \(N\). The general theorem correctly keeps the residue class admissible.

\[ 2,\ 8,\ 14,\ 26 \]

Four accepted values occur in the minimal period \(30\), exactly as the theorem specifies.

From theorem to reading point

The theorem specifies the mathematical structure. A computation or measurement can then supply a reading point within that specification. The interactive modulo 30 instrument at readingpoint.app lets you enter an integer and see its residue in the 30-state modular reading space.

Open Reading Point

How Good Math works

Mathematical claims are kept close to the specifications that support them. Proof establishes the general result. Formal verification checks the encoded theorem mechanically. Computation supplies concrete cases and reading points where it adds useful evidence.

Specify

State the mathematical objects, assumptions, constraints, and applicable boundaries.

Prove

Establish the result from the stated hypotheses and keep the proof close to the theorem it supports.

Verify

Formalize the theorem where machine checking provides an independent check of the encoded mathematical statement and proof.

Read

Record the resulting mathematical or computational reading point together with the specification that produces it.

Computation remains part of the workflow. Executable tests can realize examples, test cases, and reading points. Formal verification and computation provide different kinds of checks.

Mathematical Basis

For readers who want the underlying project structure, Mathematical Basis keeps statements, proof audits, formalizations, tests, and results separately addressable.

MB_0001 General Divisor Theorem proved · Lean verified MB_0005 Coordinate Distribution Specifies the Ellipsoid-Fitting Phase Boundary audited · supported

Connected work

Mathematical statements, scientific investigations, formal verification, and reading-point tools remain separately addressable while sharing a common specification workflow.

goodmath.app Mathematical specifications, proofs, formal verification, and reading points. readingpoint.app Interactive specifications and computational reading points. labreports.app Source-grounded scientific investigations. GitHub Statements, proof audits, formalizations, tests, results, and papers.
\[ \text{specification} \neq \text{reading point} \]

State the reading together with the specification that produces it.

```