• Paper 167 — Sophie Germain Primes: Barrier-Side Empirical Observations and a Lean 4 Axiom-Free Conjunction-Wall Witness (within Rei-AIOS Context)
  • Abstract
  • Section 1. Introduction
    • 1.1 Scope and what this paper is not
    • 1.2 What this paper does not claim
    • 1.3 What this paper does claim
    • 1.4 Methodological framing
  • Section 2. Path 1 — Hardy-Littlewood ratio extrapolation N = 10³ to 10⁸
    • 2.1 Setup
    • 2.2 Results
    • 2.3 Honest interpretation 【観察】
    • 2.4 Honest non-claims
  • Section 3. Path 2 — SG prime gap spectral statistics
    • 3.1 Motivation
    • 3.2 Setup
    • 3.3 Results
    • 3.4 Honest interpretation 【観察】
    • 3.5 Honest non-claims
  • Section 4. Path 3 — Lean 4 axiom-free conjunction-wall witness
    • 4.1 Motivation
    • 4.2 Lean 4 formalization
    • 4.3 Axiom audit
    • 4.4 What this is and is not
  • Section 5. Path 4 — Best-effort online audit and a Pattern-5 correction
    • 5.1 The audit task
    • 5.2 What was online-verified
    • 5.3 The Pattern-5 correction
    • 5.4 What remains unaudited
    • 5.5 Honest interpretation of Path 4 itself
  • Section 6. Honest scope footer (audit gates)
  • Section 7. References
    • 7.1 Primary references — directly cited
    • 7.2 Background references — cited for context
    • 7.3 OEIS and computational references
    • 7.4 Rei-AIOS internal references — for traceability
  • Appendix A — Lean 4 axiom audit output
  • Appendix B — Computational reproduction details
  • Version history

§Paper 167 — Sophie Germain Primes: Barrier-Side Empirical Observations and a Lean 4 Axiom-Free Conjunction-Wall Witness (within Rei-AIOS Context)

Status: v0.1-DRAFT (2026-06-18) Authors: 藤本 伸樹 (Nobuki Fujimoto) / Claude Opus (Anthropic) / chat-Claude (Anthropic, articulation thread 2026-06-17) Date: 2026-06-18 License: AGPL-3.0 + Commercial (Rei-AIOS dual license) DOI: TBD (Zenodo deposit at publish time) Version: v0.1-DRAFT note.com: https://note.com/nifty_godwit2635 rei-aios site: https://rei-aios.pages.dev Source artifacts:

• scripts/empirical/parity-barrier-toy-2026-06-18.py (parity barrier toy implementation)
• scripts/empirical/sg-analysis-2026-06-18.py (Experiments 1–4 comprehensive)
• scripts/empirical/sg-extrapolation-2026-06-18.py (Path 1 N=10⁸ extrapolation)
• scripts/empirical/sg-gap-spectral-2026-06-18.py (Path 2 spectral analysis)
• data/lean4-mathlib/CollatzRei/SGConjunctionWall.lean (Path 3 Lean 4 axiom-free witnesses)

§Abstract

We report four barrier-side empirical observations on Sophie Germain (SG) primes — primes p with 2p + 1 also prime — using the Bellman-Ford LP-infeasibility framework previously developed for Collatz Lyapunov obstructions (Rei-AIOS Phase B, 2026-06-17). No part of this work claims progress toward the SG-primes-infinity conjecture or any other forward direction; per Rei-AIOS feedback principle 8 (barrier-side discipline) and three explicit non-claim boundaries, the present paper is restricted to observation, formal witness, and online-verifiable audit. The four observations are: (1) the ratio empirical / Hardy-Littlewood-predicted decreases monotonically 1.337 → 1.221 → 1.176 → 1.120 → 1.103 → 1.087 across N = 10³, 10⁴, 10⁵, 10⁶, 10⁷, 10⁸, consistent with the Hardy-Littlewood (1923) asymptote 2C₂ x / (ln x)² but constituting empirical convergence, not a proof; (2) the SG prime gap distribution is Poisson-like with ⟨r⟩ = 0.4154 (Atas et al. 2013 reference values: Poisson ≈ 0.386, GOE ≈ 0.531, GUE ≈ 0.603), with L1 distance to Poisson 0.123 vs. to GUE 0.745 — in sharp contrast to Riemann zeros which are GUE-like; (3) an explicit Lean 4 axiom-free finite-witness theorem set (11/11 theorems, depending only on propext, Classical.choice, Quot.sound) exhibits that several single-component feature families — is_prime(n), is_prime(2n+1), n mod 6, and the pair (is_prime(n), n mod 6) — fail to strict-detect SG-primality, with the BF-feasibility phase boundary located precisely at the full conjunction is_prime(n) ∧ is_prime(2n+1); (4) a best-effort online audit of Friedlander-Iwaniec (2010, Opera de Cribro) and Selberg’s parity problem catches a Pattern-5 internal record error (Selberg’s parity-problem identification year is 1949, not the previously recorded “1960s”), confirmed against Wikipedia and Tao (2007). The paper is best read alongside the Selberg parity-problem literature (Selberg 1949; Friedlander–Iwaniec 2010; Tao 2007) as a small barrier-side description, not as a contribution to forward sieve theory.

