terminology: remove internal jargon, sync docs to v3.4.13

Comprehensive cleanup of internal project-specific vocabulary in
Lean source files, public documentation, and the blueprint. No
mathematical content changed; only comments, docstrings, headers,
and public-facing summaries were touched.

Jargon removed (in comments/docstrings only):
- Phase 1 / 1b / 2 / 3 / 3A / 3B / 3C / 3D / 4 / 5 milestone labels
- Tier 1 / 1.1 / 2 / A / B elimination batch labels
- Category A / B / C / D / E / F axiom classification letters
- Route II / III / α investigative path names
- "Choice B", "cymyc" → generic "Kähler class" / "neural-network
  approximation"
- "Colab-verified 2026-XX-XX" date stamps in Lean files
- Internal notebook / script filenames (colab_phase*.ipynb,
  phase*.py, milestone_2026_04_19_g_star_phases.md, etc.)
- "BIRS", "R_REF", session-specific dates in docstrings

Files touched:
- 23 Lean files in GIFT/Foundations, GIFT/Spectral, GIFT/Relations,
  GIFT/Hierarchy (~55 occurrences cleaned)
- README.md: version bump 3.4.12 → 3.4.13, build jobs 8378 → 8380,
  axiom phrasing clarified ("4 logical axioms + 11 interval certs")
- contrib/CHANGELOG.md: new v3.4.13 entry documenting today's
  axiom reduction (22 → 11 in IntervalCertificates.lean),
  v3.4.12 entry rewritten in neutral vocabulary
- blueprint/src/content.tex: chapter heading + summary axiom-count
  item restated

Build: 8380 jobs OK, 0 sorry, 0 new warnings. No identifier names
or theorem statements modified; downstream proofs unchanged.

Author: Brieuc

GIFT/Foundations.lean

@@ -49,9 +49,9 @@ import GIFT.Foundations.ExplicitG2Metric
 import GIFT.Foundations.NewtonKantorovich
 -- K3 harmonic correction: torsion reduction ×2995, 1D floor (v4.0)
 import GIFT.Foundations.K3HarmonicCorrection
--- K3 NK certificate: CI(2,2,2) Donaldson k=4, h=7.83e-2 ×6.4 (v2.2, 2026-04-18)
+-- K3 NK certificate: CI(2,2,2) Donaldson k=4, h=7.83e-2 ×6.4 (v2.2)
 import GIFT.Foundations.K3NewtonKantorovich
--- Interval certificates: Phase 1b + Phase 3 Colab interval-arith brackets (2026-04-19)
+-- Interval certificates: interval-arithmetic brackets
 import GIFT.Foundations.IntervalCertificates
 
 namespace GIFT.Foundations
@@ -116,9 +116,9 @@ Derives: b₂ = 21 = 7 + 14 from G₂ representation theory!
    - Torsion-free is necessary but NOT sufficient for G₂ holonomy
    - so(7) = g₂ ⊕ g₂⊥ decomposition: 21 = 14 + 7
    - AS constraints: 147 = dim(K₇) × b₂ per point
-   - Phase 3 diagnostic: hol_rank = 21 (target: 14)
+   - Training diagnostic: hol_rank = 21 (target: 14)
 
-6. **TCSConstruction.lean** (corrected 2026-04-14)
+6. **TCSConstruction.lean**
    - Abstract TCS framework (ACyl_CY3, TCS_b2/TCS_b3 formulas)
    - Arithmetic witnesses: M1_candidate (b₂=11, b₃=40), M2_candidate (b₂=10, b₃=37)
    - b₂=21, b₃=77 certified by NK metric (not derived from TCS)

GIFT/Foundations/AmbroseSinger.lean

@@ -1,7 +1,7 @@
 -- GIFT Foundations: Ambrose-Singer Theorem and Holonomy Diagnostics
 -- The gap between torsion-free G₂ structure and G₂ holonomy
 --
