docs: add external research import maps

2026-07-31 03:05:21 +00:00 · 2026-05-20 18:41:21 -05:00 · 2026-05-20 18:41:21 -05:00 · 836b587573
commit 836b587573
parent e7c93feec2
11 changed files with 1332 additions and 1 deletions
--- a/0-Core-Formalism/otom/docs/audit/Erdos2026_StatusTiers_ConfirmedReported.md
+++ b/0-Core-Formalism/otom/docs/audit/Erdos2026_StatusTiers_ConfirmedReported.md
@ -32,6 +32,93 @@ UNVERIFIED:

 ## Items

+### OpenAI planar unit-distance breakthrough
+
+Status:
+
+```text
+CONFIRMED_BY_OFFICIAL_SOURCE
+EXTERNAL_EXPERT_REVIEW_REPORTED
+EXTERNAL_REFERENCE
+```
+
+Claim:
+
+```text
+OpenAI reports that an internal general-purpose reasoning model produced a proof disproving Erdős's planar unit-distance conjectured upper bound.
+The proof constructs infinitely many n-point planar sets with nu(n) >= n^(1+delta) for fixed delta > 0.
+```
+
+Source:
+
+```text
+Official post: https://openai.com/index/model-disproves-discrete-geometry-conjecture/
+Proof PDF: https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-proof.pdf
+Companion remarks: https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-remarks.pdf
+```
+
+Judo flip:
+
+```text
+Square-grid prior was too narrow. Algebraic number theory supplies a richer construction family for planar incidence density.
+```
+
+Stack action:
+
+```text
+Add OpenAIUnitDistance2026ExternalReference and route through all seven layers via docs/research/OPENAI_UNIT_DISTANCE_2026_IMPORT.md.
+Do not promote to internal theorem until a local formalization or executable verifier exists.
+```
+
+### Recent AI math solves import map
+
+Status:
+
+```text
+EXTERNAL_REFERENCE
+STATUS_TIERED_IMPORT
+```
+
+Claim:
+
+```text
+Several additional 2026 AI-math results now have enough source quality to track
+as external references, while keeping proof status separate from narrative
+status.
+```
+
+Source:
+
+```text
+Import note: 6-Documentation/docs/research/RECENT_AI_MATH_SOLVES_2026_IMPORT.md
+```
+
+Included targets:
+
+```text
+Fel's Conjecture on Syzygies of Numerical Semigroups:
+  PAPER_BACKED_FORMALIZED, arXiv:2602.03716
+
+Rethlas/Archon Anderson open problem:
+  PAPER_BACKED_FORMALIZED, arXiv:2604.03789
+
+OpenAI First Proof submissions:
+  OFFICIAL_REVIEW_PENDING, OpenAI official post + arXiv:2602.05192
+
+Formal Conjectures benchmark:
+  TRACKING_SURFACE, arXiv:2605.13171
+
+Tao Erdős AI contributions wiki:
+  TRACKING_SURFACE, provisional triage index only
+```
+
+Stack action:
+
+```text
+Add RecentAIMathSolves2026ExternalReference.
+Use the source-tier labels before funding any V_scope claim.
+```
+
 ### Erdős Problem #728

 Status:
