research(proximity): add G139 Phi certificate probe

[coopertweak]

Summary

• add a stdlib-only exact probe for the G139 Phi_H certificate
• certify diagonal selected cells n = 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576
• include two non-injective accident controls: G173 and n=512,p=138027521
• add a Phi-collision witness extractor that turns failed injectivity into explicit subgroup additive relations
• add a production-scale Phi-collision witness verifier that does not enumerate the subgroup
• add a production-row arithmetic contract verifier for the public n = 2^30 retained-chunk artifact
• add Lean bridges from PhiWindowInjective to SidonModNeg and then to zero normalized G139 accidents
• expose the primitive cyclic root-set equivalence

IsPrimitiveRoot g n + n != 0 + Even n
  ==> (PhiWindowInjective g n <-> SidonModNeg (rootsFinset g n))

Result

For an order-n subgroup H=<g>, the probe checks

Phi_H(r) = (g^r - 1)^n,  1 <= r <= n/2

The first public probe rows are injective on the diagonal cells below, and the two accident controls are non-injective as expected:

diagonal-n8192:  injective=True, collision_count=0
diagonal-n16384: injective=True, collision_count=0
diagonal-n32768: injective=True, collision_count=0
diagonal-n65536: injective=True, collision_count=0
diagonal-n131072: injective=True, collision_count=0
diagonal-n262144: injective=True, collision_count=0
diagonal-n524288: injective=True, collision_count=0
diagonal-n1048576: injective=True, collision_count=0
G173-accident: non-injective, collision_count=3
n512-offdiag-accident: non-injective, collision_count=3

For each known control collision, the extractor verifies the compact relation

u = (g^r - 1) / (g^s - 1)
g^r + u = 1 + u*g^s
u^n = 1

and records the corresponding subgroup exponents/values in scripts/probes/_out_g139_phi_collision_witnesses.json. The six retained control witnesses are all non-lawful normalized G139 relations.

The verifier in scripts/probes/verify_g139_phi_collision_witness.py checks the same witness contract from either a JSON witness record or a custom command-line witness using --u or --u-exp. It never constructs the full subgroup table, so proposed production-scale collisions can be audited directly from (n,p,g,r,s,u) or (n,p,g,r,s,u_exp).

For the public production-scale retained-chunk artifact, the arithmetic contract verifier checks the row facts consumed by the Lean bridge and cross-checks the published result/verifier JSON metadata when supplied:

n = 1073741824
p = 365375409332725729550921208179070755196377235457
p - 1 = n * q
g^n = 1
g^(n/2) = -1
exact_order_n = true
merged_count = 536870912
collision_count = 0
injective = true
independent_verify_status = verified

The Lean side now proves the structural bridge:

SidonModNeg H + 1 in H ==> accidents H = empty
PhiWindowInjective g n + exact order/even hypotheses ==> SidonModNeg (rootsFinset g n)
PhiWindowInjective g n + exact order/even hypotheses ==> (accidents (rootsFinset g n)).card = 0
IsPrimitiveRoot g n + n != 0 + Even n ==> (PhiWindowInjective g n <-> SidonModNeg (rootsFinset g n))

Scope

Finite exact-arithmetic evidence plus Lean-checked bridge/API cleanup only. This is not a theorem for all n, not a production closure by itself, not a proof of the exact first-prime rule, and not a prize claim.

This builds on the G139 accident-census lane in PR #526 and Geoff's order-512 census comment on #466. The CLM-018 and CLM-019 refutations on #466 concern separate universal six-Jacobi / threshold-circularity claims and do not refute this Phi/Sidon certificate route.

Verification