Keywords: Sophie Germain primes, parity problem, sieve theory barrier, Hardy-Littlewood conjecture, Bellman-Ford infeasibility, Lean 4 axiom-free, conjunction wall, barrier-side discipline.

§Section 1. Introduction

§1.1 Scope and what this paper is not

This paper documents an exploratory analysis carried out within the Rei-AIOS workflow on 2026-06-18, in response to the question: given the barrier-mapping toolkit assembled for Collatz Lyapunov-style obstructions, what empirical observations does that same toolkit produce when applied to Sophie Germain primes?

The answer, honestly recorded, is four small observations, none of which advance the SG-primes-infinity conjecture and none of which constitute new sieve-theoretic methodology. We name them up front so the scope is clear:

1. Numerical convergence of empirical-to-predicted ratio under the Hardy-Littlewood (1923) k-tuple conjecture (Section 2).
2. Poisson-like spectral statistics for SG-prime gaps, in contrast to the GUE-like statistics of Riemann zeros (Section 3).
3. A Lean 4 axiom-free finite-witness theorem set showing several single-component features fail to strict-detect SG-ness; the conjunction is the wall (Section 4).
4. A Pattern-5 internal record correction caught by best-effort online audit (Section 5).

§1.2 What this paper does not claim

Per Rei-AIOS feedback principle 8 (“Rei methodology = barrier-side discipline”, established 2026-06-18 from four independent applications: Collatz / Millennium-general / Sophie Germain / individual-Millennium), the forward direction — solving, partially solving, or producing technical apparatus that would solve SG-primes infinity — is structurally outside the present toolkit’s range. The Selberg parity barrier (Selberg 1949; cf. Tao 2007 for a modern exposition) is a proven obstruction to standard sieve methods reaching the infinity result, and the present paper does not pretend to circumvent it. The toy model in Section 4 is a simplified linear analogue of the parity barrier, not the real barrier.

In particular, this paper explicitly does not:

• (a) Claim progress toward SG primes being infinite.
• (b) Claim verification of the Hardy-Littlewood formula (numerical agreement is observation, not proof; cf. the Skewes-number historical lesson on π(x) vs. Li(x)).
• (c) Claim that D-FUMT₈, ZCSG, SNST, SELF⟲, or any other Rei-native artifact is a unification of, technical input to, or formalization of the parity barrier.
• (d) Claim a “general obstruction prover” or “Beyond Selberg” framework. The Bellman-Ford infeasibility encoding is a labelling correspondence with parity-style barriers, not a formal homomorphism.

These four non-claims are recorded as permanent boundaries in the Rei-AIOS memory at project_sg_explicit_non_claims_2026-06-18.md; the present paper restates them in Section 6 as audit gates for any future reading.

§1.3 What this paper does claim

The four sections each include a precise scope-pinned claim of the kind: under the specific encoding / parameters / feature family used, the following finite or computational observation holds. The claims are individually checkable from the source artifacts listed in the header.

§1.4 Methodological framing

The methodology is borrowed wholesale from the Rei-AIOS Phase A→B→C Collatz work of 2026-06-17 (project_collatz_aeb_sequence_2026-06-18.md, reference_collatz_lyapunov_obstruction_generalized_2026-06-17.md):