--- a/6-Documentation/docs/research/OPENAI_UNIT_DISTANCE_2026_IMPORT.md
+++ b/6-Documentation/docs/research/OPENAI_UNIT_DISTANCE_2026_IMPORT.md
@ -0,0 +1,177 @@
+# OpenAI 2026 Planar Unit-Distance Breakthrough Import
+
+Status: EXTERNAL_REFERENCE
+Date ingested: 2026-05-20
+Primary source: https://openai.com/index/model-disproves-discrete-geometry-conjecture/
+Proof PDF: https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-proof.pdf
+Companion remarks: https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-remarks.pdf
+Abridged model trace: https://cdn.openai.com/pdf/1625eff6-5ac1-40d8-b1db-5d5cf925de8b/unit-distance-cot.pdf
+
+## Claim Boundary
+
+This is an external mathematical result, not a Research Stack theorem.
+
+The result concerns the planar unit-distance function:
+
+```text
+nu(P) = number of unordered pairs {x,y} in P with |x-y| = 1
+nu(n) = max nu(P) over all n-point planar sets P
+```
+
+OpenAI reports that an internal general-purpose reasoning model produced a proof disproving Erdős's conjectured upper bound `nu(n) <= n^(1 + C / log log n)`. The proof establishes that for infinitely many `n`, there are planar point sets with:
+
+```text
+nu(n) >= n^(1 + delta)
+```
+
+for some fixed `delta > 0`. OpenAI's summary says a forthcoming refinement by Will Sawin can take `delta = 0.014`.
+
+## What Changed
+
+Before this result, the best known lower-bound constructions were essentially lattice/grid constructions in the spirit of Erdős's 1946 construction. The common expectation was that square-grid-like behavior was asymptotically close to optimal.
+
+The new result refutes that belief by importing deep algebraic number theory into planar combinatorial geometry.
+
+## How It Was Done
+
+The proof has two separable parts.
+
+### 1. Arithmetic Engine
+
+The classical grid construction can be understood through Gaussian integers `Z[i]`: many factorizations of a norm create many lattice vectors of the same length.
+
+The new construction generalizes this idea:
+
+- Replace `Q(i)` / Gaussian integers with `K = L(i)`, where `L` is a totally real field of growing degree.
+- Choose rational primes that split completely in `L`.
+- Use conjugate prime-ideal pairs in `K` to create many ideal products.
+- Use a class-group pigeonhole argument to turn many ideal choices into many elements `u` with relative norm `u c(u) = 1`.
+- Under every complex embedding, those elements have absolute value `1`, so they become candidate unit translations.
+
+The hard existence input is a family of number fields with controlled discriminants/class numbers and prescribed splitting. The paper gets this via:
+
+- unramified pro-3 class field towers
+- Chebotarev splitting
+- Shafarevich relation-rank estimates
+- Golod-Shafarevich theory
+- Hajir-Maire-style class-field-tower methods
+
+### 2. Geometric Projection
+
+Once the proof has many norm-one elements:
+
+- Embed `K` into a high-dimensional complex Minkowski space.
+- Build a lattice `Lambda` from a scaled ring of integers.
+- Cut the lattice by a product of discs.
+- Count directed pairs `(x, x+u)` where `u` is one of the many norm-one elements.
+- Project injectively to one complex coordinate, identified with `R^2`.
+
+Because the first coordinate of each `u` has modulus `1`, counted pairs project to unit segments in the plane. A packing bound controls the number of projected points, giving the polynomial improvement:
+
+```text
+nu(P_j) >= n_j^(1 + delta)
+```
+
+for infinitely many projected point sets.
+
+## Why AI Found It
+
+The companion remarks emphasize that the path was easy for humans to dismiss:
+
+- Most attention was spent trying to prove the Erdős upper bound, not disprove it.
+- A counterexample required seriously pursuing a generalization of the original lattice construction.
+- The route only works if the solver knows enough class field theory to recognize the needed infinite towers.
+- The AI appears to have persisted down a long-shot construction path while combining distant machinery.
+
+This is a useful stack lesson: frontier search needs a route memory that does not over-penalize "unlikely but lawful" bridges between distant domains.
+
+## Level-by-Level Import
+
+### L0 Primordial
+
+Import as a new arithmetic-geometric witness pattern:
+
+```text
+norm-one algebraic unit -> unit translation vector
+```
+
+This belongs beside PIST/DIAT shell arithmetic as a reminder that integer/factorization structure can surface as geometric incidence density.
+
+### L1 Geometric
+
+Import as a unit-distance construction surface:
+
+```text
+high-dimensional lattice cut -> injective complex-coordinate projection -> planar unit segments
+```
+
+This should inform GWL, toroidal shell, and quaternion/torsion work: useful planar geometry may be a projection shadow of a richer arithmetic embedding.
+
+### L2 Biological
+
+Import only as an analogy guard:
+
+```text
+latent high-dimensional code -> projected phenotype/contact graph
+```
+
+Do not promote biological claims from it. The safe use is structural: hidden algebraic constraints can produce dense observable interaction graphs.
+
+### L3 Thermodynamic
+
+Import as a cost/entropy lesson:
+
+```text
+many low-dimensional contacts can be generated by high-dimensional structured search
+```
+
+This matters for compression pressure and donated-cycle work: a large search cost can be worthwhile when it discovers a reusable construction family.
+
+### L4 Security
+
+Import into AngrySphinx/FAMM:
+
+```text
+do not discard long-shot routes solely because the community prior is low
+```
+
+The model succeeded by exploring a route humans had little incentive to pursue. FAMM scars should penalize failed routes, but not globally ban lawful cross-domain routes with strong invariant hooks.
+
+### L5 Semantic
+
+Import as a semantic bridge:
+
+```text
+algebraic number theory <-> discrete geometry
+```
+
+The bridge is not metaphorical: norm, splitting, embedding, projection, and unit distance are linked by explicit maps.
+
+### L6 Meta
+
+Import as a search-policy update:
+
+```text
+frontier discovery = broad technical vocabulary + persistence + verifier feedback
+```
+
+The relevant meta-strategy is not "AI magic"; it is cross-domain generation, strict proof checking, external expert verification, and later human simplification.
+
+## Stack Actions
+
+- Add `OpenAIUnitDistance2026` as an external reference in concept maps.
+- Add an Erdős unit-distance route distinct from existing Erdős distinct-distance notes.
+- Create future Lean/Rust placeholders only after the proof objects to formalize are selected.
+- Do not claim an internal proof until a local formalization or executable verifier exists.
+- Use this as a benchmark class for donated-cycle science plugins: bounded search over arithmetic/geometric construction candidates with cheap downstream invariants.
+
+## Suggested Future Modules
+
+```text
+Semantics.UnitDistance2026
+Semantics.NumberFieldUnitDistance
+Semantics.ArithmeticGeometryProjection
+tools-rs/unit-distance-receipts
+```
+
+These should begin as receipt/checker surfaces, not as theorem claims.
--- a/6-Documentation/docs/research/PHYSICS_BOOTCAMP_REFINEMENT_AUDIT.md
+++ b/6-Documentation/docs/research/PHYSICS_BOOTCAMP_REFINEMENT_AUDIT.md
@ -0,0 +1,209 @@
+# Physics Bootcamp Refinement Audit
+
+Status: EXTERNAL_REFERENCE
+Date ingested: 2026-05-20
+Source: https://www.physicsbootcamp.org/
+Primary index surface: https://www.physicsbootcamp.org/fundamentals-bootcamp.html
+
+## Claim Boundary
+
+Physics Bootcamp is used here as a curriculum coverage index, not as an
+authority for new physical claims. The stack already has broad physics equation
+coverage and several Lean physics surfaces; this audit identifies refinement
+gaps where the stack would benefit from explicit receipts, examples, or
+coverage tracking.
+
+Do not import prose or implementation from the site. Use the topic map as an
+external checklist.
+
+## Local Coverage Snapshot
+
+Existing stack surfaces already cover:
+
+```text
+Hamiltonian dimensions and dimensional homogeneity:
+  0-Core-Formalism/lean/Semantics/Semantics/HamiltonianFormal.lean
+
+SI constants and unit conversion:
+  0-Core-Formalism/lean/Semantics/Semantics/SIConstants.lean
+  0-Core-Formalism/lean/Semantics/Semantics/UnitConversion.lean
+
+Mechanics, thermodynamics, E&M, and quantum equation map:
+  3-Mathematical-Models/physics_eqs_mapped.md
+
+Physical-semantics boundary:
+  6-Documentation/docs/physics/PHYSICAL_SEMANTICS_PARADIGM.md
+
+Electromagnetic and electrostatic Lean surfaces:
+  Semantics.ElectromagneticSpectrum
+  Semantics.ElectrostaticsMetaprobe
+```
+
+## Missing Or Underweighted Refinements
+
+### 1. Measurement Receipt Layer
+
+Bootcamp starts with uncertainty, precision, accuracy, significant figures,
+absolute/relative uncertainty, propagation of uncertainty, order of magnitude,
+and dimensional analysis.
+
+Current stack has dimensions and units, but measurement quality is scattered
+across residual/error terms. Add a first-class measurement receipt:
+
+```text
+MeasuredQuantity = value + unit + absoluteUncertainty + relativeUncertainty
+MeasurementReceipt = dimensional_ok + sigfig_policy + propagation_rule
+```
+
+Suggested future Lean module:
+
+```text
+Semantics.MeasurementReceipt
+```
+
+This should be Q16_16/Q0_16 based and avoid floats in compute paths.
+
+### 2. Curriculum Coverage Matrix
+
+Bootcamp is useful because it is sequential: mechanics -> fluids/waves ->
+thermal physics -> E&M -> optics -> relativity/quantum/atomic/nuclear topics.
+
+The stack has many advanced and speculative surfaces but no simple matrix that
+answers:
+
+```text
+topic -> local module -> receipt type -> verified examples -> gaps
+```
+
+Suggested artifact:
+
+```text
+6-Documentation/docs/physics/PHYSICS_COVERAGE_MATRIX.md
+```
+
+This should prevent over-investing in high-level physics while missing basic
+receipts such as frame transforms, units, and measurement propagation.
+
+### 3. Noninertial Frame Receipts
+
+Bootcamp explicitly separates accelerating frames, rotating frames, Earth-frame
+physics, and Coriolis force.
+
+The stack mentions Coriolis in equation maps, but should expose a finite
+receipt surface:
+
+```text
+InertialFrame
+UniformlyAcceleratingFrame
+UniformlyRotatingFrame
+CoriolisTermReceipt
+```
+
+This belongs near rotation, torsion, and shell/PIST frame work. It should be a
+coordinate-transform receipt, not a new physics claim.
+
+### 4. Rigid-Body Tensor Receipts
+
+Bootcamp separates fixed-axis rotation, moment of inertia, principal axes,
+gyroscope behavior, and kinetic energy about center of mass.
+
+The stack has rotation/quaternion/torsion machinery, but the classical rigid
+body interface should have a simple tensor audit:
+
+```text
+InertiaTensorReceipt
+PrincipalAxesReceipt
+ParallelAxisReceipt
+RotationalEnergyReceipt
+```
+
+This is a good bridge between `UnitQuaternion`, GWL/toroidal shells, and
+hardware attitude/control surfaces.
+
+### 5. Thermal Transport Before Thermodynamic Abstractions
+
+Bootcamp separates thermal expansion, calorimetry, conduction, convection,
+radiation, Newton cooling, black-body radiation, first law, entropy, and kinetic
+theory.
+
+The stack has strong entropy and thermodynamic language, but it should keep
+transport receipts separate from global entropy claims:
+
+```text
+ThermalConductionReceipt
+ConvectionBoundaryReceipt
+RadiationBalanceReceipt
+CalorimetryBalanceReceipt
+MeanFreePathReceipt
+```
+
+This matters for hardware, materials, AngrySphinx compute-cost heat budgets, and
+any donated-cycle defense work.
+
+### 6. E&M Boundary Receipts
+
+Bootcamp proceeds through charge conservation, Coulomb force, potentials,
+conductors as boundaries, method of images, dielectrics, circuits, AC complex
+impedance, displacement current, Maxwell equations, and EM waves.
+
+Current stack has EM surfaces, but the boundary-condition receipts should be
+made explicit:
+
+```text
+ConductorBoundaryReceipt
+DielectricResponseReceipt
+ImageChargeReceipt
+ContinuityEquationReceipt
+MaxwellPointFormReceipt
+ComplexImpedanceReceipt
+```
+
+These are especially useful because they give cheap, checkable examples for
+semantic boundary laws.
+
+### 7. Optics As A Routing/Projection Testbed
+
+Bootcamp covers Fermat's principle, Snell/refraction, lenses, optical
+instruments, Fresnel equations, polarization, birefringence, interference, and
+interferometers.
+
+The stack already has optics references and EM spectra, but optics should be
+treated as a clean projection/routing testbed:
+
+```text
+FermatPathReceipt
+SnellBoundaryReceipt
+FresnelPolarizationReceipt
+ThinFilmInterferenceReceipt
+InterferometerPhaseReceipt
+```
+
+This is directly relevant to semantic routing: least-time path selection,
+boundary impedance mismatch, phase accounting, and projection loss.
+
+## Priority Order
+
+```text
+P0 MeasurementReceipt
+P1 PhysicsCoverageMatrix
+P2 FrameTransformReceipt
+P3 ThermalTransportReceipt
+P4 BoundaryConditionReceipt
+P5 OpticsRoutingReceipt
+```
+
+## Integration Rule
+
+Use Bootcamp as a checklist for missing receipts, not as a new theory source.
+Every promoted refinement must land as one of:
+
+```text
+Lean theorem
+Lean #eval receipt
+Q16_16/Q0_16 checker
+coverage matrix row with HOLD status
+```
+
+The likely highest-value next implementation is `MeasurementReceipt`: it would
+connect units, uncertainty propagation, significant figures, and dimensional
+analysis into a single gate before physics formulas enter the stack.
--- a/6-Documentation/docs/research/RECENT_AI_MATH_SOLVES_2026_IMPORT.md
+++ b/6-Documentation/docs/research/RECENT_AI_MATH_SOLVES_2026_IMPORT.md
@ -0,0 +1,220 @@
+# Recent AI Math Solves 2026 Import
+
+Status: EXTERNAL_REFERENCE
+Date ingested: 2026-05-20
+
+## Claim Boundary
+
+This note tracks recent AI-assisted or AI-autonomous mathematical solves that
+should influence Research Stack search policy. These are not internal theorems
+until the relevant proof object is imported, checked, or locally formalized.
+
+Status labels:
+
+```text
+PAPER_BACKED_FORMALIZED:
+  arXiv/paper claim includes a formal proof artifact or Lean/Mathlib claim
+
+OFFICIAL_REVIEW_PENDING:
+  official source reports expert-review confidence, but not a final theorem gate
+
+TRACKING_SURFACE:
+  benchmark or community index useful for routing, not itself a proof
+```
+
+## Additions
+
+### Fel's Conjecture on Syzygies of Numerical Semigroups
+
+Status:
+
+```text
+PAPER_BACKED_FORMALIZED
+EXTERNAL_REFERENCE
+```
+
+Source:
+
+```text
+arXiv: https://arxiv.org/abs/2602.03716
+```
+
+Claim:
+
+```text
+The paper proves Fel's conjecture for normalized alternating syzygy power sums
+of numerical semigroup rings. The abstract states that the argument is fully
+formalized in Lean/Mathlib and was produced automatically by AxiomProver from a
+natural-language statement.
+```
+
+Stack import:
+
+```text
+Receipt pattern: natural-language conjecture -> generated Lean proof -> paper
+writeup.
+Relevant layers: L0 algebraic identities, L5 autoformalization bridge, L6
+proof-object-first routing.
+```
+
+Do not claim local validity until the Lean project or proof artifact is checked
+inside the stack.
+
+### Rethlas/Archon Anderson Open Problem
+
+Status:
+
+```text
+PAPER_BACKED_FORMALIZED
+EXTERNAL_REFERENCE
+```
+
+Source:
+
+```text
+arXiv: https://arxiv.org/abs/2604.03789
+```
+
+Claim:
+
+```text
+The paper reports an automated framework with Rethlas for informal reasoning
+and Archon for Lean 4 formal verification. It reports resolving an open problem
+in commutative algebra with essentially no human mathematical intervention.
+Secondary summaries identify the target as D. D. Anderson's 2014 question:
+whether weak quasi-completeness implies quasi-completeness for Noetherian local
+rings, with the system producing a counterexample.
+```
+
+Stack import:
+
+```text
+Receipt pattern: theorem retrieval -> candidate proof -> formal agent gap-fill
+-> no-sorry Lean project.
+Relevant layers: L4 route memory, L5 retrieval/formalization bridge, L6
+multi-agent proof search policy.
+```
+
+The safe stack claim is about the reported architecture and proof artifact. Do
+not promote the Anderson theorem internally until the referenced Lean project is
+built locally.
+
+### OpenAI First Proof Submissions
+
+Status:
+
+```text
+OFFICIAL_REVIEW_PENDING
+EXTERNAL_REFERENCE
+```
+
+Source:
+
+```text
+OpenAI post: https://openai.com/index/first-proof-submissions/
+First Proof paper: https://arxiv.org/abs/2602.05192
+```
+
+Claim:
+
+```text
+OpenAI reports running an internal model on all ten First Proof problems. Based
+on expert feedback, OpenAI says at least five proof attempts, for problems 4, 5,
+6, 9, and 10, have a high chance of correctness, while other attempts remain
+under review.
+```
+
+Stack import:
+
+```text
+Receipt pattern: research-level problem set -> public proof attempt bundle ->
+expert feedback loop.
+Relevant layers: L6 evaluation design, L4 adversarial proof checking, L5
+problem-statement ambiguity handling.
+```
+
+This is not a solved-theorem import yet. It is a review-pipeline import.
+
+### Formal Conjectures Benchmark
+
+Status:
+
+```text
+TRACKING_SURFACE
+EXTERNAL_REFERENCE
+```
+
+Source:
+
+```text
+arXiv: https://arxiv.org/abs/2605.13171
+```
+
+Claim:
+
+```text
+Formal Conjectures provides a Lean 4 benchmark of research-level formal
+mathematical problem statements, including open conjectures and solved problems.
+The abstract reports that the benchmark has already been used to make new
+mathematical discoveries, including resolutions of open research conjectures.
+```
+
+Stack import:
+
+```text
+Receipt pattern: formalized open-problem queue -> verified proof/disproof audit
+-> benchmark refresh.
+Relevant layers: L5 formal statement routing, L6 contamination-resistant
+evaluation.
+```
+
+Use it to seed target selection and proof-checking policy, not as a theorem
+source by itself.
+
+### Erdős AI Contributions Wiki
+
+Status:
+
+```text
+TRACKING_SURFACE
+PROVISIONAL
+```
+
+Source:
+
+```text
+Tao Erdős wiki: https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems
+```
+
+Claim:
+
+```text
+The wiki tracks many 2026 AI contributions to Erdős problems, including full
+solutions, partial results, formalizations, incorrect attempts, and literature
+rediscoveries. The page itself warns that it is provisional and not a definitive
+verdict.
+```
+
+Stack import:
+
+```text
+Receipt pattern: triage index -> source lookup -> status-tiered import.
+Relevant layers: L4 scar handling for incorrect proofs, L6 provenance discipline.
+```
+
+Use the wiki as a watchlist only. Each row needs its own source or formal
+artifact before promotion.
+
+## Search Policy Update
+
+The current frontier is not one single pattern. It is four patterns:
+
+```text
+1. AI finds a proof and humans write or review it.
+2. AI generates Lean/Mathlib proof artifacts directly.
+3. AI searches literature and discovers the problem was already effectively solved.
+4. AI generates plausible attempts that require expert review and may fail.
+```
+
+The stack should keep separate receipts for all four. Collapsing them into a
+single "AI solved it" label destroys the audit value.
--- a/6-Documentation/docs/specs/ANGRYSPHINX_DONATED_CYCLE_GATE_SPEC.md
+++ b/6-Documentation/docs/specs/ANGRYSPHINX_DONATED_CYCLE_GATE_SPEC.md
@ -0,0 +1,569 @@
+# AngrySphinx Donated-Cycle Gate Specification
+
+## Version History
+
+| Version | Date | Author | Changes |
+|---------|------|--------|---------|
+| 0.1 | 2026-05-20 | Codex | Initial design spec for Anubis-style web proxy integration |
+
+---
+
+## 1. Purpose
+
+AngrySphinx Donated-Cycle Gate is a web-facing proof-of-defense layer where suspicious or adversarial clients must spend local compute before receiving protected content. Unlike generic proof-of-work, the client work is shaped so accepted proofs contribute to the defender's own gate calibration, route hardening, challenge corpus, or bounded useful-compute queue.
+
+The security doctrine is:
+
+> The attacker either leaves, or donates cycles that improve the gate defending the system.
+
+The system is intentionally compatible with an Anubis-style anti-bot proxy: browser-side or client-side challenge work is expensive for the requester, while server-side verification remains cheap and bounded.
+
+Baseline critique: a plain Anubis-style proof-of-work gate is needlessly wasteful when the solved work is only discarded. It can still be operationally useful as bot friction, but the compute is burned rather than converted into route memory, defensive calibration, or challenge hardening. AngrySphinx keeps the cheap-verification proxy shape while requiring accepted work to leave a defensive receipt.
+
+---
+
+## 2. Design Goals
+
+### 2.1 Primary Goals
+
+- Convert abusive traffic into measurable defensive work.
+- Avoid burn-only proof-of-work where accepted client cycles produce no defensive state.
+- Preserve cheap server verification for every challenge response.
+- Increase challenge difficulty based on observed attack pressure.
+- Attach every accepted proof to an auditable proof-of-defense receipt.
+- Keep protected origin services insulated from untrusted clients.
+- Make useful work optional and bounded; the default challenge remains hashcash-compatible.
+
+### 2.2 Non-Goals
+
+- Do not execute arbitrary attacker-supplied code.
+- Do not rely on server-expensive verification.
+- Do not claim that web proof-of-work stops all bot traffic.
+- Do not require useful scientific computation in the first prototype.
+- Do not weaken accessibility or legitimate low-power client access without fallback paths.
+
+---
+
+## 3. System Model
+
+### 3.1 Components
+
+| Component | Responsibility |
+|-----------|----------------|
+| Edge Proxy | Intercepts requests before origin access, issues challenges, verifies proofs |
+| Challenge Engine | Builds challenge payloads from policy, telemetry, and difficulty state |
+| Work Client | Browser or command-line solver performing bounded local compute |
+| Proof Verifier | Checks proof cheaply and deterministically |
+| PoD Ledger | Records accepted work, shell depth, attestation, and route metadata |
+| Defense Calibrator | Converts proof telemetry into difficulty and route-hardening updates |
+| Policy Layer | Refuses forbidden operations and selects fallback behavior |
+
+### 3.2 Existing Formal Anchors
+
+- `Semantics.AngrySphinx.AttackPressure`: represents attack pressure as energy quanta.
+- `Semantics.AngrySphinx.ShellDepth`: tracks S3 shell depth.
+- `Semantics.AngrySphinx.gearProduct`: computes the shell multiplier, defaulting to `2^depth`.
+- `Semantics.AngrySphinx.solveEnergy`: models required solve energy from pressure and shell depth.
+- `Semantics.AngrySphinx.PodAccumulator`: records accepted work and the last attestation.
+- `Semantics.AngrySphinx.verifyPod`: checks accumulated work against shell depth.
+- `Semantics.AngrySphinxPolicy`: enforces refusal and review gates.
+
+---
+
+## 4. Core Mechanic
+
+### 4.1 Request Flow
+
+1. Client requests a protected URL.
+2. Edge Proxy evaluates request risk using IP, path, rate, user-agent, cookies, prior receipts, and route class.
+3. If risk is low, request passes normally.
+4. If risk is medium or high, Challenge Engine emits an AngrySphinx challenge.
+5. Work Client solves the challenge locally.
+6. Client submits proof, nonce, challenge ID, and optional timing telemetry.
+7. Proof Verifier checks the proof cheaply.
+8. If valid, Edge Proxy issues a short-lived access token and forwards the request.
+9. PoD Ledger records donated work and updates defensive state.
+10. Defense Calibrator adjusts future challenge difficulty or route policy.
+
+### 4.2 Challenge Shape
+
+Every challenge must contain:
+
+```json
+{
+  "challenge_id": "opaque id",
+  "route_id": "normalized protected route class",
+  "issued_at": "unix timestamp",
+  "expires_at": "unix timestamp",
+  "difficulty": 24,
+  "shell_depth": 8,
+  "gear_ratio": 2,
+  "mode": "hashcash",
+  "seed": "server signed random seed",
+  "policy_root": "angrysphinx:web_gate:v0.1",
+  "receipt_required": true
+}
+```
+
+The initial prototype should use `mode = "hashcash"` because it is simple, auditable, and cheap to verify. Later modes can embed bounded useful-compute tasks, but only when verification remains cheap.
+
+### 4.3 Proof Shape
+
+Every proof must contain:
+
+```json
+{
+  "challenge_id": "opaque id",
+  "nonce": "client nonce",
+  "digest": "hash(seed || nonce || route_id)",
+  "client_elapsed_ms": 1830,
+  "work_claim": 16777216,
+  "client_class_hint": "browser"
+}
+```
+
+The verifier must be able to recompute the digest and compare it to the target threshold without replaying the full search.
+
+---
+
+## 5. Donated-Cycle Accounting
+
+### 5.1 Work Units
+
+The proxy records accepted challenge work as `work_units`, not trusted joules. For hashcash challenges:
+
+```text
+work_units = 2^difficulty
+```
+
+For sampled verification modes:
+
+```text
+work_units = verified_steps * confidence_factor
+```
+
+The client may report elapsed time, but elapsed time is telemetry only. It must not be trusted for accounting.
+
+### 5.2 PoD Ledger Entry
+
+Each accepted proof appends a record:
+
+```json
+{
+  "receipt_id": "pod receipt id",
+  "challenge_id": "challenge id",
+  "route_id": "normalized route",
+  "client_fingerprint": "privacy-preserving bucket",
+  "risk_class": "medium|high|hostile",
+  "difficulty": 24,
+  "shell_depth_before": 8,
+  "shell_depth_after": 9,
+  "work_units": 16777216,
+  "accepted_at": "unix timestamp",
+  "attestation": "work=...,depth=...",
+  "policy_root": "angrysphinx:web_gate:v0.1"
+}
+```
+
+This corresponds to `PodAccumulator.accumulateWork`: accepted work increases `totalWork`, and sustained hostile pressure can deepen the shell.
+
+### 5.3 Work Sinks
+
+Accepted work can support four defensive sinks:
+
+| Sink | Description | Prototype Priority |
+|------|-------------|--------------------|
+| Difficulty Calibration | Tune future difficulty by observed solve rates and route pressure | High |
+| Route Hardening | Raise challenge depth for routes receiving hostile pressure | High |
+| Challenge Corpus Expansion | Generate new signed seeds and route-specific challenge variants | Medium |
+| Science Donation Plugin Queue | Assign bounded, verifiable tasks that contribute to research or defense models | Later |
+
+The first implementation should only support calibration and route hardening. Science donation plugins should be added only after threat modeling and verification design are complete.
+
+---
+
+## 6. Difficulty and Shell Policy
+
+### 6.1 Attack Pressure
+
+Attack pressure is computed per route bucket:
+
+```text
+pressure = f(request_rate, failed_proofs, replay_attempts, origin_errors, suspicious_paths)
+```
+
+The pressure maps to `AttackPressure.joules` in the formal model. This is a normalized integer, not physical energy.
+
+### 6.2 Shell Depth
+
+Shell depth increases when hostile traffic keeps paying challenges or failing proofs:
+
+```text
+new_depth = min(max_depth, base_depth + pressure_band + route_sensitivity)
+```
+
+With default gear ratio `2`, solve cost scales as:
+
+```text
+required_work >= 2^shell_depth
+```
+
+### 6.3 Difficulty Bounds
+
+The proxy must enforce bounds:
+
+| Bound | Purpose |
+|-------|---------|
+| `min_difficulty` | Prevent zero-cost bypass |
+| `max_difficulty` | Avoid denial of service against legitimate clients |
+| `max_solve_ms_target` | Accessibility and device-safety budget |
+| `token_ttl` | Limit replay value |
+| `challenge_ttl` | Limit stale challenge reuse |
+
+Suggested initial defaults:
+
+```text
+min_difficulty = 18
+max_difficulty = 28
+base_shell_depth = 8
+max_shell_depth = 32
+challenge_ttl = 120 seconds
+access_token_ttl = 900 seconds
+```
+
+---
+
+## 7. Verification Requirements
+
+### 7.1 Server Verification
+
+Verification must be:
+
+- Deterministic.
+- Stateless or bounded-state.
+- O(1) or O(log n) relative to client work.
+- Replay resistant.
+- Bound to route, timestamp, and policy root.
+- Signed or MACed so clients cannot forge easier challenges.
+
+### 7.2 Replay Protection
+
+The server must reject:
+
+- Expired challenge IDs.
+- Reused challenge IDs.
+- Proofs bound to different routes.
+- Proofs with invalid policy roots.
+- Proofs below the target threshold.
+- Proofs for revoked challenge versions.
+
+### 7.3 Origin Isolation
+
+The origin service should only receive requests with a valid access token or trusted bypass identity. It should not implement challenge verification itself.
+
+---
+
+## 8. Science Donation Plugin Extension
+
+The science donation concept is a plugin track layered beside the live security gate. The gate still decides access using cheap proof verification. The plugin consumes eligible donated-cycle opportunities and assigns bounded work packets that can support science or defense research.
+
+The plugin must not make origin access depend on expensive server-side recomputation. Its job is to turn otherwise wasted proof-of-work into auditable science work when safe, not to put arbitrary scientific workloads in the critical request path.
+
+Critical rule: science donation is funded only by surplus attacker cost. The gate must first satisfy its defensive work requirement. Only the excess work budget above the active defense floor may be redirected to science tasks.
+
+```text
+required_defense_work = defense_floor(route, shell_depth, pressure, policy)
+paid_work            = accepted client work
+surplus_work         = max(0, paid_work - required_defense_work)
+
+science_work_allowed iff surplus_work > 0 and defense_level_after >= defense_level_before
+```
+
+If a science plugin would reduce route hardening, lower shell depth, consume verifier budget, delay refusal, weaken replay protection, or otherwise reduce the active defense level, the plugin is not admissible for that request.
+
+### 8.1 Required Properties
+
+Science donation plugins are admissible only if they satisfy:
+
+- Cheap verification.
+- No private data exposure.
+- No attacker-controlled program execution.
+- No result dependence on unverifiable floating-point behavior.
+- Bounded memory and CPU footprint.
+- Deterministic challenge generation.
+- Clear failure mode that falls back to hashcash.
+- Explicit plugin manifest describing task class, verification method, resource budget, and data provenance.
+
+### 8.2 Plugin Boundary
+
+Each plugin exposes:
+
+```json
+{
+  "plugin_id": "science.protein_microtask.v0",
+  "task_class": "bounded_search",
+  "verification": "known_witness_or_spot_check",
+  "max_client_ms": 2000,
+  "max_memory_mb": 64,
+  "data_policy": "public_or_synthetic_only",
+  "fallback_mode": "hashcash",
+  "receipt_schema": "science_donation_receipt.v0"
+}
+```
+
+The Challenge Engine may select a plugin task only when:
+
+- required defensive work has already been met
+- projected defense level will not decrease
+- surplus work remains after gate accounting
+- route policy permits plugin work
+- client class can safely run it
+- task verification remains bounded
+- task data is public or synthetic
+- fallback hashcash challenge is available
+
+### 8.3 Candidate Task Classes
+
+| Task Class | Verification Strategy | Risk |
+|------------|-----------------------|------|
+| Hashcash with route-derived seeds | Recompute digest | Low |
+| Verifiable random function preimage search | Recompute proof | Low |
+| Merkleized micro-benchmark witness | Spot-check trace commitments | Medium |
+| SAT/CNF micro-instance with known witness | Verify assignment | Medium |
+| Protein/graph heuristic search | Hard to verify cheaply | High |
+
+Scientific or research-side tasks should start as offline sinks fed by proof telemetry, not as direct web challenges.
+
+### 8.4 Plugin Receipt
+
+Science donation work emits a separate receipt linked to the PoD receipt:
+
+```json
+{
+  "science_receipt_id": "science receipt id",
+  "pod_receipt_id": "linked proof-of-defense receipt id",
+  "plugin_id": "science.protein_microtask.v0",
+  "task_id": "bounded task id",
+  "verification_result": "accepted|rejected|sampled",
+  "work_units": 16777216,
+  "output_commitment": "hash of submitted result",
+  "data_policy": "public_or_synthetic_only"
+}
+```
+
+This lets the security ledger remain simple while science donation work gets its own provenance chain.
+
+### 8.5 Defense-Preserving Redirect
+
+The redirect rule is:
+
+```text
+defense first, science second
+```
+
+The Challenge Engine computes a route-specific defense floor before issuing any science task. A client may be asked to solve a combined challenge, but the proof must be decomposable into:
+
+- the defensive portion required for access control
+- the surplus portion eligible for science donation
+
+The PoD Ledger records the defensive portion first. The Science Donation Plugin records only surplus work. If the client abandons the science portion, the gate may still accept the defensive proof if the required defense floor was met.
+
+This prevents the plugin system from becoming an accidental bypass where science work replaces route hardening.
+
+### 8.6 Practical Rule
+
+For web deployment:
+
+```text
+If verification is not cheap, it is not an AngrySphinx web gate task.
+```
+
+For plugin deployment:
+
+```text
+If science work cannot be verified cheaply online, route it to an offline donation queue instead of the access gate.
+If science work competes with the defense floor, reject the science plugin and keep the defense work.
+```
+
+---
+
+## 9. Privacy and Safety
+
+### 9.1 Client Fingerprints
+
+The ledger should store coarse buckets, not raw fingerprints:
+
+- route bucket
+- risk class
+- approximate client class
+- proof timing quantile
+- coarse network bucket if needed
+
+Avoid storing raw IPs unless operationally required. If raw IPs are stored, define retention and deletion policy.
+
+### 9.2 Legitimate Client Fallback
+
+The system must support:
+
+- authenticated bypass
+- low-power mode
+- accessibility bypass
+- allowlisted crawlers where appropriate
+- manual review or contact path
+
+### 9.3 Abuse Constraints
+
+The system must not become a client-side cryptominer or hidden compute extractor. Challenges are only issued for access control and defense. The page must clearly indicate that a security check is running.
+
+---
+
+## 10. Anubis Integration Plan
+
+### 10.1 Minimal Fork Strategy
+
+Use Anubis as the edge proxy and challenge transport, but treat its default burn-only proof-of-work model as the baseline to improve. Add AngrySphinx as a policy/accounting layer:
+
+```text
+Anubis request classifier
+  -> AngrySphinx difficulty policy
+  -> Anubis-style hash challenge
+  -> AngrySphinx proof ledger
+  -> access token
+  -> origin
+```
+
+This avoids rewriting proxy mechanics before the donated-cycle model is validated.
+
+### 10.2 Required Integration Points
+
+| Integration Point | Required Change |
+|-------------------|-----------------|
+| Challenge generation | Include `route_id`, `shell_depth`, `policy_root`, signed seed |
+| Challenge page | Brand/copy as AngrySphinx, expose clear security-check semantics |
+| Proof verification | Emit ledger event after accepted proof |
+| Difficulty policy | Compute challenge difficulty from route pressure and shell depth |
+| Metrics | Track solves, failures, replay attempts, elapsed time, and origin pass-through |
+| Admin config | Add route-specific min/max difficulty and bypass rules |
+
+### 10.3 First Prototype Scope
+
+The first prototype should implement:
+
+- Hashcash-only challenge mode.
+- Route-bound challenge IDs.
+- Signed challenge payloads.
+- In-memory or SQLite PoD ledger.
+- Per-route difficulty adjustment.
+- Basic admin metrics.
+- No useful-compute tasks yet.
+- No science donation plugins in the request-critical path yet.
+
+---
+
+## 11. Formal Mapping
+
+### 11.1 Lean Correspondence
+
+| Web Spec Concept | Lean Concept |
+|------------------|--------------|
+| risk pressure | `AttackPressure` |
+| route shell depth | `ShellDepth` |
+| difficulty multiplier | `GearRatio` / `gearProduct` |
+| donated proof work | `PodAccumulator.totalWork` |
+| accepted proof receipt | `PodAccumulator.lastAttestation` |
+| work admission check | `verifyPod` |
+| refusal policy | `AngrySphinxPolicy` / `AngrySphinxGate` |
+
+### 11.2 Intended Theorem Direction
+
+Future formal work should prove:
+
+```text
+accepted_web_proof implies ledger_work_increases
+ledger_work_increases implies nondecreasing_defense_budget
+shell_depth_increases implies required_work_non_decreasing
+invalid_or_expired_proof implies no_origin_access
+```
+
+The existing `solveEnergyExponential` theorem is the core target: route pressure should imply exponentially increasing solve obligation under bounded depth.
+
+---
+
+## 12. Operational Metrics
+
+Track:
+
+- challenge issue count
+- proof success count
+- proof failure count
+- replay rejection count
+- average solve time by difficulty
+- p95 solve time by client class
+- route pressure score
+- current route shell depth
+- donated work units per route
+- origin requests spared
+- bypass uses
+
+The key dashboard metric:
+
+```text
+defense_work_ratio = accepted_donated_work_units / origin_requests_served
+```
+
+---
+
+## 13. Open Questions
+
+- Which Anubis version and extension points should be used for the prototype?
+- Should the first ledger be SQLite, JSONL, or Prometheus-only?
+- How should authenticated users bypass or receive lower difficulty?
+- What is the maximum acceptable challenge time for low-power devices?
+- Which route classes deserve independent shell depth?
+- Should useful-compute be implemented at all in the web path, or only as an offline research sink?
+- How should FAMM route scars and PIST shell coordinates be bound into the live challenge policy?
+- What plugin manifest and receipt schema should science donation tasks use?
+
+---
+
+## 14. Implementation Milestones
+
+### Milestone 1: Baseline Gate
+
+- Run Anubis-style hashcash challenge on protected route.
+- Bind challenge to route, timestamp, and policy root.
+- Verify proof and issue short-lived access token.
+
+### Milestone 2: PoD Ledger
+
+- Persist accepted proof records.
+- Track donated work units.
+- Emit `work=...,depth=...` attestations compatible with `PodAccumulator`.
+
+### Milestone 3: Adaptive Shell Policy
+
+- Compute per-route pressure.
+- Adjust shell depth and difficulty within bounds.
+- Add replay and failure-rate hardening.
+- Wire FAMM scar memory into route hardening using `FAMMScarMemory.lean`, `FAMM.lean`, and `RouteCost.lean`.
+- Map route and challenge IDs into PIST/ShellModel coordinates using `PIST.lean`, `ShellModel.lean`, and `PistBridge.lean`.
+
+### Milestone 4: Admin and Observability
+
+- Add metrics endpoint or dashboard.
+- Show route pressure, donated work, failure rate, and current difficulty.
+- Add operational bypass and allowlist controls.
+
+### Milestone 5: Useful-Compute Research Track
+
+- Evaluate verifiable task classes offline.
+- Add only if verification remains cheap and policy-compliant.
+- Define the science donation plugin manifest.
+- Define the linked science donation receipt schema.
+- Keep plugin tasks outside the request-critical path until bounded verification is proven.
+
+---
+
+## 15. Summary
+
+AngrySphinx Donated-Cycle Gate turns anti-bot friction into a defensive asset. The attacker does not merely burn cycles; accepted work is receipted, counted, and used to harden the same gate that blocked them. An Anubis-style proxy provides the correct implementation shape because it already separates expensive client solving from cheap server verification.
--- a/6-Documentation/wiki/Concept-Archive.md
+++ b/6-Documentation/wiki/Concept-Archive.md
@ -71,7 +71,10 @@ findable with an honest status.
 | **Neural Type Eigenvector Coverage** | CANDIDATE | Broad neuron-type morphology/evidence graph reduced to a principal coverage direction, used to rank which biological analogues improve routing, compression, or verification efficiency. | `6-Documentation/docs/research/NEURAL_TYPE_EIGENVECTOR_COVERAGE.md` |
 | **NUVMAP** | CANONICAL | Non-uniform variable mapping and address projection. | `docs/GLOSSARY.md`, NUVMAP specs |
 | **OEPI** | ACTIVE | Operator Escalation Percentage Index. | `Semantics.OEPI` |