• python3 scripts/probes/probe_g139_phi_certificate.py
• python3 scripts/probes/extract_g139_phi_collision_witnesses.py
• python3 scripts/probes/extract_g139_phi_collision_witnesses.py --n 64 --p 17318209 --r 4 --s 11 --label G173-single
• python3 scripts/probes/verify_g139_phi_collision_witness.py
• python3 scripts/probes/verify_g139_phi_collision_witness.py --n 64 --p 17318209 --g 9133071 --r 4 --s 11 --u-exp 34 --label G173-single
• python3 scripts/probes/verify_g139_phi_collision_witness.py --n 64 --p 17318209 --g 9133071 --r 4 --s 11 --u 11893578 --label G173-single-u
• python3 -m py_compile scripts/probes/probe_g139_phi_certificate.py scripts/probes/extract_g139_phi_collision_witnesses.py scripts/probes/verify_g139_phi_collision_witness.py scripts/probes/verify_g139_n2e30_arithmetic_contract.py
• python3 scripts/probes/verify_g139_n2e30_arithmetic_contract.py
• lake build ArkLib.Data.CodingTheory.ProximityGap.Frontier._G139SidonModNegClean
• lake build ArkLib.Data.CodingTheory.ProximityGap.Frontier._G139PhiInjectiveSidonBridge
• python3 scripts/forbidden_tokens.py
• git diff --check

Axiom audits for the new Lean bridge theorems report only:

[propext, Classical.choice, Quot.sound]

[coopertweak]

Follow-up artifact for the same Phi_H certificate line of attack:

I published a retained-chunk artifact for the selected production-scale row n = 2^30:

https://github.com/coopertweak/ArkLib/releases/tag/g139-n2e30-phi-certificate-20260807

Scope and result:

n = 1073741824
p = 365375409332725729550921208179070755196377235457
domain_size = 536870912
chunk_count = 128
collision_count = 0
injective = true
phi_image_sha256 = 47e60af06c23828d8b4353255b0dca55a4f8b7580692778ec03f6f3f8fabbc6a
sorted_record_stream_sha256 = 6e084eb8a7fa66d7e63d8f3855649764ad06a7e2de4dbe4145f34337c372b6f5

The release has 265 assets: 128 retained chunk binaries, 128 chunk manifests, verifier/generator scripts, result JSONs, README, reproduction script, and SHA256SUMS.txt.

The independent verifier was run against the public-shaped layout before upload and returned:

status = verified
mismatches = {}
merged_count = 536870912
collision_count = 0
injective = true

This is intentionally framed as a finite exact-arithmetic computational certificate for this selected cell. It is not a prize-closure claim, not a theorem for all n, and not a proof of the exact first-prime rule.

[coopertweak]

Small Lean-side bridge added in f738526477601f6df6f4363f59a58112808f3c0a:

SidonModNeg H + 1 ∈ H  ==>  accidents H = ∅
SidonModNeg H + 1 ∈ H  ==>  (accidents H).card = 0

File:

ArkLib/Data/CodingTheory/ProximityGap/Frontier/_G139SidonModNegClean.lean

This is the downstream formal reduction only: it proves that once the subgroup is Sidon modulo negation, every normalized G139 rung-2 solution is one of the three lawful Mann families. It does not prove Phi_H injectivity or turn the n=2^30 artifact into a theorem by itself.

Checks run locally:

lake env lean ArkLib/Data/CodingTheory/ProximityGap/Frontier/_G139SidonModNegClean.lean
lake build ArkLib.Data.CodingTheory.ProximityGap.Frontier._G139SidonModNegClean
python3 scripts/forbidden_tokens.py

Axiom audit for the new cardinality theorem reports only:

[propext, Classical.choice, Quot.sound]

[coopertweak]

Upstream Lean bridge added in fd58d8897693371f2382d9550f0c528bc2aa2478:

HasExactOrder g n
+ g^n = 1
+ n even / n != 0
+ 1 ∈ rootsFinset g n
+ PhiWindowInjective g n
==>
(accidents (rootsFinset g n)).card = 0

File:

ArkLib/Data/CodingTheory/ProximityGap/Frontier/_G139PhiInjectiveSidonBridge.lean

This is the upstream formal bridge connecting the Phi_H certificate predicate to zero normalized G139 accidents, under the explicit exact-order hypothesis for the generator. The finite artifact still supplies the computational PhiWindowInjective evidence for the selected n = 2^30 row; this commit does not claim a theorem for all n, prize closure, or the exact first-prime rule.

Checks run locally:

lake env lean ArkLib/Data/CodingTheory/ProximityGap/Frontier/_G139PhiInjectiveSidonBridge.lean
lake build ArkLib.Data.CodingTheory.ProximityGap.Frontier._G139PhiInjectiveSidonBridge
python3 scripts/forbidden_tokens.py
git diff --check