• An LP-infeasibility / negative-cycle Bellman-Ford encoding of “Lyapunov-like” feasibility questions, reduced via log-cancellation to pure rational linear arithmetic and decidable by standard graph algorithms in O(|V| · |E|) time.
• An axiom-free Lean 4 + Mathlib v4.27 record discipline for finite witnesses, with kernel-axiom audits via #print axioms.
• A three-tier honest-scope discipline: 【観察 / observation】, 【仮説 / hypothesis】, 【思弁 / speculation】, with a fourth implicit tier 【連想 / mere association】 used as a reject-default.

We make no claim that this framing is new: the BF/LP encoding is a standard tool, the axiom-free Lean 4 discipline is widely practiced in the Mathlib community, and the three-tier honesty discipline is a long tradition under different names. Section 6 records the discipline.

§Section 2. Path 1 — Hardy-Littlewood ratio extrapolation N = 10³ to 10⁸

§2.1 Setup

The Hardy-Littlewood (1923) k-tuple conjecture, specialized to Sophie Germain primes, predicts

$$ \pi_{SG}(x) \sim 2 C_2 \cdot \frac{x}{(\ln x)^2} $$

where C_2 = ∏_{p ≥ 3 prime} p(p-2) / (p-1)² ≈ 0.66016181584... is the twin-prime constant. We computed the empirical count π_{SG}(N) for N ∈ {10³, 10⁴, 10⁵, 10⁶, 10⁷, 10⁸} and the ratio empirical / predicted.

The sieve was implemented as a single bytearray of length 2N + 1 (one byte per index), giving memory footprint of about 191 MB at N = 10⁸. Total wall-clock at N = 10⁸ was approximately 13 seconds on a single thread.

§2.2 Results

The empirical counts at N = 10³, 10⁴, 10⁵, 10⁶, 10⁷, 10⁸ all match OEIS A092816 exactly.

§2.3 Honest interpretation 【観察】

The ratio sequence {1.3372, 1.2207, 1.1758, 1.1198, 1.1025, 1.0875} is strictly monotone decreasing, with successive decade-to-decade ratios 0.913, 0.963, 0.952, 0.985, 0.984 — i.e. the rate of approach is itself slowing, consistent with the predicted 1 + O(1 / \ln N) correction structure of the leading-order asymptotic.

This is the kind of finite-N behaviour one would expect if the Hardy-Littlewood prediction is the correct asymptotic. It is not a proof. Numerical evidence of even far greater extent has historically been misleading in analytic number theory — the canonical example being Littlewood (1914) and Skewes (1933) on π(x) vs. Li(x), where empirical evidence up to enormous x suggested an inequality that was later shown to reverse infinitely often. We do not claim verification of the Hardy-Littlewood conjecture; we claim that the empirical count, at our scan range, is consistent with that conjecture’s leading order.

§2.4 Honest non-claims

• We do not claim the deviation will continue to decrease (only that it has in our range).
• We do not claim a rate of convergence.
• We do not claim agreement at any specific N beyond 10⁸.

§Section 3. Path 2 — SG prime gap spectral statistics

§3.1 Motivation

Riemann zeros, under the Hilbert–Pólya programme, show eigenvalue statistics matching the Gaussian Unitary Ensemble (GUE) — a well-documented empirical match (Montgomery 1973; Odlyzko 1987; cf. Rei-AIOS STEP 1162–1165 for our own reproduction of this). One natural question, in the spirit of “how much spectral structure is visible in SG primes?”, is: do SG prime gaps exhibit any of the same eigenvalue-like statistics?

The standard test statistics are:

• ⟨r⟩ (Atas et al. 2013): the mean of r_i = min(s_i, s_{i+1}) / max(s_i, s_{i+1}) where s_i is the i-th gap. Reference values: Poisson ≈ 0.386, GOE ≈ 0.531, GUE ≈ 0.603.
• The spacing histogram (in units of mean gap), compared to the Poisson density e^{-s} and the GUE Wigner surmise density (32/π²) s² e^{-4s²/π}.
• The number variance Σ²(L) (number of points in a length-L window), compared to Poisson Σ²(L) = L (linear) and GUE Σ²(L) ∼ (1/π²)(\ln(2πL) + γ + 1) (sub-linear logarithmic).

§3.2 Setup

We used the 56,032 SG primes up to 10⁷ from Section 2. From these we computed 56,030 nearest-neighbour-ratio samples and a 20-bin spacing histogram on [0, 4] (in units of mean gap).

§3.3 Results