+| **OpenAI Unit Distance 2026** | EXTERNAL_REFERENCE | AI-generated proof/import map for the planar unit-distance breakthrough: algebraic number fields and class-field towers produce projected planar point sets with `nu(n) >= n^(1+delta)` infinitely often. | `6-Documentation/docs/research/OPENAI_UNIT_DISTANCE_2026_IMPORT.md` |
+| **Recent AI Math Solves 2026** | EXTERNAL_REFERENCE | Status-tiered watchlist for 2026 AI-assisted math solves and proof pipelines, including Fel's conjecture, Rethlas/Archon Anderson, OpenAI First Proof, Formal Conjectures, and the provisional Erdős AI contributions wiki. | `6-Documentation/docs/research/RECENT_AI_MATH_SOLVES_2026_IMPORT.md` |
 | **OTOM** | CANONICAL | Ordered Transformation and Orchestration Model. | `CONCEPTS.md`, `OTOMOntology.lean` |
+| **Physics Bootcamp Refinement Audit** | EXTERNAL_REFERENCE | Curriculum-checklist audit used to identify missing physics receipts: measurement uncertainty, coverage matrix, noninertial frames, rigid-body tensors, thermal transport, E&M boundaries, and optics routing. | `6-Documentation/docs/research/PHYSICS_BOOTCAMP_REFINEMENT_AUDIT.md` |
 | **PIST** | CANONICAL | Shell witness/address surface with mass conservation. | `docs/GLOSSARY.md`, `Semantics.PIST` |
 | **PodAccumulator** | ACTIVE | Distributed witness/signature accumulator. | `docs/GLOSSARY.md` |
 | **Q0_16 / Q0_64 / Q16_16** | CANONICAL | Fixed-point and scalar communication formats. | `Semantics.FixedPoint`, `docs/GLOSSARY.md` |