--- Central insight from Phase 3 PINN training (v6-v20, Feb 2026):
+-- Central insight from PINN training (v6-v20, Feb 2026):
 -- Torsion-free (nabla phi = 0) is NECESSARY but NOT SUFFICIENT for G₂ holonomy.
 -- The curvature must additionally lie in the g₂ subalgebra of so(7).
 --
@@ -10,7 +10,7 @@
 -- 2. Dimensional gap: dim(so(7)) = 21, dim(g₂) = 14, gap = 7 = dim(K₇)
 -- 3. Holonomy constraint: Riem(g) must have image in g₂ ⊂ so(7)
 -- 4. AS diagnostic: ratio ||proj_{g₂⊥}(R)||/||R|| measures holonomy deviation
--- 5. Phase 3 status: AS ratio ~4.0 (target <1.0), hol_rank = 21 (target 14)
+-- 5. Current training status: AS ratio ~4.0 (target <1.0), hol_rank = 21 (target 14)
 --
 -- References:
 --   - Ambrose, W.; Singer, I.M. (1953). "A theorem on holonomy."
@@ -81,7 +81,7 @@ For a metric g on a 7-manifold M:
 **G₂ holonomy criterion**: AS ratio = 0 everywhere
   equivalently: the holonomy algebra has rank ≤ 14 = dim(g₂)
 
-**Phase 3 v20 status** (Feb 2026):
+**Training status** (v20, Feb 2026):
   - g₂_self (torsion-free loss) descended from 3.86 to 2.251
   - AS ratio ≈ 4.0 (curvature still has significant g₂⊥ component)
   - Holonomy rank = 21 = dim(so(7)) (full SO(7), not yet G₂)
@@ -93,7 +93,7 @@ the curvature into g₂. An explicit Ambrose-Singer loss is needed.
 /-- Target holonomy rank for G₂ holonomy -/
 def target_hol_rank : ℕ := dim_G2
 
-/-- Current holonomy rank from PINN Phase 3 v20: full so(7) -/
+/-- Current holonomy rank from PINN training v20: full so(7) -/
 def current_hol_rank : ℕ := dim_so7
 
 /-- Target holonomy rank is 14 -/
@@ -271,11 +271,11 @@ theorem holonomy_manifold_ratio : dim_G2 = p2 * dim_K7 := by native_decide
 theorem so7_triple_K7 : dim_so7 = 3 * dim_K7 := by native_decide
 
 -- =============================================================================
--- PHASE 3 PINN TRAINING METRICS (numerical constants)
+-- PINN TRAINING METRICS (numerical constants)
 -- =============================================================================
 
 /-!
-## Phase 3 PINN metrics (v6-v20)
+## PINN metrics (v6-v20)
 
 The PINN training descended g₂_self from 3.86 (v6) to 2.251 (v20)
 over 19 training runs and ~64,000 epochs.
@@ -287,23 +287,23 @@ Key diagnostic values at v20:
 - hol_rank = 21 (target: 14)
 
 The AS ratio ~4.0 indicates the curvature generates all of so(7),
-confirming that explicit Ambrose-Singer loss is needed for Phase 4.
+confirming that an explicit Ambrose-Singer loss is needed going forward.
 -/
 
-/-- Phase 3 best g₂_self loss (×1000 for integer arithmetic): 2251 -/
+/-- Best g₂_self loss (×1000 for integer arithmetic): 2251 -/
 def phase3_g2_self_x1000 : ℕ := 2251
 
-/-- Phase 3 initial g₂_self loss (×1000): 3860 -/
+/-- Initial g₂_self loss (×1000): 3860 -/
 def phase3_g2_self_initial_x1000 : ℕ := 3860
 
 /-- Improvement factor numerator (×1000): 3860 - 2251 = 1609 -/
 theorem phase3_improvement : phase3_g2_self_initial_x1000 - phase3_g2_self_x1000 = 1609 := by
   native_decide
 