⟨r⟩ statistic:

The closest reference is Poisson, with a modest positive deviation of 0.029.

Spacing histogram L1 distance:

The empirical spacing distribution is approximately 6× closer to Poisson than to GUE.

Number variance Σ²(L) for L ∈ {1, 2, 4, 8, 16} on the unfolded sequence:

The ratio variance / L is approximately 1.0 for L ≤ 8, consistent with Poisson; deviation at L = 16 is likely a finite-sample artefact (200 windows per L).

§3.4 Honest interpretation 【観察】

SG prime gaps display essentially Poisson statistics on these standard tests. This is consistent with the heuristic view, going back to Hardy–Littlewood, that primes (and constrained-prime patterns such as SG) behave statistically like a random Poisson-thinned process at finite scales. It is structurally different from the GUE behaviour of Riemann zeros; the two are not the same kind of “spectral” object.

§3.5 Honest non-claims

• We do not claim that SG primes are a Poisson process (only that the three test statistics, at our sample size, are Poisson-consistent).
• We do not claim a Riemann-zeros-style spectral interpretation; the apparent randomness is itself the structural fact.
• The modest positive ⟨r⟩ deviation (0.4154 vs. 0.386) is not investigated as a “structure”; we record it.

§Section 4. Path 3 — Lean 4 axiom-free conjunction-wall witness

§4.1 Motivation

In an earlier Rei-AIOS experiment (Experiment 3 of the SG comprehensive analysis, 2026-06-18), we observed a sharp phase transition in the BF-LP-infeasibility encoding of SG-detection: every parity-blind feature family produced INFEASIBLE, and the transition to FEASIBLE occurred precisely at the full conjunction is_prime(n) ∧ is_prime(2n+1) — no intermediate feature combination gave FEASIBLE. We refer to this as the conjunction wall observation.

The wall observation is itself structurally tautological: “the feature you’d need to know to detect SG-ness is literally SG-ness”. But the finite-witness form of the underlying insufficiency claim — for each named feature F, exhibit two specific natural numbers n, m with F(n) = F(m) but is_SG(n) ≠ is_SG(m) — is non-trivially recordable as an axiom-free Lean 4 + Mathlib v4.27 theorem.

§4.2 Lean 4 formalization

The file data/lean4-mathlib/CollatzRei/SGConjunctionWall.lean (~110 lines) records 11 theorems:

• 6 elementary isSG-status theorems (sg_eleven, not_sg_seven, sg_five, not_sg_seventeen, sg_two, not_sg_thirteen), each proved by decide plus negation of a Nat.Prime-claim;
• 4 single-feature insufficiency witnesses (feature_isprime_n_insufficient, feature_isprime_2np1_insufficient, feature_mod6_insufficient, feature_pair_isprime_mod6_insufficient);
• 1 tautological positive control (conjunction_is_sufficient) recording that isSG n ↔ Nat.Prime n ∧ Nat.Prime (2n+1).

The concrete witnesses are: 7, 11 (both prime; 15 = 3·5 composite vs. 23 prime), 2, 8 (both have is_prime(2n+1) true; 2 is SG, 8 is not prime so not SG), 5, 17 (both prime, both ≡ 5 (mod 6); 11 prime vs. 35 = 5·7 composite).

§4.3 Axiom audit

A #print axioms audit was carried out on a temporary SGConjunctionWallAxiomCheck.lean file, with the following result. All four insufficiency witness theorems and all six elementary status theorems depend exactly on [propext, Classical.choice, Quot.sound] — the Mathlib kernel base for decide-tactics involving Decidable.Nat.Prime. The tautological conjunction_is_sufficient depends only on [propext]. No theorem in the file uses sorryAx or native_decide, and the kernel-axiom profile matches that of the Phase A T1ObstructionWitness.lean and Paper 158 (Bipartite Ramsey) records.

§4.4 What this is and is not

This is a Lean 4 record of finite, decidable arithmetic facts. It is not:

• A formalization of the Selberg parity barrier (which is a statement about asymptotic-density behaviour of sieve weights, not about finite witnesses).
• A proof that all parity-blind feature families are insufficient (which would require an existence-of-conflict-bucket lemma that we did not attempt to formalize).
• An advancement on SG-primes-infinity in any direction.

It is: a small mechanical record of the phase-transition observation, in the form of named axiom-free witnesses that another Lean 4 user can lake env lean and verify in a few seconds.