--- a/6-Documentation/wiki/Home.md
+++ b/6-Documentation/wiki/Home.md
@ -26,6 +26,9 @@
 | `docs/specs/PHI_S3C_PIST_BRIDGE_SPEC.md` | Phi–S3C–PIST bridge — witness transport for Phi-centered transforms |
 | `docs/specs/GCL_FIELD_EQUATIONS_SPEC.md` | GCL field equations — manifold-weighted field snapshot |
 | `docs/specs/MS3C_NESTED_REDUCTION_GEAR_SPEC.md` | Nested reduction gear — S³ shell gear reduction for AngrySphinx |
+| `docs/research/OPENAI_UNIT_DISTANCE_2026_IMPORT.md` | OpenAI 2026 planar unit-distance breakthrough — external import map across all stack levels |
+| `docs/research/RECENT_AI_MATH_SOLVES_2026_IMPORT.md` | Recent 2026 AI math solves — status-tiered external import map |
+| `docs/research/PHYSICS_BOOTCAMP_REFINEMENT_AUDIT.md` | Physics Bootcamp refinement audit — curriculum coverage gaps and receipt priorities |

 ## Research Domains

--- a/ARCHITECTURE.md
+++ b/ARCHITECTURE.md
@ -32,6 +32,22 @@ Level 0 — Primordial             PIST/DIAT Shells │ Q16.16 Arithmetic │ Br
 | 5 (Semantic) | Meaning-aware | CrossDimensionalFilter (12 primes), manifold networking, compression control | shared primes non-empty, flat→ordinary kernel |
 | 6 (Meta) | Self-aware | Cognitive load router, auto-adaptive metatyping (7 invariants), adaptation, SSMS_nD | efficiency ≥ 0, mass conservation across tiers |