-/-- Phase 3 total training runs -/
+/-- Total training runs -/
 def phase3_total_runs : ℕ := 20
 
-/-- Phase 3 approximate total epochs -/
+/-- Approximate total epochs -/
 def phase3_total_epochs : ℕ := 64000
 
 -- =============================================================================

GIFT/Foundations/Analysis/HarmonicForms.lean

@@ -11,8 +11,8 @@ Harmonic forms are isomorphic to de Rham cohomology.
 |-------|----------|--------|
 | `K7_hodge_data` | — | **FUSED v3.3.42** into `K7_analysis_data` |
 | `K7_harmonic_basis` | — | **FUSED v3.3.42** into `K7_analysis_data` |
-| `K7_analysis_data` | C: Geometric structure | **NEW** bundled K7 Hodge + harmonic data |
-| `hodge_isomorphism` | B: Standard result | Hodge (1941) |
+| `K7_analysis_data` | geometric structure | **NEW** bundled K7 Hodge + harmonic data |
+| `hodge_isomorphism` | standard result | Hodge (1941) |
 
 Version: 3.3.42 (axiom consolidation: K7_hodge_data + K7_harmonic_basis → K7_analysis_data)
 -/
@@ -101,7 +101,7 @@ Constructive witness: zero Laplacian (Δ=0, all forms harmonic), standard
 inner product (Σᵢ ωᵢηᵢ), standard basis vectors (Pi.single i 1).
 
 **Axiom consolidation (v3.3.42):** Replaces `K7_hodge_data` + `K7_harmonic_basis` (9→1).
-**Phase 3 (v4.0.12):** Added spectral fields — absorbs K7_exists axiom (→ noncomputable def).
+**v4.0.12:** Added spectral fields — absorbs K7_exists axiom (→ noncomputable def).
 **Eliminated (v3.4.9):** axiom → noncomputable def via constructive witness. -/
 -- Constructive witness components (private, not exported)
 private def k7_bundle : DifferentialFormBundle K7 where

GIFT/Foundations/Analysis/K7Orthonormality.lean

@@ -18,7 +18,7 @@ These verify:
   - The L2 inner product is well-defined and non-degenerate
   - Yukawa coupling normalization Y_ijk = int omega_i ^ omega_j ^ eta_k is well-posed
 
-All constants below are **Category F (Numerically verified)** — values from
+All constants below are **numerically verified** — values from
 `private/notebooks/k7_orthonormality_results.json`. The arithmetic on these
 constants is proven, not axiomatized.
 
@@ -67,7 +67,7 @@ Computed from 220,000-point Monte Carlo integration using:
 
 /-- G_K3(22) condition number numerator (×10000): cond = 1.0523.
 
-**Category F**: Numerically verified, eigenvalue range [0.9739, 1.0248]. -/
+**Numerically verified**, eigenvalue range [0.9739, 1.0248]. -/
 def G_K3_cond_num : ℕ := 10523
 
 /-- G_K3(22) condition number denominator -/
@@ -81,7 +81,7 @@ theorem G_K3_cond_gt_one : G_K3_cond_num > G_K3_cond_den := by native_decide
 
 /-- G_K3(22) off-diagonal (normalized) numerator (×10000): max = 0.01180.
 
-**Category F**: max|G_norm - I| over off-diagonal entries. -/
+**Numerically verified**: max|G_norm - I| over off-diagonal entries. -/
 def G_K3_offdiag_num : ℕ := 118
 
 /-- G_K3(22) off-diagonal (normalized) denominator -/
@@ -92,7 +92,7 @@ theorem G_K3_22_near_orthonormal : G_K3_offdiag_num < 150 := by native_decide
 
 /-- G_K3(22) min eigenvalue (×10000): 9739.
 