§Section 5. Path 4 — Best-effort online audit and a Pattern-5 correction

§5.1 The audit task

The Rei-AIOS Sophie-Germain workstream had, from its first turn, recorded an honest confession that two primary references had not been consulted in their original form:

• Friedlander, J., and Iwaniec, H. (2010), Opera de Cribro, AMS Colloquium Publications, Vol. 57.
• Selberg, A. (cited as “1960s”), original papers on the parity problem in sieve theory.

Path 4 of the present analysis was a best-effort online audit to verify, by Wikipedia / blog / book-listing access, what facts about these references could be confirmed and where the audit gap remains.

§5.2 What was online-verified

The following items were checked against the Wikipedia article Parity problem (sieve theory), the Terence Tao blog post “Open question: the parity problem in sieve theory” (2007-06-05), and the AMS / Google Books listing for Opera de Cribro:

• Selberg identified and named the parity problem in 1949 (not “1960s” as the workstream had been recording).
• The “parity principle” name traces to Selberg’s sieve work, with the observation present from around 1946.
• Tao’s modern formulation: if A is a set whose elements are all products of an odd number of primes (or all products of an even number of primes), then sieve theory cannot provide non-trivial lower bounds on the size of A.
• The Liouville function λ(n) is the mechanism: λ is essentially orthogonal to divisor sums, and multiplying (1 + λ(n)) into a sieve identity forces the main term to vanish for one parity class.
• Opera de Cribro (Friedlander–Iwaniec 2010) is the modern reference, ISBN 978-0821849705, and the book explicitly addresses the parity-barrier-breach work the same authors initiated in their 1996 result on primes of the form a² + b⁴.
• Recent post-2010 progress on twin-prime-style bounded gaps (Zhang 2013; Maynard–Tao 2014) does not cross the parity barrier and does not reach gap = 2.

§5.3 The Pattern-5 correction

The “1960s” date in the Rei-AIOS internal record was incorrect; it should have been 1949. The error appeared in five files:

• memory/project_sg_discipline_application_2026-06-18.md
• memory/reference_difficulty_typology_collatz_riemann_sg_2026-06-18.md
• scripts/empirical/parity-barrier-toy-2026-06-18.py
• scripts/empirical/parity-barrier-toy-spec-2026-06-18.md
• (referenced indirectly in scripts/empirical/sg-analysis-2026-06-18.py honest-scope footer)

All five were corrected in the same commit cycle as this paper, with ★ 訂正: 旧 「1960s」 誤り → 1949、 Path 4 audit per [[reference-friedlander-iwaniec-selberg-parity-audit-2026-06-18]] annotations.

The internal origin of the “1960s” date is unclear: it may have been a training-data residue, a chat-Claude-thread paraphrase that propagated, or simply a confusion with the 1968 Bombieri density theorem and other 1960s sieve-era results. We do not investigate the precise origin; we record that the audit caught it.

§5.4 What remains unaudited

Five items are explicitly not covered by online sources and remain audit-gap items for future builders:

• Selberg’s original 1949 paper, in primary form.
• Opera de Cribro’s specific chapter content (Google Books gives only the back-cover description and limited preview).
• Selberg’s 1947 sieve paper, in primary form.
• The Friedlander–Iwaniec 1996 Annals of Mathematics paper, in primary form.
• The precise formal correspondence between Tao’s barrier framework and the natural-proofs / relativization / algebrization barrier family in complexity theory.

These are recorded as audit-gap items in memory/reference_friedlander_iwaniec_selberg_parity_audit_2026-06-18.md.

§5.5 Honest interpretation of Path 4 itself

The fact that Path 4 caught an error is operationally important: it is direct evidence that the audit-gap-confession discipline (which had been articulated as a permanent principle in Rei-AIOS feedback files) is not cosmetic. The discipline produced a correction even within the same workstream that confessed the gap. We do not generalize this to “the discipline always works”; we record that, on this one occasion, it did.

§Section 6. Honest scope footer (audit gates)

Per project_sg_explicit_non_claims_2026-06-18.md, three permanent claim-boundaries are restated here as audit gates for any future use of this paper’s content:

1. No D-FUMT₈ / ZCSG / SELF⟲ “unification” claim. None of the Rei-native eight-valued logic, three-layer notation, or self-application-fixed-point apparatus is asserted to be a formalization of, technical contribution to, or unification of the parity problem or Sophie Germain primes. The phase-transition observation in Section 4 is a finite combinatorial fact about SG-detection encoded in a Bellman-Ford constraint graph; it is not a category-theoretic equivalence with any Rei-native fixed-point structure.
2. No “partial progress toward SG-primes infinity” claim. The four observations are barrier-side description, not forward solving. The wording “partial”, “progress”, “step toward”, or “direction” is rejected as a paraphrase for any of the results recorded here.
3. No “Rei verified the Hardy-Littlewood formula” claim. Numerical agreement between empirical counts and the leading-order asymptotic at finite N is observation, not proof. Sections 2 and 3 are explicit about this; the Skewes-number historical lesson is cited.

We also restate the eighth Rei-AIOS feedback principle (feedback_rei_methodology_barrier_side_discipline.md, 2026-06-18): Rei methodology is a barrier-side / describing discipline, not a forward-side / solving one. This paper is one operational instance of that principle. We do not claim the principle is universally correct, only that, on the four problem cases on which it has been tested to date (Collatz, Millennium-7 in general, Sophie Germain, individual Millennium problems), the boundary it describes has held.

§Section 7. References

§7.1 Primary references — directly cited

• Atas, Y. Y., Bogomolny, E., Giraud, O., and Roux, G. (2013), “Distribution of the ratio of consecutive level spacings in random matrix ensembles”, Physical Review Letters 110, 084101.
• Friedlander, J., and Iwaniec, H. (2010), Opera de Cribro, AMS Colloquium Publications, Vol. 57. ISBN 978-0821849705.
• Hardy, G. H., and Littlewood, J. E. (1923), “Some problems of ‘Partitio Numerorum’: III. On the expression of a number as a sum of primes”, Acta Mathematica 44, 1–70.
• Selberg, A. (1949), papers introducing the parity problem in sieve theory (cited via Wikipedia: Parity problem (sieve theory); primary text not directly consulted).
• Tao, T. (2007), “Open question: the parity problem in sieve theory”, blog post at https://terrytao.wordpress.com/2007/06/05/open-question-the-parity-problem-in-sieve-theory/, accessed 2026-06-18.
• Wikipedia (2026), Parity problem (sieve theory), https://en.wikipedia.org/wiki/Parity_problem_(sieve_theory), accessed 2026-06-18.

§7.2 Background references — cited for context

• Brun, V. (1919), original sieve theorem on twin primes (cited via secondary sources).
• Chen, J. R. (1973), “On the representation of a larger even integer as the sum of a prime and the product of at most two primes”, Sci. Sinica 16, 157–176.
• Friedlander, J., and Iwaniec, H. (1998), “The polynomial x² + y⁴ captures its primes”, Annals of Mathematics 148, 945–1040 (parity-barrier-breach result).
• Littlewood, J. E. (1914), “Sur la distribution des nombres premiers”, Comptes Rendus 158, 1869–1872.
• Maynard, J. (2015), “Small gaps between primes”, Annals of Mathematics 181, 383–413.
• Montgomery, H. L. (1973), “The pair correlation of zeros of the zeta function”, in Proceedings of Symposia in Pure Mathematics 24, 181–193.
• Odlyzko, A. M. (1987), “On the distribution of spacings between zeros of the zeta function”, Mathematics of Computation 48, 273–308.
• Skewes, S. (1933), “On the difference π(x) − Li(x)”, J. London Math. Soc. 8, 277–283.
• Tao, T. (2019), “Almost all orbits of the Collatz map attain almost bounded values”, arXiv:1909.03562.
• Zhang, Y. (2014), “Bounded gaps between primes”, Annals of Mathematics 179, 1121–1174.

§7.3 OEIS and computational references

• OEIS A005384, “Sophie Germain primes p (2p + 1 also prime)”.
• OEIS A092816, “Number of Sophie Germain primes ≤ 10ⁿ”.

§7.4 Rei-AIOS internal references — for traceability