+### 2.1 External Frontier Import: OpenAI Unit-Distance 2026
+
+The 2026 OpenAI planar unit-distance result is now tracked as an external reference in `6-Documentation/docs/research/OPENAI_UNIT_DISTANCE_2026_IMPORT.md`.
+
+Layer placement:
+
+| Level | Import Hook |
+|-------|-------------|
+| 0 | Norm-one algebraic elements as arithmetic witnesses for unit translations |
+| 1 | High-dimensional lattice cuts projecting to planar unit-distance graphs |
+| 2 | Structural analogy only: latent code projecting to dense interaction graph |
+| 3 | Search-cost/compression lesson for reusable construction families |
+| 4 | FAMM/AngrySphinx prior update: preserve lawful long-shot cross-domain routes |
+| 5 | Semantic bridge: algebraic number theory to discrete geometry |
+| 6 | Meta-search policy: broad machinery + persistence + verifier feedback |
+
 ---

 ## 3. Three-Axis Pipeline
--- a/MEMORY.md
+++ b/MEMORY.md
@ -39,6 +39,18 @@ The stack is organized into seven distinct functional tiers:
   - *Substrates*: Cognitive load router, auto-adaptive metatyping.
   - *Invariant*: `efficiency >= 0`, mass conservation across tiers.