-**Category F**: Positive definiteness verified (min eigenvalue = 0.9739). -/
+**Numerically verified**: Positive definiteness verified (min eigenvalue = 0.9739). -/
 def G_K3_min_eval_num : ℕ := 9739
 
 /-- G_K3(22) min eigenvalue denominator -/
@@ -113,15 +113,15 @@ R11 = R22 ≈ 0.7504, R12 ≈ 0.3752.
 
 /-- Radial overlap R11 (×10000): R11 = 0.7504.
 
-**Category F**: Trapezoidal integration of f₁²·p over s-grid. -/
+**Numerically verified**: Trapezoidal integration of f₁²·p over s-grid. -/
 def R11_num : ℕ := 7504
 
 /-- Radial overlap denominator -/
 def R11_den : ℕ := 10000
 
 /-- G_K7(22) condition number (×10000): cond = 1.0471.
 
-**Category F**: Eigenvalue range [0.7327, 0.7672]. -/
+**Numerically verified**: Eigenvalue range [0.7327, 0.7672]. -/
 def G_K7_cond_num : ℕ := 10471
 
 /-- G_K7(22) condition number denominator -/
@@ -132,7 +132,7 @@ theorem G_K7_22_well_conditioned : G_K7_cond_num < 10500 := by native_decide
 
 /-- G_K7(22) min eigenvalue (×10000): 7327.
 
-**Category F**: min eigenvalue = 0.7327. -/
+**Numerically verified**: min eigenvalue = 0.7327. -/
 def G_K7_min_eval_num : ℕ := 7327
 
 /-- G_K7(22) positive definite: min eigenvalue > 0.73 -/
@@ -150,7 +150,7 @@ range from 1.65 to 12.57, giving condition number ≈ 7.66.
 
 /-- G_35 condition number (×10000): cond = 7.6621.
 
-**Category F**: Eigenvalue range [1.647, 12.622]. -/
+**Numerically verified**: Eigenvalue range [1.647, 12.622]. -/
 def G_35_cond_num : ℕ := 76621
 
 /-- G_35 condition number denominator -/
@@ -161,7 +161,7 @@ theorem G_35_well_conditioned : G_35_cond_num < 80000 := by native_decide
 
 /-- G_35 min eigenvalue (×1000): 1647.
 
-**Category F**: min eigenvalue = 1.647. -/
+**Numerically verified**: min eigenvalue = 1.647. -/
 def G_35_min_eval_num : ℕ := 1647
 
 /-- G_35 positive definite: min eigenvalue > 1.6 -/
@@ -179,15 +179,15 @@ S_θ ≈ S_ψ ≈ 6.127, S_cross ≈ -6.5 × 10⁻⁵.
 
 /-- S_theta (×1000): S_θ = 6.127.
 
-**Category F**: ∫ g^{θθ} √det(g) ds. -/
+**Numerically verified**: ∫ g^{θθ} √det(g) ds. -/
 def S_theta_num : ℕ := 6127
 
 /-- S_theta denominator -/
 def S_theta_den : ℕ := 1000
 
 /-- Cross-block max (×10^7): |S_cross| · max|G_K3| ≈ 653.
 
-**Category F**: max = 6.53 × 10⁻⁵. -/
+**Numerically verified**: max = 6.53 × 10⁻⁵. -/
 def G_77_cross_num : ℕ := 653
 
 /-- Cross-block max denominator -/
@@ -207,7 +207,7 @@ an orthonormalization matrix T = L⁻ᵀ such that TᵀGT = I.
 
 All four matrices pass with residual < 10⁻¹⁵.
 
-**Category F**: Residuals: 3.3e-16, 3.3e-16, 4.4e-16, 4.4e-16.
+**Numerically verified**: Residuals: 3.3e-16, 3.3e-16, 4.4e-16, 4.4e-16.
 -/
 
 /-- Gram-Schmidt residual exponent: all residuals < 10⁻¹⁵ -/