• memory/feedback_rei_methodology_barrier_side_discipline.md (8th principle).
• memory/feedback_no_rush_publication.md (1st principle).
• memory/feedback_evaluation_symmetry_principle.md (2nd principle).
• memory/feedback_world_uniqueness_claim_controllable.md (3rd principle).
• memory/feedback_super_naming_siren_family_pattern.md (4th principle).
• memory/feedback_chat_claude_over_deference.md (6th principle).
• memory/feedback_chat_claude_hallucination_warning.md (7th principle).
• memory/feedback_line_count_size_vs_kind_distinction.md (5th principle).
• memory/reference_collatz_lyapunov_obstruction_generalized_2026-06-17.md (Phase B BF framework origin).
• memory/project_collatz_aeb_sequence_2026-06-18.md (Phase B 9-feature-space extension).
• memory/reference_difficulty_typology_collatz_riemann_sg_2026-06-18.md (three-axis typology).
• memory/project_sg_discipline_application_2026-06-18.md (six discipline-asset application).
• memory/project_sg_explicit_non_claims_2026-06-18.md (three explicit non-claims).
• memory/reference_friedlander_iwaniec_selberg_parity_audit_2026-06-18.md (Path 4 audit + 1949 correction).
• scripts/empirical/parity-barrier-toy-spec-2026-06-18.md (toy model specification).

§Appendix A — Lean 4 axiom audit output

The audit was carried out by adding a temporary SGConjunctionWallAxiomCheck.lean file invoking #print axioms on each load-bearing theorem. The complete output is reproduced below.

'CollatzRei.SGConjunctionWall.sg_eleven' depends on axioms:
  [propext, Classical.choice, Quot.sound]
'CollatzRei.SGConjunctionWall.not_sg_seven' depends on axioms:
  [propext, Classical.choice, Quot.sound]
'CollatzRei.SGConjunctionWall.sg_five' depends on axioms:
  [propext, Classical.choice, Quot.sound]
'CollatzRei.SGConjunctionWall.not_sg_seventeen' depends on axioms:
  [propext, Classical.choice, Quot.sound]
'CollatzRei.SGConjunctionWall.sg_two' depends on axioms:
  [propext, Classical.choice, Quot.sound]
'CollatzRei.SGConjunctionWall.not_sg_thirteen' depends on axioms:
  [propext, Classical.choice, Quot.sound]
'CollatzRei.SGConjunctionWall.feature_isprime_n_insufficient' depends on axioms:
  [propext, Classical.choice, Quot.sound]
'CollatzRei.SGConjunctionWall.feature_isprime_2np1_insufficient' depends on axioms:
  [propext, Classical.choice, Quot.sound]
'CollatzRei.SGConjunctionWall.feature_mod6_insufficient' depends on axioms:
  [propext, Classical.choice, Quot.sound]
'CollatzRei.SGConjunctionWall.feature_pair_isprime_mod6_insufficient' depends on axioms:
  [propext, Classical.choice, Quot.sound]
'CollatzRei.SGConjunctionWall.conjunction_is_sufficient' depends on axioms:
  [propext]

No theorem uses sorryAx or native_decide. The audit file was deleted after verification.

§Appendix B — Computational reproduction details

All four experiments are reproducible from the listed source artifacts. Key parameters:

• Path 1 sieve: bytearray of length 2N + 1, mark-multiples up to √(2N+1). At N = 10⁸, memory ≈ 191 MB; wall-clock ≈ 13 s on a single thread (Intel i7-class 2020s commodity workstation).
• Path 2 statistics: ⟨r⟩ over 56,030 consecutive-gap-ratio samples; spacing histogram with 20 bins on [0, 4] in units of mean gap; number variance over 200 random windows per L value.
• Path 3 Lean: lake env lean CollatzRei/SGConjunctionWall.lean (~6 s on the same workstation; 780 jobs total when including dependencies).
• Path 4 audit: two WebSearch and two WebFetch calls against Wikipedia and Tao’s blog; no API keys or restricted access required.

The full JSON output of the four experiments is committed to the source repository at data/empirical/sg-analysis-2026-06-18.json, data/empirical/sg-extrapolation-2026-06-18.json, data/empirical/sg-gap-spectral-2026-06-18.json, and (separately, for the more general toy model) data/empirical/parity-barrier-toy-2026-06-18.json.

§Version history

• v0.1-DRAFT (2026-06-18): Initial release. Four sections corresponding to Paths 1–4 of the 2026-06-18 SG analysis workstream. Three explicit non-claim boundaries restated. Pattern-5 correction (Selberg 1949, not 1960s) recorded as Section 5 finding.