+### 2.1 External Frontier Import — OpenAI Unit-Distance 2026
+
+Tracked in `6-Documentation/docs/research/OPENAI_UNIT_DISTANCE_2026_IMPORT.md`.
+
+- **L0:** norm-one algebraic elements become arithmetic witnesses for unit translations.
+- **L1:** high-dimensional lattice cuts project injectively to planar unit-distance graphs.
+- **L2:** structural analogy only: latent code can project to dense observable contact graphs.
+- **L3:** search cost can be amortized when it yields a reusable construction family.
+- **L4:** FAMM/AngrySphinx should not over-prune lawful long-shot cross-domain routes.
+- **L5:** explicit semantic bridge: algebraic number theory to discrete geometry.
+- **L6:** meta-search lesson: broad machinery, persistence, verifier feedback, external review.
+
 ---

 ## 3. The Seven Core Invariants
--- a/obsidian-vault/01-LAYERS/00-Overview.md
+++ b/obsidian-vault/01-LAYERS/00-Overview.md
@ -4,6 +4,18 @@

 The Research Stack is organized into 7 layers following the USTSM architecture, from fundamental mathematics to meta-cognitive systems.

+## External Frontier Import
+
+[[OpenAI Unit Distance 2026 Import]] is tracked as an external reference across all layers:
+
+- **L0:** norm-one arithmetic witnesses.
+- **L1:** projected unit-distance geometry.
+- **L2:** latent-code/contact-graph analogy guard.
+- **L3:** reusable construction family as search-cost amortization.
+- **L4:** FAMM/AngrySphinx long-shot route preservation.
+- **L5:** algebraic-number-theory to discrete-geometry semantic bridge.
+- **L6:** meta-search policy update from AI-generated proof + verifier feedback.
+
 ## Layer Structure

 ### Layer L0: Primordial 🟥