Axiom audit for the final theorem reports only:

[propext, Classical.choice, Quot.sound]

[coopertweak]

Arithmetic contract verifier added in 5cf7d9d0cd9bc46cbe418067a3992a22422e338f for the public n = 2^30 Phi artifact.

Files:

scripts/probes/verify_g139_n2e30_arithmetic_contract.py
scripts/probes/_out_g139_n2e30_arithmetic_contract.txt

This is a lightweight companion to the retained chunk verifier. It does not reread the 128 large chunk binaries; instead it verifies the row facts consumed by the Lean bridge and cross-checks the public result/verifier JSON metadata:

p prime via recursive Pocklington certificate
p - 1 = n * q
q factorization recorded
g^n = 1
g^(n/2) = -1
exact_order_n = true
merged_count = 536870912
collision_count = 0
injective = true
independent_verify_status = verified

Local checks run:

python3 -m py_compile scripts/probes/verify_g139_n2e30_arithmetic_contract.py
python3 scripts/probes/verify_g139_n2e30_arithmetic_contract.py
python3 scripts/probes/verify_g139_n2e30_arithmetic_contract.py --result-json <downloaded release result JSON> --verify-json <downloaded release verifier JSON>
python3 scripts/forbidden_tokens.py
git diff --check

Scope remains unchanged: finite exact-arithmetic support for this selected cell plus the formal Lean reduction; no prize-closure claim and no theorem for all n.

[coopertweak]

Small bridge-polish commit added in 88668ff6eb7ce26cbb2787a8637d06d368d552e6:

IsPrimitiveRoot g n
+ n != 0
+ Even n
==>
(PhiWindowInjective g n <-> SidonModNeg (rootsFinset g n))

This exposes the reverse direction for primitive cyclic root sets: a Phi collision gives a root-of-unity additive relation, so SidonModNeg forces Phi injectivity on the half-window. Combined with the existing forward bridge, Phi is now the certificate-friendly coordinate for exactly the Sidon obstruction in this setting.

Local checks run:

lake build ArkLib.Data.CodingTheory.ProximityGap.Frontier._G139PhiInjectiveSidonBridge
python3 scripts/forbidden_tokens.py
git diff --check

Axiom audit for the new equivalence reports only:

[propext, Classical.choice, Quot.sound]

Scope unchanged: formal bridge/API cleanup only; no theorem for all n, no prize-closure claim, and no change to the finite artifact assumptions.

[coopertweak]

Lightweight public-release metadata audit for the n = 2^30 retained artifact:

Downloaded only the small public release assets from:

https://github.com/coopertweak/ArkLib/releases/tag/g139-n2e30-phi-certificate-20260807

Assets checked:

README.md
RELEASE_NOTES.md
SHA256SUMS.txt
arklib-g139-streaming-phi-prototype-n2e30.json
arklib-g139-streaming-phi-verify-n2e30.json

The four downloaded lightweight files match their entries in SHA256SUMS.txt:

README.md: OK
RELEASE_NOTES.md: OK
arklib-g139-streaming-phi-prototype-n2e30.json: OK
arklib-g139-streaming-phi-verify-n2e30.json: OK

Then I ran the PR verifier against the downloaded public JSONs:

python3 scripts/probes/verify_g139_n2e30_arithmetic_contract.py \
  --result-json /tmp/g139-n2e30-release-light/arklib-g139-streaming-phi-prototype-n2e30.json \
  --verify-json /tmp/g139-n2e30-release-light/arklib-g139-streaming-phi-verify-n2e30.json

The output matches scripts/probes/_out_g139_n2e30_arithmetic_contract.txt exactly. In particular, the public JSON metadata agrees on:

n = 1073741824
p = 365375409332725729550921208179070755196377235457
q = 340282366920938463463374607431768211719
generator = 26841566604131443990650262696798142924116991820
domain_size = 536870912
merged_count = 536870912
collision_count = 0
injective = true
independent_verify_status = verified
mismatches = {}
chunk_records_sum = 536870912

This is only the lightweight release-metadata/contract check; it does not redownload or reverify the 128 large chunk binaries here.