Finite Erdos Denominator-Order Certificate Strike

Computes an exact-arithmetic denominator-order identity and catches forged ones, not the open Erdos problem.

Contract

Does Computes a finite denominator-order certificate in exact whole-number arithmetic. For a finite set F of exponents and a base b, it sums 1/(b^n - 1) over the exponents as an exact fraction P/Q, then checks a sharp claim: the multiplicative order of b modulo the reduced denominator Q is exactly the least common multiple of F. It shows the certificate holding on small cases — including one where a common factor cancels in the fraction yet the claim still holds — and it shows two forged certificates being caught: a wrong order and a wrong denominator are both rejected because the runner recomputes the real values and compares. This is the finite identity behind the Erdos #257 period-noncollapse strike; it is not a solution to the open problem.

Scope limit It computes the finite denominator-order certificate ord_Q(b)=lcm(F) for S_F(b)=sum 1/(b^n-1)=P/Q in exact rational arithmetic over bounded public fixtures and rejects forged certificates by recomputation; it does not establish the open infinite Erdos #257 problem, is not an oracle, prover, or provider result, and a holding certificate is a bounded computational witness, not a machine-checked proof.

Run

Quick probe

microcosm finite-erdos-denominator-certificate-strike run --input fixtures/first_wave/finite_erdos_denominator_certificate_strike/input --out /tmp/plectis-public-runs/finite_erdos_denominator_certificate_strike

Validator command

microcosm finite-erdos-denominator-certificate-strike run --input fixtures/first_wave/finite_erdos_denominator_certificate_strike/input --out receipts/first_wave/finite_erdos_denominator_certificate_strike --acceptance-out receipts/acceptance/first_wave/finite_erdos_denominator_certificate_strike_fixture_acceptance.json

Evidence

ClassBounded runtime computationevidence 4/5Real runtime resultRuns real tools

Links to Certificate Kernel Execution Lab, Verifier Lab Kernel, Formal Math Lean Proof Witness

formal-mathnumber-theoryexact-arithmetic

Source

Source Design note · Source

Map Show on the map

Index Open compact index card

Paper module

Paper module Finite Erdos Denominator-Order Certificate Strike

The finite Erdos denominator-order certificate strike surfaces the public finite_denominator_order_certificate bundle and verifies, in exact rational arithmetic, that ord_Q(b)=lcm(F) for S_F(b)=sum 1/(b^n-1)=P/Q over bounded public fixtures.

Read the full write-up

Back to Components index → Reference roster →