@ -171,4 +183,4 @@ L4 (Security) → L5 (Semantic) → L6 (Meta)

 ---

-#layer-overview #ustsm #architecture #system-design
+#layer-overview #ustsm #architecture #system-design
--- a/obsidian-vault/OpenAI
+++ b/obsidian-vault/OpenAI
@ -0,0 +1,23 @@
+# OpenAI Unit Distance 2026 Import
+
+Status: external reference
+
+Canonical repo note:
+`6-Documentation/docs/research/OPENAI_UNIT_DISTANCE_2026_IMPORT.md`
+
+Summary:
+
+- OpenAI reports an internal general-purpose reasoning model found a proof disproving Erdős's planar unit-distance conjectured upper bound.
+- The proof constructs infinitely many planar point sets with `nu(n) >= n^(1 + delta)`.
+- The method uses algebraic number theory: class field towers, splitting primes, norm-one elements, Minkowski embeddings, lattice cuts, and injective projection to one complex coordinate.
+- Stack lesson: do not let FAMM route scars over-prune lawful long-shot cross-domain bridges.
+
+Layer hooks:
+
+- L0: norm-one arithmetic witness
+- L1: projected unit-distance geometry
+- L2: latent-code/contact-graph analogy guard
+- L3: search-cost amortization
+- L4: AngrySphinx/FAMM route-prior update
+- L5: algebraic-number-theory to discrete-geometry bridge
+- L6: meta-search policy update