1
Scope and trust semantics
2
Witnesses and the conditional theorem
3
The signed smoothed circle method
4
Major arcs
5
Minor arcs
6
Tail removal and large-odd closure
7
Production providers and final threshold split
8
Reusable formal infrastructure
▶
8.1
Primary-source-linked analytic extensions
9
Native computation: semantics, risk, and mitigation
▶
9.1
What Lean accepts
9.2
Two orthogonal classifications
9.3
Threat model and residual risk
9.4
Mitigations in this repository
9.5
Worked audit chain: the Chebyshev \(\psi \) sweep
9.6
Practices in other Lean projects
10
Exact trust-boundary drilldown
▶
10.1
Native-decision certificate families
▶
10.1.1
Classification by computation architecture
10.1.2
Classification by independent replay evidence
10.2
Named external/source trust atoms
11
Primary-source audit catalog
12
Source alignment and repairs
A
Development-only profiles
B
Bibliography
Dependency graph
Blueprint for the Ternary Goldbach Formalization
Gershon Bialer
1
Scope and trust semantics
2
Witnesses and the conditional theorem
3
The signed smoothed circle method
4
Major arcs
5
Minor arcs
6
Tail removal and large-odd closure
7
Production providers and final threshold split
8
Reusable formal infrastructure
8.1
Primary-source-linked analytic extensions
9
Native computation: semantics, risk, and mitigation
9.1
What Lean accepts
9.2
Two orthogonal classifications
9.3
Threat model and residual risk
9.4
Mitigations in this repository
9.5
Worked audit chain: the Chebyshev \(\psi \) sweep
9.6
Practices in other Lean projects
10
Exact trust-boundary drilldown
10.1
Native-decision certificate families
10.1.1
Classification by computation architecture
10.1.2
Classification by independent replay evidence
10.2
Named external/source trust atoms
11
Primary-source audit catalog
12
Source alignment and repairs
A
Development-only profiles
B
Bibliography