v0.6: TAF Card hero+accordion UI + γ_check + Lean+Mathlib badges

- Hero strip (arch class + meta + 3 pills: count breakdown, γ headline, Anti-Ising) + 4 accordions: Recipes, Diagnostics, Verification, Provenance
- New js/gamma_check.js: Padé closed-form + classifyRegime (normal/fraud/compressed/overpade/swa), browser-only
- New js/lean_badges.js + data/lean_status.json: manifest of 37 theorems in 7 groups + 1 substantive finding (V_derivative_ne_RG_beta factor-2). Sortable theorem table, hero Anti-Ising pill links to Taf/Identities.lean#L188 (beta_chi_closure)
- Verdict aggregation: count breakdown (✅ · ⚠ · ❌) replaces worst-of-N confusion when orthogonal recipes disagree
- ⓘ tooltips inline: hero pills (3), Profile form params (6), Diagnostics keys (6), γ_check results (5)
- Help v0.6 section: TAF Card layout + 5 regime use cases + Cardy ΔH + concrete Lean reverify command + 37/1 count, all 4 langs
- i18n EN/ES/FR/ZH parity: 295+ keys per lang, 0 missing
- gamma_check classifier verified 5/5 regimes via headless Chrome simulation

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

data/lean_status.json

@@ -0,0 +1,506 @@
+{
+  "schema_version": 1,
+  "generated_at": "2026-05-06",
+  "lean_repo": {
+    "name": "karlesmarin/lean-taf",
+    "url": "https://github.com/karlesmarin/lean-taf",
+    "default_branch": "master",
+    "commit": "25c77fd2180b8e0d6bc9a634de36667f11597cae",
+    "commit_short": "25c77fd",
+    "commit_date": "2026-05-05T22:50:58+02:00",
+    "build_status": "ok",
+    "build_jobs": 1973,
+    "compile_time_seconds": 5,
+    "lean_toolchain": "leanprover/lean4:v4.30.0-rc2",
+    "mathlib_imports": [
+      "Mathlib.Data.Real.Basic",
+      "Mathlib.Analysis.SpecialFunctions.Pow.Real",
+      "Mathlib.Analysis.Calculus.Deriv.Pow",
+      "Mathlib.Analysis.Calculus.Deriv.Add",
+      "Mathlib.Tactic"
+    ],
+    "verification_report": "tmp/FORMULAS_LEAN_VERIFICATION_2026-05-05.md"
+  },
+  "summary": {
+    "theorems_total": 37,
+    "lean_verified": 37,
+    "lean_rejected": 0,
+    "skipped_sorry": 0,
+    "substantive_findings": 1
+  },
+  "findings": [
+    {
+      "id": "F1",
+      "title": "V/β factor-of-2 inconsistency in paper formula tables",
+      "severity": "substantive",
+      "detected_by": "V_derivative_ne_RG_beta",
+      "fixed_by": ["V_correct_derivative", "V_correct_matches_RG_beta"],
+      "summary": "Paper tables jointly state V(γ)=γ−γ³/3 + β=−V' + β(γ)=−(1−γ²)/2. Lean proves these inconsistent ∀γ∉{−1,+1} (residual factor 2). Corrected V_correct(γ)=γ/2−γ³/6 *does* integrate to the RG β.",
+      "recommendation": "Restate V as γ/2 − γ³/6, or rescale β to −(1−γ²), or document the Lagrangian-normalization convention."
+    }
+  ],
+  "groups": [
+    {
+      "id": "pade",
+      "title": "Padé approximant identities",
+      "theorems": [
+        {
+          "name": "pade_22_minus_pade_11",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 31,
+          "claim": "Padé[2,2](z) − Padé[1,1](z) = 2z³ / ((z+2)(z²+6z+12))",
+          "preconditions": ["z + 2 ≠ 0", "z² + 6z + 12 ≠ 0"],
+          "tactic": "field_simp; ring",
+          "status": "ok",
+          "tags": ["pade", "exact"],
+          "source": { "doc": "FORMULA_TABLE.md", "line": 13, "label": "G-15 ★ EXACT" }
+        },
+        {
+          "name": "one_minus_pade_11",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 50,
+          "claim": "1 − (2−z)/(2+z) = 2z/(2+z)",
+          "preconditions": ["2 + z ≠ 0"],
+          "tactic": "field_simp; ring",
+          "status": "ok",
+          "tags": ["pade", "exact"],
+          "source": { "doc": "FORMULAS_TOOLKIT.md", "section": "§4.4", "line": 572, "label": "★ EXACT" }
+        },
+        {
+          "name": "pade_z_substitution",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 207,
+          "claim": "γ_Padé canonical form: with z = T√2/θ, (2−z)/(2+z) = (2θ − T√2) / (2θ + T√2)",
+          "preconditions": ["θ ≠ 0", "2θ + T√2 ≠ 0"],
+          "tactic": "field_simp",
+          "status": "ok",
+          "tags": ["pade", "exact", "core"],
+          "source": { "doc": "FORMULAS_TOOLKIT.md", "section": "§4.1", "line": 456, "label": "★ EXACT" }
+        },
+        {
+          "name": "theta_eff_pade",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 61,
+          "claim": "θ_eff_Padé: T√2 / (1 − γ_Padé(T√2/θ)) = θ + T/√2",
+          "preconditions": ["θ ≠ 0", "T ≠ 0", "2θ + T√2 ≠ 0"],
+          "tactic": "field_simp; ring_nf + manual rewrite √2³ = √2·2",
+          "status": "ok",
+          "tags": ["pade", "exact", "core"],
+          "source": { "doc": "FORMULAS_TOOLKIT.md", "line": 572, "label": "★ EXACT" }
+        },
+        {
+          "name": "pade_saturation_leading_coefficient",
+          "kind": "theorem",
+          "file": "Taf/AmGmPade.lean",
+          "line": 100,
+          "claim": "Padé[2,2] − Padé[1,1] leading coefficient at z=0 is 1/12",
+          "tactic": "norm_num + field_simp",
+          "status": "ok",
+          "tags": ["pade", "audit_finding"],
+          "source": { "doc": "FORMULA_TABLE.md", "label": "★ EXACT (Padé saturation, paper §sec:gamma_decomposition)" }
+        }
+      ]
+    },
+    {
+      "id": "rg_flow",
+      "title": "RG flow / β-function (with V/β factor-2 finding)",
+      "theorems": [
+        {
+          "name": "logistic_to_beta_algebraic",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 91,
+          "claim": "Substitution x = (1−γ)/2 ⇒ x(1−x) = (1−γ²)/4",
+          "tactic": "ring",
+          "status": "ok",
+          "tags": ["rg", "exact"],
+          "source": { "doc": "FORMULA_TABLE.md", "line": 90, "label": "§23 ✅ ALGEBRAIC EXACT" }
+        },
+        {
+          "name": "V_derivative",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 111,
+          "claim": "d/dγ (γ − γ³/3) = 1 − γ²",
+          "tactic": "HasDerivAt chain (id, pow, div_const, sub)",
+          "status": "ok",
+          "tags": ["rg", "exact"],
+          "source": { "doc": "FORMULA_TABLE.md", "line": 91, "label": "§23 ✅ ALGEBRAIC EXACT" }
+        },
+        {
+          "name": "V_derivative_ne_RG_beta",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 122,
+          "claim": "−V'(γ) ≠ −(1 − γ²)/2 for all γ ∉ {−1, +1}",
+          "preconditions": ["γ ≠ 1", "γ ≠ −1"],
+          "tactic": "linarith after expanding V'(γ) = 1 − γ²",
+          "status": "ok",
+          "tags": ["rg", "audit_finding", "substantive"],
+          "source": { "doc": "FORMULAS_TOOLKIT.md", "section": "§19", "line": 191, "label": "FINDING — factor-2 inconsistency" }
+        },
+        {
+          "name": "V_correct_derivative",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 238,
+          "claim": "d/dγ (γ/2 − γ³/6) = (1 − γ²)/2",
+          "tactic": "HasDerivAt chain",
+          "status": "ok",
+          "tags": ["rg", "fix"],
+          "source": { "doc": "FORMULAS_LEAN_VERIFICATION_2026-05-05.md", "label": "Corrected V" }
+        },
+        {
+          "name": "V_correct_matches_RG_beta",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 256,
+          "claim": "−d/dγ (γ/2 − γ³/6) = −(1 − γ²)/2 = β(γ)",
+          "tactic": "rw [V_correct_derivative]; ring",
+          "status": "ok",
+          "tags": ["rg", "fix"],
+          "source": { "doc": "FORMULAS_LEAN_VERIFICATION_2026-05-05.md", "label": "V_correct integrates to RG β" }
+        },
+        {
+          "name": "trajectory_sign_inversion",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 344,
+          "claim": "Trajectory tanh sign convention check (paper used +t/2; correct is −t/2 from dγ/dt = −(1−γ²)/2)",
+          "tactic": "deriv computation + sign analysis",
+          "status": "ok",
+          "tags": ["rg", "audit_finding"]
+        }
+      ]
+    },
+    {
+      "id": "cayley",
+      "title": "Cayley fixed-point + χ susceptibility roots",
+      "theorems": [
+        {
+          "name": "cayley_fixed_point_iff",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 139,
+          "claim": "−(z − 2)/(z + 2) = z ⟺ z² + 3z − 2 = 0",
+          "preconditions": ["z + 2 ≠ 0"],
+          "tactic": "nlinarith after clearing denominator",
+          "status": "ok",
+          "tags": ["cayley"],
+          "source": { "doc": "FORMULAS_TOOLKIT.md", "line": 173 }
+        },
+        {
+          "name": "cayley_root",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 151,
+          "claim": "z* = (√17 − 3)/2 satisfies z*² + 3z* − 2 = 0",
+          "tactic": "explicit Real.sq_sqrt expansion",
+          "status": "ok",
+          "tags": ["cayley", "exact"],
+          "source": { "doc": "FORMULAS_TOOLKIT.md", "line": 174, "label": "Physical fixed point z*" }
+        },
+        {
+          "name": "chi_root",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 170,
+          "claim": "χ = (5 + √17)/4 satisfies 2χ² − 5χ + 1 = 0",
+          "tactic": "explicit Real.sq_sqrt expansion",
+          "status": "ok",
+          "tags": ["cayley", "exact"],
+          "source": { "doc": "FORMULA_TABLE.md", "line": 92, "label": "§26 ✅ ALGEBRAIC EXACT" }
+        },
+        {
+          "name": "cayley_floquet_form_equivalence",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 310,
+          "claim": "−4(√17+1)/(5√17+13) = (√17 − 9)/8  (equivalent forms; both ≈ −0.6096)",
+          "tactic": "nlinarith via div_eq_div_iff",
+          "status": "ok",
+          "tags": ["cayley", "exact"],
+          "source": { "doc": "FORMULAS_TOOLKIT.md", "line": 177 }
+        },
+        {
+          "name": "cayley_floquet_stable",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 290,
+          "claim": "|(√17 − 9)/8| < 1  (stable attractor, |μ| < 1)",
+          "tactic": "abs_of_neg + linarith with √17 < 5",
+          "status": "ok",
+          "tags": ["cayley", "stability"],
+          "source": { "doc": "FORMULAS_TOOLKIT.md", "line": 178, "label": "STABLE attractor" }
+        }
+      ]
+    },
+    {
+      "id": "dsage",
+      "title": "D-SAGE algebraic identities (Sage Groebner + Lean)",
+      "theorems": [
+        {
+          "name": "D_SAGE_1",
+          "kind": "theorem",
+          "file": "Taf/Identities.lean",
+          "line": 47,
+          "claim": "2η² + η·γ_χ + 1 = 0  (★★ CORE quadratic identity)",
+          "preconditions": ["γ ≠ 1"],
+          "tactic": "field_simp; ring",
+          "status": "ok",
+          "tags": ["dsage", "core"],
+          "source": { "doc": "analysis/sage_recursive_sweep_2026-04-30.sage", "label": "Groebner-discovered" }
+        },
+        {
+          "name": "D_SAGE_2",
+          "kind": "theorem",
+          "file": "Taf/Identities.lean",
+          "line": 56,
+          "claim": "β·χ = −1  (Phase A signature, Anti-Ising marker)",
+          "preconditions": ["γ ≠ 1"],
+          "tactic": "field_simp; ring",
+          "status": "ok",
+          "tags": ["dsage", "anti_ising", "core"]
+        },
+        {
+          "name": "D_SAGE_4",
+          "kind": "theorem",
+          "file": "Taf/Identities.lean",
+          "line": 65,
+          "claim": "α + χ = 2  (Josephson hyperscaling consequence)",
+          "preconditions": ["γ ≠ 1"],
+          "tactic": "field_simp; ring",
+          "status": "ok",
+          "tags": ["dsage"]
+        },
+        {
+          "name": "D_SAGE_5",
+          "kind": "theorem",
+          "file": "Taf/Identities.lean",
+          "line": 74,
+          "claim": "α + γ_χ = 2(2 − γ)  (linear sum identity)",
+          "preconditions": ["γ ≠ 1"],
+          "tactic": "field_simp; ring",
+          "status": "ok",
+          "tags": ["dsage"]
+        },
+        {
+          "name": "D_SAGE_7",
+          "kind": "theorem",
+          "file": "Taf/Identities.lean",
+          "line": 182,
+          "claim": "c · |ν_imprint| · 2π = 3  (CFT central charge × imprint slope dimensional closure)",
+          "tactic": "ring",
+          "status": "ok",
+          "tags": ["dsage", "imprint"]
+        },
+        {
+          "name": "rushbrooke_tautology",
+          "kind": "theorem",
+          "file": "Taf/Identities.lean",
+          "line": 92,
+          "claim": "2β + γ_χ = ν · d  at d=1  (Rushbrooke hyperscaling, holds as TAUTOLOGY in TAF since γ_χ defined to satisfy)",
+          "preconditions": ["γ ≠ 1"],
+          "tactic": "field_simp; ring",
+          "status": "ok",
+          "tags": ["dsage", "tautology"]
+        },
+        {
+          "name": "josephson_tautology",
+          "kind": "theorem",
+          "file": "Taf/Identities.lean",
+          "line": 101,
+          "claim": "2 − α = ν · d  at d=1  (Josephson hyperscaling, TAUTOLOGY in TAF)",
+          "preconditions": ["γ ≠ 1"],
+          "tactic": "field_simp; ring",
+          "status": "ok",
+          "tags": ["dsage", "tautology"]
+        },
+        {
+          "name": "fisher_zero_iff",
+          "kind": "theorem",
+          "file": "Taf/Identities.lean",
+          "line": 119,
+          "claim": "Fisher relation γ_χ = (2 − η)·ν holds iff residual γ(2γ−3)/(1−γ) = 0  (i.e. NEVER in Phase A)",
+          "preconditions": ["γ ≠ 1"],
+          "tactic": "field_simp; ring",
+          "status": "ok",
+          "tags": ["dsage", "independent"]
+        },
+        {
+          "name": "beta_chi_closure",
+          "kind": "theorem",
+          "file": "Taf/Identities.lean",
+          "line": 188,
+          "claim": "β · χ = −1  (Anti-Ising β=γ−1<0 closure, machine-verified)",
+          "preconditions": ["γ ≠ 1"],
+          "tactic": "field_simp; ring",
+          "status": "ok",
+          "tags": ["dsage", "anti_ising", "core"],
+          "ui_badge": "anti_ising"
+        },
+        {
+          "name": "nu_beta_id",
+          "kind": "theorem",
+          "file": "Taf/Identities.lean",
+          "line": 197,
+          "claim": "ν · β = −1  in Phase A (variant of D-SAGE-2)",
+          "preconditions": ["γ ≠ 1"],
+          "tactic": "field_simp; ring",
+          "status": "ok",
+          "tags": ["dsage", "anti_ising"]
+        }
+      ]
+    },
+    {
+      "id": "audit_findings",
+      "title": "Paper-1 audit findings (refutations + erratums)",
+      "theorems": [
+        {
+          "name": "eta_2gamma_residual",
+          "kind": "theorem",
+          "file": "Taf/Identities.lean",
+          "line": 148,
+          "claim": "Paper 1 claim η = 2γ has residual (−4γ³ + 5γ + 1)/(1−γ) — NOT identically zero",
+          "preconditions": ["γ ≠ 1"],
+          "tactic": "field_simp; ring",
+          "status": "ok",
+          "tags": ["audit_finding", "refutation"]
+        },
+        {
+          "name": "eta_2gamma_fails_phase_A",
+          "kind": "theorem",
+          "file": "Taf/Identities.lean",
+          "line": 156,
+          "claim": "η = 2γ fails throughout Phase A (residual > 0 ∀γ ∈ (0,1))  — paper 1 claim formally refuted",
+          "preconditions": ["0 < γ", "γ < 1"],
+          "tactic": "nlinarith with Phase A bounds",
+          "status": "ok",
+          "tags": ["audit_finding", "refutation", "substantive"]
+        },
+        {
+          "name": "AM_GM_gamma_chi",
+          "kind": "theorem",
+          "file": "Taf/AmGmPade.lean",
+          "line": 45,
+          "claim": "γ_χ = 1/(1−γ) + 2(1−γ) ≥ 2√2 with minimum at γ = 1 − 1/√2 ≈ 0.293",
+          "preconditions": ["0 < γ", "γ < 1"],
+          "tactic": "AM-GM on positive reals",
+          "status": "ok",
+          "tags": ["audit_finding", "amgm"]
+        }
+      ]
+    },
+    {
+      "id": "erratum_cv",
+      "title": "C_V coefficient erratum (paper §5.2 — 1/4 → 1/12)",
+      "theorems": [
+        {
+          "name": "log_one_plus_x_coefficient_24",
+          "kind": "theorem",
+          "file": "Taf/ErratumCV.lean",
+          "line": 55,
+          "claim": "log(1+x) Taylor coefficient at x²/2: 1/24 in cumulant expansion",
+          "tactic": "norm_num",
+          "status": "ok",
+          "tags": ["erratum"]
+        },
+        {
+          "name": "cv_corrected_at_hagedorn",
+          "kind": "theorem",
+          "file": "Taf/ErratumCV.lean",
+          "line": 93,
+          "claim": "C_V at Hagedorn limit = (log L)²/12  (CORRECTED — paper §5.2 had 1/4)",
+          "tactic": "field_simp; ring after cumulant identity",
+          "status": "ok",
+          "tags": ["erratum", "core"]
+        },
+        {
+          "name": "original_is_three_times_corrected",
+          "kind": "theorem",
+          "file": "Taf/ErratumCV.lean",
+          "line": 103,
+          "claim": "Paper's original (log L)²/4 = 3 × corrected (log L)²/12  (factor-3 quantification)",
+          "tactic": "ring",
+          "status": "ok",
+          "tags": ["erratum"]
+        },
+        {
+          "name": "original_ne_corrected",
+          "kind": "theorem",
+          "file": "Taf/ErratumCV.lean",
+          "line": 107,
+          "claim": "Original ≠ corrected for L ≠ 0 (formal statement of disagreement)",
+          "preconditions": ["L ≠ 0"],
+          "tactic": "linarith after factor-3 expansion",
+          "status": "ok",
+          "tags": ["erratum"]
+        },
+        {
+          "name": "cv_hagedorn_correct_coefficient",
+          "kind": "theorem",
+          "file": "Taf/CvHagedornCorrection.lean",
+          "line": 51,
+          "claim": "∫(log x)²/x dx from 1 to N = (log N)³ / 3  ⟹ C_V coefficient 1/12 (not 1/4)",
+          "preconditions": ["1 ≤ N"],
+          "tactic": "integral derivation via log_sq_half + integral_log_div_x",
+          "status": "ok",
+          "tags": ["erratum", "integral"]
+        }
+      ]
+    },
+    {
+      "id": "misc",
+      "title": "Misc identities + dimensional checks",
+      "theorems": [
+        {
+          "name": "rope_beta_form",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 189,
+          "claim": "RoPE β-form: √3/6 = 1/√12",
+          "tactic": "field_simp; nlinarith with √12 = 2√3",
+          "status": "ok",
+          "tags": ["misc"],
+          "source": { "doc": "FORMULAS_TOOLKIT.md", "line": 411 }
+        },
+        {
+          "name": "cft_nu_identity",
+          "kind": "theorem",
+          "file": "Taf/RGFlow.lean",
+          "line": 220,
+          "claim": "ν · (1 − γ) = 1  for ν = 1/(1−γ)",
+          "preconditions": ["1 − γ ≠ 0"],
+          "tactic": "field_simp",
+          "status": "ok",
+          "tags": ["misc", "cft"],
+          "source": { "doc": "FORMULAS_TOOLKIT.md", "section": "§15", "line": 265 }
+        },
+        {
+          "name": "D_14_nu_imprint",
+          "kind": "theorem",
+          "file": "Taf/Identities.lean",
+          "line": 176,
+          "claim": "ν_imprint × 2π = −1  (RoPE rotation period × imprint slope dimensional check)",
+          "preconditions": ["π > 0"],
+          "tactic": "ring",
+          "status": "ok",
+          "tags": ["imprint", "misc"]
+        }
+      ]
+    }
+  ],
+  "ui_bindings": {
+    "anti_ising_pill":          "beta_chi_closure",
+    "gamma_pade_panel":         "pade_z_substitution",
+    "theta_eff_panel":          "theta_eff_pade",
+    "cardy_delta_h":            null,
+    "algebraic_consistency_check": ["D_SAGE_1", "D_SAGE_2", "D_SAGE_4", "D_SAGE_5", "rushbrooke_tautology", "josephson_tautology", "beta_chi_closure", "nu_beta_id"],
+    "audit_findings_section":   ["V_derivative_ne_RG_beta", "eta_2gamma_fails_phase_A", "cv_corrected_at_hagedorn", "trajectory_sign_inversion"],
+    "padé_saturation_diagnose": "pade_saturation_leading_coefficient"
+  }
+}

index.html

@@ -162,6 +162,31 @@
 
       <p><strong data-i18n="v05.repro.label">Reproducibility</strong> — <span data-i18n="v05.repro.desc">All 15 theorems machine-proof in Lean Mathlib4 (1973 jobs build success). Sage script: <code>analysis/sage_recursive_sweep_2026-04-30.sage</code>. Lean code: <code>lean_taf/taf/Taf/Identities.lean</code>.</span></p>
 
+      <h3 style="margin-top: 1.5em;" data-i18n="help.v06.title">🆕 v0.6 — γ predicted-vs-observed + Cardy ΔH + Lean badges</h3>
+      <p style="opacity: 0.85;" data-i18n="help.v06.intro"><em>v0.6 (2026-05-06): three new diagnostics live in the TAF Card under <strong>🔬 Diagnostics</strong>. All run in your browser; γ_observed comes from the Diagnose CLI on real weights.</em></p>
+
+      <p><strong data-i18n="help.v06.layout.title">TAF Card layout (new in v0.6)</strong></p>
+      <p data-i18n="help.v06.layout.body">After clicking <strong>🚀 Generate full profile</strong> the card shows: a <strong>hero strip</strong> on top (architecture class + meta + 3 pills: aggregate verdict ✅/⚠/❌, γ headline, 🧲 Anti-Ising if Phase A) and four <strong>expandable sections</strong>: <strong>📋 Recipes</strong> (open by default — verdict per dimension), <strong>🔬 Diagnostics</strong> (key numbers, γ predicted vs observed, what-if explorer), <strong>✓ Verification</strong> (Sage+Lean algebraic consistency, falsification F1-F23), <strong>📂 Provenance &amp; share</strong> (calibration audit + JSON download / share link / registry submit). Click any header to expand. Every variable has an inline <strong>ⓘ</strong> tooltip.</p>
+
+      <p><strong data-i18n="help.v06.gamma_check.title">γ predicted vs observed</strong></p>
+      <p data-i18n="help.v06.gamma_check.body">Enter the empirically-measured γ from your model and the tool computes <strong>η = θ_eff_obs / θ_eff_Padé</strong> and classifies into one of 5 regimes:</p>
+      <ul style="font-size: 0.92em;">
+        <li data-i18n="help.v06.case.normal"><strong>Normal</strong> (η ∈ [0.85, 1.15]) — model uses its full nominal context. <em>Use case</em>: validate a new release before adopting it.</li>
+        <li data-i18n="help.v06.case.fraud"><strong>Fraud</strong> (η &lt; 0.01) — nominal θ inflated; model behaves as if θ ≪ advertised. <em>Use case</em>: detect YaRN/marketing inflation (CodeLlama / Mistral-Nemo pattern).</li>
+        <li data-i18n="help.v06.case.compressed"><strong>Compressed</strong> (η &lt; 0.5) — context compressed; model attends shorter than nominal θ. <em>Use case</em>: spot RLHF/instruction-tuning compression (LLaMA-2 pattern).</li>
+        <li data-i18n="help.v06.case.overpade"><strong>Over-Padé</strong> (η &gt; 1.5) — model attends farther than Padé predicts. <em>Use case</em>: identify Lerch-corrected regime or undertrained early checkpoints (pythia-1b pattern).</li>
+        <li data-i18n="help.v06.case.swa"><strong>SWA random-corpus</strong> (γ_obs &gt; 1.05 with random_corpus=Yes) — sliding-window attention signature. <em>Use case</em>: confirm Mistral / Gemma SWA on random tokens.</li>
+      </ul>
+
+      <p><strong data-i18n="help.v06.cardy.title">Cardy ΔH diagnostic</strong></p>
+      <p data-i18n="help.v06.cardy.body"><strong>ΔH_Cardy = log(θ_eff_obs / θ_nominal)</strong>. Entropy shift between observed effective θ and nominal θ. Strong negative = compression entropy; near zero = nominal match. Complements η for borderline cases.</p>
+
+      <p><strong data-i18n="help.v06.lean.title">Lean + Mathlib verification badges</strong></p>
+      <p data-i18n="help.v06.lean.body">TAF identities (Anti-Ising, D-SAGE-1 quadratic, Padé z-substitution, etc.) are formally machine-proven in Lean Mathlib4. Source: <a href="https://github.com/karlesmarin/lean-taf" target="_blank">github.com/karlesmarin/lean-taf</a>. Anyone can clone + <code>lake build</code> to re-verify. The 🧲 Anti-Ising pill in the hero strip is one such badge.</p>
+
+      <p><strong data-i18n="help.v06.glossary.title">Variable glossary (also embedded in TAF Card)</strong></p>
+      <p data-i18n="help.v06.glossary.body">Every variable in the TAF Card has an inline ⓘ tooltip. The complete list: γ, γ_Padé, γ_decomposed, γ_observed, θ, θ_eff_obs, θ_eff_Padé, η, ΔH_Cardy, χ, d_horizon, L_NIAH, KV memory, regime. Hover any ⓘ for the definition + paper section.</p>
+
       <h3 data-i18n="help.add_models.title">Adding new models (3 ways)</h3>
       <ul>
         <li data-i18n="help.add_models.preset"><strong>Preset list</strong>: 11 popular models curated. Just select from dropdown.</li>
@@ -292,27 +317,27 @@
           <input type="number" id="profile-T_eval" value="32000" />
         </div>
         <div class="form-field">
-          <label data-i18n="param.n_attn">n_attention_heads</label>
+          <label><span data-i18n="param.n_attn">n_attention_heads</span> <span class="info"><span class="tooltip" data-i18n="param.n_attn.tip">Number of attention heads per layer. From <code>num_attention_heads</code>.</span></span></label>
           <input type="number" id="profile-n_attn" value="32" />
         </div>
         <div class="form-field">
-          <label data-i18n="param.n_kv">n_kv_heads</label>
+          <label><span data-i18n="param.n_kv">n_kv_heads</span> <span class="info"><span class="tooltip" data-i18n="param.n_kv.tip">KV heads. If &lt; n_attention_heads → GQA (Grouped Query Attention). Reduces KV memory but pushes γ toward Hagedorn.</span></span></label>
           <input type="number" id="profile-n_kv" value="8" />
         </div>
         <div class="form-field">
-          <label data-i18n="param.d_head">head_dim</label>
+          <label><span data-i18n="param.d_head">head_dim</span> <span class="info"><span class="tooltip" data-i18n="param.d_head.tip">Per-head dimension. Typical 64, 96, 128. From <code>head_dim</code> or <code>hidden_size / num_attention_heads</code>.</span></span></label>
           <input type="number" id="profile-d_head" value="128" />
         </div>
         <div class="form-field">
-          <label data-i18n="param.n_layers">n_layers</label>
+          <label><span data-i18n="param.n_layers">n_layers</span> <span class="info"><span class="tooltip" data-i18n="param.n_layers.tip">Number of transformer blocks. From <code>num_hidden_layers</code>.</span></span></label>
           <input type="number" id="profile-n_layers" value="32" />
         </div>
         <div class="form-field">
-          <label data-i18n="param.n_params">n_params (e.g. 8e9)</label>
+          <label><span data-i18n="param.n_params">n_params (e.g. 8e9)</span> <span class="info"><span class="tooltip" data-i18n="param.n_params.tip">Total parameter count. Threshold ~400M for induction-head emergence. Affects KV memory and budget recipes.</span></span></label>
           <input type="text" id="profile-n_params" value="8e9" />
         </div>
         <div class="form-field">
-          <label data-i18n="param.has_swa">Has SWA?</label>
+          <label><span data-i18n="param.has_swa">Has SWA?</span> <span class="info"><span class="tooltip" data-i18n="param.has_swa.tip">Sliding Window Attention. <code>true</code> for Mistral, gemma-2, phi-3. Calibration audit (v0.5.3) disabled the historical δ_SWA correction (n=1 fit).</span></span></label>
           <select id="profile-has_swa">
             <option value="false" selected data-i18n="common.no">No</option>
             <option value="true" data-i18n="common.yes">Yes</option>

js/gamma_check.js

@@ -0,0 +1,70 @@
+// γ predicted-vs-observed diagnostic — Padé closed-form + regime classifier.
+// Pure functions ported from tools/taf/diagnose/gamma_check.py.
+// All math is browser-only (no backend, no Python).
+
+const SQRT2 = Math.SQRT2;
+
+export function gammaPade(theta, T) {
+  if (!Number.isFinite(theta) || theta <= 0 || !Number.isFinite(T) || T < 0) return NaN;
+  const z = (T * SQRT2) / theta;
+  return (2 - z) / (2 + z);
+}
+
+export function thetaEffPade(theta, T) {
+  if (!Number.isFinite(theta) || !Number.isFinite(T)) return NaN;
+  return theta + T / SQRT2;
+}
+
+export function thetaEffObserved(gObs, T) {
+  if (!Number.isFinite(gObs) || !Number.isFinite(T) || T < 0) return NaN;
+  if (Math.abs(1 - gObs) < 1e-12) return Infinity;
+  return (T * SQRT2) / (1 - gObs);
+}
+
+export function efficiency(thEffObs, thEffPade) {
+  if (!Number.isFinite(thEffObs) || !Number.isFinite(thEffPade) || thEffPade === 0) return NaN;
+  return thEffObs / thEffPade;
+}
+
+export function deltaHCardy(thEffObs, thetaNominal) {
+  if (!Number.isFinite(thEffObs) || thEffObs <= 0) return NaN;
+  if (!Number.isFinite(thetaNominal) || thetaNominal <= 0) return NaN;
+  return Math.log(thEffObs / thetaNominal);
+}
+
+export function classifyRegime(eff, gObs, isRandom) {
+  if (!Number.isFinite(gObs)) return "unknown";
+  if (gObs > 1.05) return isRandom ? "swa" : "unknown";
+  if (!Number.isFinite(eff)) return "unknown";
+  if (eff < 0.01) return "fraud";
+  if (eff < 0.50) return "compressed";
+  if (eff > 1.50) return "overpade";
+  if (eff >= 0.85 && eff <= 1.15) return "normal";
+  return "unknown";
+}
+
+export function gammaCheckAll({ theta, T, gObs, isRandom }) {
+  const gPade = gammaPade(theta, T);
+  const thEffPade = thetaEffPade(theta, T);
+  const thEffObs = thetaEffObserved(gObs, T);
+  const eff = efficiency(thEffObs, thEffPade);
+  const dH = deltaHCardy(thEffObs, theta);
+  const regime = classifyRegime(eff, gObs, !!isRandom);
+  return {
+    gammaPade: gPade,
+    thetaEffPade: thEffPade,
+    thetaEffObs: thEffObs,
+    efficiency: eff,
+    deltaHCardy: dH,
+    regime,
+  };
+}
+
+export const REGIME_META = {
+  normal:     { emoji: "✅", cls: "v-yes" },
+  fraud:      { emoji: "🚨", cls: "v-no"  },
+  compressed: { emoji: "📉", cls: "v-deg" },
+  overpade:   { emoji: "📈", cls: "v-deg" },
+  swa:        { emoji: "🪟", cls: "v-deg" },
+  unknown:    { emoji: "❓", cls: "v-deg" },
+};

js/i18n.js

@@ -121,9 +121,18 @@ export const TRANSLATIONS = {
     "falsification.col.evidence": "Evidence",
 
     "tafcard.title":           "📇 TAF Card — full model profile",
-    "tafcard.recipes_title":   "📋 Recipes (verdict per dimension)",
+    "tafcard.recipes_title":   "📋 Recipes — verdict per dimension",
+    "tafcard.recipes_count_label": "dimensions",
     "tafcard.numbers_title":   "🔢 Key numbers (paper §26)",
-    "tafcard.fals_title":      "🔬 Falsification status (FALSIFICATION.md F1-F23)",
+    "tafcard.fals_title":      "🔬 Falsification status (F1-F23)",
+    "tafcard.fals_none":       "No falsifications applicable.",
+    "tafcard.diag_title":      "🔬 Diagnostics — numbers · γ check · what-if",
+    "tafcard.verify_title":    "✓ Verification — Lean + Sage + falsification",
+    "tafcard.share_title":     "📂 Provenance & share",
+    "tafcard.whatif_title":    "🎚️ What-if explorer",
+    "verdict.go":              "GO",
+    "verdict.no":              "NO",
+    "verdict.degraded":        "DEGRADED",
 
     "compare.title_out":       "🆚 Comparison Table",
 
@@ -147,12 +156,18 @@ export const TRANSLATIONS = {
     "param.T_train.tip":   "<strong>Max training context</strong>. From <code>max_position_embeddings</code>. Beyond this is extrapolation.",
     "param.T_eval":        "T_eval (your target)",
     "param.T_eval.tip":    "<strong>Your target inference context</strong>. The whole question is: will the model behave well at THIS length?",
-    "param.n_attn":        "num_attention_heads",
-    "param.n_kv":          "num_key_value_heads",
+    "param.n_attn":        "n_attention_heads",
+    "param.n_attn.tip":    "<strong>Number of attention heads</strong> per layer. From <code>num_attention_heads</code>.",
+    "param.n_kv":          "n_kv_heads",
+    "param.n_kv.tip":      "<strong>KV heads</strong>. If &lt; n_attention_heads → GQA (Grouped Query Attention). Reduces KV memory but pushes γ toward Hagedorn.",
     "param.d_head":        "head_dim",
-    "param.n_layers":      "num_hidden_layers",
+    "param.d_head.tip":    "<strong>Per-head dimension</strong>. Typical 64, 96, 128. From <code>head_dim</code> or <code>hidden_size / num_attention_heads</code>.",
+    "param.n_layers":      "n_layers",
+    "param.n_layers.tip":  "<strong>Number of transformer blocks</strong>. From <code>num_hidden_layers</code>.",
     "param.n_params":      "n_params (e.g. 8e9)",
+    "param.n_params.tip":  "<strong>Total parameter count</strong>. Threshold ~400M for induction-head emergence. Affects KV memory and budget recipes.",
     "param.has_swa":       "Has SWA?",
+    "param.has_swa.tip":   "<strong>Sliding Window Attention</strong>. <code>true</code> for Mistral, gemma-2, phi-3. v0.5.3 calibration audit disabled the historical δ_SWA correction (n=1 fit).",
     "common.yes":          "Yes",
     "common.no":           "No",
 
@@ -272,6 +287,92 @@ export const TRANSLATIONS = {
     "v053.calibration.title":     "🔬 v0.5.3 — Calibration audit (2026-05-02)",
     "v053.calibration.note":      "<strong>SWA correction disabled</strong> — original δ_SWA = -0.21 was fit on n=1 model (insufficient data; group-mean +0.355 with single yes-case). <strong>post_IH correction marked exploratory</strong> — group-mean ≈ 0 in re-audit (n=22 panel) does not replicate the OLS fit. <strong>GQA correction replicates</strong> (panel +0.115 vs hardcoded +0.11). <strong>D_f formula corrected for Phase B (γ&gt;1)</strong> — uses discrete cumulative sum instead of continuum approximation. LLaMA-3, Mistral, Gemma now report correct compression values.",
     "v053.release.banner":        "🔧 v0.5.3 — Audit-driven fixes: KV compression D_f now uses discrete sum (correct for all γ); δ_SWA disabled (n=1 calibration); paper §5.2 C_V coefficient erratum (1/4 → 1/12).",
+
+    // §35 v0.6 — γ predicted-vs-observed diagnostic
+    "gamma_check.title":           "🔍 γ predicted vs observed",
+    "gamma_check.desc":            "Enter your empirically measured γ. Tool detects regime: fraud (θ inflated) / compressed / over-Padé / SWA-random / normal.",
+    "gamma_check.gobs_label":      "γ_observed",
+    "gamma_check.gobs_tip":        "Empirically measured γ from your model's attention scores. Use the Diagnose CLI to obtain this from real weights.",
+    "gamma_check.random_label":    "Random corpus?",
+    "gamma_check.random_tip":      "Tick if γ_observed was measured on random/unstructured tokens. Distinguishes SWA signature (γ_obs > 1) from anomaly.",
+    "gamma_check.regime":          "Regime",
+    "gamma_check.regime.normal":         "Normal",
+    "gamma_check.regime.fraud":          "Fraud (θ inflated)",
+    "gamma_check.regime.compressed":     "Compressed context",
+    "gamma_check.regime.overpade":       "Over-Padé",
+    "gamma_check.regime.swa":            "SWA random-corpus signature",
+    "gamma_check.regime.unknown":        "Unknown",
+    "gamma_check.regime.normal.desc":    "η ∈ [0.85, 1.15]: model uses its full nominal context, no anomaly.",
+    "gamma_check.regime.fraud.desc":     "η < 0.01: nominal θ inflated. Model behaves as if θ ≪ advertised. Likely YaRN/marketing inflation without true context extension.",
+    "gamma_check.regime.compressed.desc":"η ∈ [0.01, 0.5): context is compressed (model attends less far than nominal θ predicts). Common in instruction-tuned / RLHF models.",
+    "gamma_check.regime.overpade.desc":  "η > 1.5: model attends farther than Padé predicts. Possible Lerch-corrected regime or undertrained early-checkpoint.",
+    "gamma_check.regime.swa.desc":       "γ_obs > 1.05 on random corpus = sliding-window attention signature (Mistral / Gemma family).",
+    "gamma_check.regime.unknown.desc":   "Inputs out of range or γ_obs > 1 without random-corpus flag. Verify measurement.",
+    "gamma_check.glossary.title":        "ⓘ Glossary — what these variables mean",
+    "gamma_check.glossary.gamma_pade":   "<strong>γ_Padé</strong>: closed-form prediction (2−z)/(2+z), z = T√2/θ. Paper §sec:gamma_decomposition.",
+    "gamma_check.glossary.gamma_obs":    "<strong>γ_observed</strong>: empirically measured from your model's attention scores (run the Diagnose CLI on real weights).",
+    "gamma_check.glossary.theta_eff_obs":"<strong>θ_eff (observed)</strong>: inverted from γ_obs via T√2 / (1 − γ_obs). Effective θ implied by your measurement.",
+    "gamma_check.glossary.theta_eff_pade":"<strong>θ_eff (Padé)</strong>: θ + T/√2. Effective θ predicted by closed-form.",
+    "gamma_check.glossary.efficiency":   "<strong>η</strong>: ratio θ_eff_obs / θ_eff_Padé. ≈1 = normal · &lt;0.01 = fraud · &lt;0.5 = compressed · &gt;1.5 = over-Padé.",
+    "gamma_check.glossary.delta_h":      "<strong>ΔH_Cardy</strong>: log(θ_eff_obs / θ_nominal). Cardy entropy shift. Negative = compression entropy. ~0 = nominal match.",
+    "gamma_check.glossary.regime":       "<strong>Regime</strong>: automatic classifier from η + γ_obs + random_corpus flag.",
+
+    // §36 v0.6 — Tooltips for inline ⓘ icons (per-variable explanations)
+    "tooltip.gamma_pade":          "<strong>γ_Padé(T_eval)</strong>: closed-form prediction (2−z)/(2+z), z = T√2/θ. Paper §sec:gamma_decomposition.",
+    "tooltip.gamma_decomposed":    "<strong>γ_decomposed</strong>: γ from full architectural decomposition. Padé baseline + GQA shift + post-IH shift (calibrated audit-replicated subset).",
+    "tooltip.d_horizon":           "<strong>d_horizon</strong>: effective attention horizon. Beyond this position, scores fall below noise floor (paper §26).",
+    "tooltip.L_NIAH":              "<strong>L_NIAH ceiling</strong>: predicted ceiling for needle-in-a-haystack retrieval reliability at current d_horizon.",
+    "tooltip.chi":                 "<strong>χ susceptibility</strong>: χ = 1/(1−γ). Diverges at the Hagedorn line γ=1.",
+    "tooltip.kv_memory":           "<strong>KV memory @ T_eval (BF16)</strong>: per-request KV cache = 2 · n_layers · n_kv_heads · d_head · T_eval bytes.",
+    "tooltip.theta_eff_obs":       "<strong>θ_eff (observed)</strong>: effective θ implied by your γ_observed: T√2 / (1 − γ_obs).",
+    "tooltip.theta_eff_pade":      "<strong>θ_eff (Padé)</strong>: effective θ predicted by closed-form: θ + T/√2.",
+    "tooltip.efficiency":          "<strong>η = θ_eff_obs / θ_eff_Padé</strong>: efficiency ratio. ≈1 = normal · &lt;0.01 = fraud · &lt;0.5 = compressed · &gt;1.5 = over-Padé.",
+    "tooltip.delta_h_cardy":       "<strong>ΔH_Cardy</strong>: log(θ_eff_obs / θ_nominal). Cardy entropy shift. Negative = compression entropy. ~0 = nominal match.",
+    "tooltip.verdict_aggregate":   "<strong>Verdict</strong>: worst-of across all recipes. ✅ GO = all green · ⚠ DEGRADED = ≥1 yellow · ❌ NO = ≥1 red.",
+    "tooltip.verdict_breakdown":   "<strong>Per-recipe breakdown</strong>: each recipe tests an <em>independent</em> decision axis (long-context · budget · hardware · custom-vs-API · KV-compression). A ❌ on X-1 means \"use the API for your volume\" not \"the model fails\" — open the Recipes section for per-axis context.",
+    "tooltip.gamma_pill":          "<strong>γ headline</strong>: γ_decomposed (or γ_Padé fallback). Range (0,1) = Phase A (anti-Ising). γ ≥ 1 = Hagedorn / Phase B.",
+    "tooltip.anti_ising":          "<strong>Anti-Ising class</strong>: Phase A → β = γ−1 &lt; 0. Machine-verified (Sage + Lean Mathlib4). See §35 v0.5.",
+
+    // §37 v0.6 — Lean+Mathlib theorem table
+    "lean.table.title":            "📑 Lean+Mathlib theorem table",
+    "lean.table.desc":             "Every entry below is machine-proven against Lean 4 + Mathlib4. Click any L# link to jump to the source line on GitHub. Grouped by topic — click a header to expand.",
+    "lean.table.theorem":          "Theorem",
+    "lean.table.claim":            "Claim",
+    "lean.table.tactic":           "Tactic",
+    "lean.table.source":           "Source",
+    "lean.table.lean":             "Lean",
+    "lean.findings.title":         "🔎 Substantive findings",
+    "lean.findings.detected_by":   "Detected by",
+    "lean.findings.fixed_by":      "Fixed by",
+    "lean.findings.recommendation":"Recommendation",
+    "lean.meta.repo":              "Repo",
+    "lean.meta.build":             "Build",
+    "lean.meta.theorems":          "Theorems",
+    "lean.meta.verified":          "verified",
+    "lean.meta.rejected":          "rejected",
+    "lean.meta.sorry":             "sorry",
+    "lean.meta.findings":          "substantive findings",
+    "lean.manifest.loading":       "Loading Lean manifest…",
+    "lean.manifest.error":         "Lean manifest unavailable",
+
+    // Help modal — v0.6 section
+    "help.v06.title":              "🆕 v0.6 — γ predicted-vs-observed + Cardy ΔH + Lean badges",
+    "help.v06.intro":              "<em>v0.6 (2026-05-06): three new diagnostics live in the TAF Card under <strong>🔬 Diagnostics</strong>. All run in your browser; γ_observed comes from the Diagnose CLI on real weights.</em>",
+    "help.v06.layout.title":       "TAF Card layout (new in v0.6)",
+    "help.v06.layout.body":        "After clicking <strong>🚀 Generate full profile</strong> the card shows: a <strong>hero strip</strong> on top (architecture class + meta + 3 pills: aggregate verdict ✅/⚠/❌, γ headline, 🧲 Anti-Ising if Phase A) and four <strong>expandable sections</strong>: <strong>📋 Recipes</strong> (open by default — verdict per dimension), <strong>🔬 Diagnostics</strong> (key numbers, γ predicted vs observed, what-if explorer), <strong>✓ Verification</strong> (Sage+Lean algebraic consistency, falsification F1-F23), <strong>📂 Provenance &amp; share</strong> (calibration audit + JSON download / share link / registry submit). Click any header to expand. Every variable has an inline <strong>ⓘ</strong> tooltip.",
+    "help.v06.gamma_check.title":  "γ predicted vs observed",
+    "help.v06.gamma_check.body":   "Enter the empirically-measured γ from your model and the tool computes <strong>η = θ_eff_obs / θ_eff_Padé</strong> and classifies into one of 5 regimes:",
+    "help.v06.case.normal":        "<strong>Normal</strong> (η ∈ [0.85, 1.15]) — model uses its full nominal context. <em>Use case</em>: validate a new release before adopting it.",
+    "help.v06.case.fraud":         "<strong>Fraud</strong> (η &lt; 0.01) — nominal θ inflated; model behaves as if θ ≪ advertised. <em>Use case</em>: detect YaRN/marketing inflation (CodeLlama / Mistral-Nemo pattern).",
+    "help.v06.case.compressed":    "<strong>Compressed</strong> (η &lt; 0.5) — context compressed; model attends shorter than nominal θ. <em>Use case</em>: spot RLHF/instruction-tuning compression (LLaMA-2 pattern).",
+    "help.v06.case.overpade":      "<strong>Over-Padé</strong> (η &gt; 1.5) — model attends farther than Padé predicts. <em>Use case</em>: identify Lerch-corrected regime or undertrained early checkpoints (pythia-1b pattern).",
+    "help.v06.case.swa":           "<strong>SWA random-corpus</strong> (γ_obs &gt; 1.05 with random_corpus=Yes) — sliding-window attention signature. <em>Use case</em>: confirm Mistral / Gemma SWA on random tokens.",
+    "help.v06.cardy.title":        "Cardy ΔH diagnostic",
+    "help.v06.cardy.body":         "<strong>ΔH_Cardy = log(θ_eff_obs / θ_nominal)</strong>. Entropy shift between observed effective θ and nominal θ. Strong negative = compression entropy; near zero = nominal match. Complements η for borderline cases.",
+    "help.v06.lean.title":         "Lean + Mathlib verification badges",
+    "help.v06.lean.body":          "TAF identities are formally machine-proven in Lean Mathlib4: <strong>37 theorems</strong> in 7 groups (Padé, RG flow, Cayley, D-SAGE, audit findings, erratum CV, misc) + <strong>1 substantive finding</strong> (V-derivative factor-2, theorem <code>V_derivative_ne_RG_beta</code>). Source: <a href=\"https://github.com/karlesmarin/lean-taf\" target=\"_blank\">github.com/karlesmarin/lean-taf</a> (commit 25c77fd). Re-verify locally: <code>git clone --depth=1 https://github.com/karlesmarin/lean-taf &amp;&amp; cd lean-taf &amp;&amp; lake exe cache get &amp;&amp; lake env lean Taf/Identities.lean</code>. The 🧲 Anti-Ising pill in the hero strip and the Verification accordion link to specific source lines.",
+    "help.v06.glossary.title":     "Variable glossary (also embedded in TAF Card)",
+    "help.v06.glossary.body":      "Every variable in the TAF Card has an inline ⓘ tooltip. The complete list: γ, γ_Padé, γ_decomposed, γ_observed, θ, θ_eff_obs, θ_eff_Padé, η, ΔH_Cardy, χ, d_horizon, L_NIAH, KV memory, regime. Hover any ⓘ for the definition + paper section.",
   },
 
   // ────────────────────────────────────────────────────────────────────────
@@ -328,6 +429,92 @@ export const TRANSLATIONS = {
     "v053.calibration.note":      "<strong>Corrección SWA desactivada</strong> — δ_SWA = -0.21 original se ajustó con n=1 modelo (datos insuficientes; promedio del único caso +0.355). <strong>Corrección post_IH marcada exploratoria</strong> — promedio de grupo ≈ 0 en re-auditoría (panel n=22) no replica el ajuste OLS. <strong>Corrección GQA replica</strong> (panel +0.115 vs hardcoded +0.11). <strong>Fórmula D_f corregida para Fase B (γ&gt;1)</strong> — usa suma cumulativa discreta en lugar de aproximación continua. LLaMA-3, Mistral, Gemma ahora reportan valores correctos de compresión.",
     "v053.release.banner":        "🔧 v0.5.3 — Correcciones por audit: D_f de compresión KV ahora usa suma discreta (correcto para todo γ); δ_SWA desactivado (calibración n=1); erratum coeficiente C_V paper §5.2 (1/4 → 1/12).",
 
+    // §35 v0.6 — Diagnóstico γ predicho vs observado
+    "gamma_check.title":           "🔍 γ predicho vs observado",
+    "gamma_check.desc":            "Introduce tu γ medido empíricamente. La herramienta detecta el régimen: fraude (θ inflado) / comprimido / sobre-Padé / SWA-aleatorio / normal.",
+    "gamma_check.gobs_label":      "γ_observado",
+    "gamma_check.gobs_tip":        "γ medido empíricamente desde los attention scores de tu modelo. Usa la CLI de Diagnose para obtenerlo desde pesos reales.",
+    "gamma_check.random_label":    "¿Corpus aleatorio?",
+    "gamma_check.random_tip":      "Marca sí si γ_observado se midió sobre tokens aleatorios/no estructurados. Distingue la firma SWA (γ_obs > 1) de una anomalía.",
+    "gamma_check.regime":          "Régimen",
+    "gamma_check.regime.normal":         "Normal",
+    "gamma_check.regime.fraud":          "Fraude (θ inflado)",
+    "gamma_check.regime.compressed":     "Contexto comprimido",
+    "gamma_check.regime.overpade":       "Sobre-Padé",
+    "gamma_check.regime.swa":            "Firma SWA (corpus aleatorio)",
+    "gamma_check.regime.unknown":        "Desconocido",
+    "gamma_check.regime.normal.desc":    "η ∈ [0.85, 1.15]: el modelo usa su contexto nominal completo, sin anomalías.",
+    "gamma_check.regime.fraud.desc":     "η < 0.01: θ nominal inflado. El modelo se comporta como si θ ≪ del anunciado. Probable inflación tipo YaRN/marketing sin extensión real de contexto.",
+    "gamma_check.regime.compressed.desc":"η ∈ [0.01, 0.5): contexto comprimido (el modelo atiende menos lejos de lo que predice θ nominal). Común en modelos instruction-tuned / RLHF.",
+    "gamma_check.regime.overpade.desc":  "η > 1.5: el modelo atiende más lejos de lo que Padé predice. Posible régimen Lerch-corregido o checkpoint temprano sub-entrenado.",
+    "gamma_check.regime.swa.desc":       "γ_obs > 1.05 sobre corpus aleatorio = firma de sliding-window attention (familias Mistral / Gemma).",
+    "gamma_check.regime.unknown.desc":   "Entradas fuera de rango o γ_obs > 1 sin flag de corpus aleatorio. Verifica la medición.",
+    "gamma_check.glossary.title":        "ⓘ Glosario — significado de las variables",
+    "gamma_check.glossary.gamma_pade":   "<strong>γ_Padé</strong>: predicción cerrada (2−z)/(2+z), z = T√2/θ. Paper §sec:gamma_decomposition.",
+    "gamma_check.glossary.gamma_obs":    "<strong>γ_observado</strong>: medido empíricamente desde los attention scores (ejecuta Diagnose CLI sobre pesos reales).",
+    "gamma_check.glossary.theta_eff_obs":"<strong>θ_eff (observado)</strong>: invertido desde γ_obs vía T√2 / (1 − γ_obs). θ efectivo implicado por tu medición.",
+    "gamma_check.glossary.theta_eff_pade":"<strong>θ_eff (Padé)</strong>: θ + T/√2. θ efectivo predicho por la fórmula cerrada.",
+    "gamma_check.glossary.efficiency":   "<strong>η</strong>: ratio θ_eff_obs / θ_eff_Padé. ≈1 = normal · &lt;0.01 = fraude · &lt;0.5 = comprimido · &gt;1.5 = sobre-Padé.",
+    "gamma_check.glossary.delta_h":      "<strong>ΔH_Cardy</strong>: log(θ_eff_obs / θ_nominal). Cambio de entropía de Cardy. Negativo = entropía de compresión. ~0 = coincide con nominal.",
+    "gamma_check.glossary.regime":       "<strong>Régimen</strong>: clasificador automático a partir de η + γ_obs + flag corpus_aleatorio.",
+
+    // §36 v0.6 — Tooltips para iconos ⓘ inline
+    "tooltip.gamma_pade":          "<strong>γ_Padé(T_eval)</strong>: predicción cerrada (2−z)/(2+z), z = T√2/θ. Paper §sec:gamma_decomposition.",
+    "tooltip.gamma_decomposed":    "<strong>γ_descompuesto</strong>: γ desde descomposición arquitectural completa. Línea base Padé + shift GQA + shift post-IH (subconjunto replicado en audit calibrado).",
+    "tooltip.d_horizon":           "<strong>d_horizon</strong>: horizonte efectivo de atención. Más allá los scores caen bajo el suelo de ruido (paper §26).",
+    "tooltip.L_NIAH":              "<strong>Techo L_NIAH</strong>: techo predicho de fiabilidad needle-in-a-haystack al d_horizon actual.",
+    "tooltip.chi":                 "<strong>χ susceptibilidad</strong>: χ = 1/(1−γ). Diverge en la línea Hagedorn γ=1.",
+    "tooltip.kv_memory":           "<strong>Memoria KV @ T_eval (BF16)</strong>: caché KV por petición = 2 · n_layers · n_kv_heads · d_head · T_eval bytes.",
+    "tooltip.theta_eff_obs":       "<strong>θ_eff (observado)</strong>: θ efectivo implicado por tu γ_observado: T√2 / (1 − γ_obs).",
+    "tooltip.theta_eff_pade":      "<strong>θ_eff (Padé)</strong>: θ efectivo predicho por la fórmula cerrada: θ + T/√2.",
+    "tooltip.efficiency":          "<strong>η = θ_eff_obs / θ_eff_Padé</strong>: ratio de eficiencia. ≈1 = normal · &lt;0.01 = fraude · &lt;0.5 = comprimido · &gt;1.5 = sobre-Padé.",
+    "tooltip.delta_h_cardy":       "<strong>ΔH_Cardy</strong>: log(θ_eff_obs / θ_nominal). Cambio de entropía de Cardy. Negativo = entropía de compresión. ~0 = coincide con nominal.",
+    "tooltip.verdict_aggregate":   "<strong>Veredicto</strong>: peor-de entre todas las recipes. ✅ ADELANTE = todo verde · ⚠ DEGRADADO = ≥1 amarillo · ❌ NO = ≥1 rojo.",
+    "tooltip.verdict_breakdown":   "<strong>Desglose por recipe</strong>: cada recipe evalúa un eje de decisión <em>independiente</em> (contexto-largo · presupuesto · hardware · custom-vs-API · compresión-KV). Un ❌ en X-1 significa «usa la API para tu volumen» no «el modelo falla» — abre la sección Recipes para contexto por eje.",
+    "tooltip.gamma_pill":          "<strong>γ titular</strong>: γ_descompuesto (o γ_Padé como fallback). Rango (0,1) = Fase A (anti-Ising). γ ≥ 1 = Hagedorn / Fase B.",
+    "tooltip.anti_ising":          "<strong>Clase Anti-Ising</strong>: Fase A → β = γ−1 &lt; 0. Machine-verified (Sage + Lean Mathlib4). Ver §35 v0.5.",
+
+    // §37 v0.6 — Tabla de teoremas Lean+Mathlib
+    "lean.table.title":            "📑 Tabla de teoremas Lean+Mathlib",
+    "lean.table.desc":             "Cada entrada está machine-proven contra Lean 4 + Mathlib4. Click en cualquier link L# para saltar a la línea fuente en GitHub. Agrupado por tema — click en cabecera para expandir.",
+    "lean.table.theorem":          "Teorema",
+    "lean.table.claim":            "Afirmación",
+    "lean.table.tactic":           "Táctica",
+    "lean.table.source":           "Fuente",
+    "lean.table.lean":             "Lean",
+    "lean.findings.title":         "🔎 Findings sustantivos",
+    "lean.findings.detected_by":   "Detectado por",
+    "lean.findings.fixed_by":      "Arreglado por",
+    "lean.findings.recommendation":"Recomendación",
+    "lean.meta.repo":              "Repo",
+    "lean.meta.build":             "Build",
+    "lean.meta.theorems":          "Teoremas",
+    "lean.meta.verified":          "verificados",
+    "lean.meta.rejected":          "rechazados",
+    "lean.meta.sorry":             "sorry",
+    "lean.meta.findings":          "findings sustantivos",
+    "lean.manifest.loading":       "Cargando manifest Lean…",
+    "lean.manifest.error":         "Manifest Lean no disponible",
+
+    // Help modal — sección v0.6
+    "help.v06.title":              "🆕 v0.6 — γ predicho-vs-observado + Cardy ΔH + badges Lean",
+    "help.v06.intro":              "<em>v0.6 (2026-05-06): tres diagnósticos nuevos viven en el TAF Card bajo <strong>🔬 Diagnósticos</strong>. Todo corre en tu navegador; γ_observado lo obtienes con la Diagnose CLI sobre pesos reales.</em>",
+    "help.v06.layout.title":       "Layout del TAF Card (nuevo en v0.6)",
+    "help.v06.layout.body":        "Tras click en <strong>🚀 Generar perfil completo</strong> la tarjeta muestra: una <strong>tira hero</strong> arriba (clase de arquitectura + meta + 3 pills: veredicto agregado ✅/⚠/❌, γ titular, 🧲 Anti-Ising si Fase A) y cuatro <strong>secciones plegables</strong>: <strong>📋 Recipes</strong> (abierto por defecto — veredicto por dimensión), <strong>🔬 Diagnósticos</strong> (números clave, γ predicho vs observado, explorador what-if), <strong>✓ Verificación</strong> (consistencia algebraica Sage+Lean, falsificación F1-F23), <strong>📂 Procedencia y compartir</strong> (auditoría de calibración + descarga JSON / enlace / submit al registro). Click en cualquier cabecera para expandir. Cada variable tiene tooltip <strong>ⓘ</strong> inline.",
+    "help.v06.gamma_check.title":  "γ predicho vs observado",
+    "help.v06.gamma_check.body":   "Introduces el γ medido empíricamente y la herramienta calcula <strong>η = θ_eff_obs / θ_eff_Padé</strong> y clasifica en uno de 5 regímenes:",
+    "help.v06.case.normal":        "<strong>Normal</strong> (η ∈ [0.85, 1.15]) — el modelo usa su contexto nominal completo. <em>Caso de uso</em>: validar un release nuevo antes de adoptarlo.",
+    "help.v06.case.fraud":         "<strong>Fraude</strong> (η &lt; 0.01) — θ nominal inflado; el modelo se comporta como si θ ≪ del anunciado. <em>Caso de uso</em>: detectar inflación YaRN/marketing (patrón CodeLlama / Mistral-Nemo).",
+    "help.v06.case.compressed":    "<strong>Comprimido</strong> (η &lt; 0.5) — contexto comprimido; el modelo atiende menos lejos que θ nominal. <em>Caso de uso</em>: detectar compresión por RLHF/instruction-tuning (patrón LLaMA-2).",
+    "help.v06.case.overpade":      "<strong>Sobre-Padé</strong> (η &gt; 1.5) — el modelo atiende más lejos que Padé predice. <em>Caso de uso</em>: identificar régimen Lerch-corregido o checkpoints tempranos sub-entrenados (patrón pythia-1b).",
+    "help.v06.case.swa":           "<strong>SWA corpus aleatorio</strong> (γ_obs &gt; 1.05 con corpus_aleatorio=Sí) — firma de sliding-window attention. <em>Caso de uso</em>: confirmar SWA en Mistral / Gemma sobre tokens random.",
+    "help.v06.cardy.title":        "Diagnóstico Cardy ΔH",
+    "help.v06.cardy.body":         "<strong>ΔH_Cardy = log(θ_eff_obs / θ_nominal)</strong>. Cambio de entropía entre el θ efectivo observado y el θ nominal. Negativo fuerte = entropía de compresión; cerca de cero = coincide con nominal. Complementa a η para casos borderline.",
+    "help.v06.lean.title":         "Badges de verificación Lean + Mathlib",
+    "help.v06.lean.body":          "Las identidades TAF están formalmente machine-proven en Lean Mathlib4: <strong>37 teoremas</strong> en 7 grupos (Padé, flujo RG, Cayley, D-SAGE, hallazgos de auditoría, erratum CV, misc) + <strong>1 hallazgo sustantivo</strong> (factor 2 en derivada V, teorema <code>V_derivative_ne_RG_beta</code>). Fuente: <a href=\"https://github.com/karlesmarin/lean-taf\" target=\"_blank\">github.com/karlesmarin/lean-taf</a> (commit 25c77fd). Re-verifica localmente: <code>git clone --depth=1 https://github.com/karlesmarin/lean-taf &amp;&amp; cd lean-taf &amp;&amp; lake exe cache get &amp;&amp; lake env lean Taf/Identities.lean</code>. La pill 🧲 Anti-Ising del hero y la sección Verificación enlazan a líneas específicas del código fuente.",
+    "help.v06.glossary.title":     "Glosario de variables (también embebido en TAF Card)",
+    "help.v06.glossary.body":      "Cada variable del TAF Card tiene un tooltip ⓘ inline. Lista completa: γ, γ_Padé, γ_descompuesto, γ_observado, θ, θ_eff_obs, θ_eff_Padé, η, ΔH_Cardy, χ, d_horizon, L_NIAH, memoria KV, régimen. Pasa el ratón sobre cualquier ⓘ para la definición + sección del paper.",
+
     "hero.title":     "🔬 TAF Agent",
     "hero.tagline":   "Prueba <strong>CUALQUIER</strong> LLM transformer antes de gastar GPU/€.",
     "hero.subtitle":  "Todo el cómputo corre localmente en tu navegador. Gratis. Sin límites. Auditable.",
@@ -438,9 +625,18 @@ export const TRANSLATIONS = {
     "falsification.col.evidence": "Evidencia",
 
     "tafcard.title":           "📇 TAF Card — perfil completo del modelo",
-    "tafcard.recipes_title":   "📋 Recetas (veredicto por dimensión)",
+    "tafcard.recipes_title":   "📋 Recetas — veredicto por dimensión",
+    "tafcard.recipes_count_label": "dimensiones",
     "tafcard.numbers_title":   "🔢 Números clave (paper §26)",
-    "tafcard.fals_title":      "🔬 Estado de falsificación (FALSIFICATION.md F1-F23)",
+    "tafcard.fals_title":      "🔬 Estado de falsificación (F1-F23)",
+    "tafcard.fals_none":       "Sin falsificaciones aplicables.",
+    "tafcard.diag_title":      "🔬 Diagnósticos — números · γ check · what-if",
+    "tafcard.verify_title":    "✓ Verificación — Lean + Sage + falsificación",
+    "tafcard.share_title":     "📂 Procedencia y compartir",
+    "tafcard.whatif_title":    "🎚️ Explorador what-if",
+    "verdict.go":              "ADELANTE",
+    "verdict.no":              "NO",
+    "verdict.degraded":        "DEGRADADO",
 
     "compare.title_out":       "🆚 Tabla comparativa",
 
@@ -464,12 +660,18 @@ export const TRANSLATIONS = {
     "param.T_train.tip":   "<strong>Contexto máximo de entrenamiento</strong>. De <code>max_position_embeddings</code>. Más allá es extrapolación.",
     "param.T_eval":        "T_eval (tu objetivo)",
     "param.T_eval.tip":    "<strong>Tu contexto de inferencia objetivo</strong>. La pregunta clave: ¿se comportará bien el modelo a ESTA longitud?",
-    "param.n_attn":        "num_attention_heads",
-    "param.n_kv":          "num_key_value_heads",
+    "param.n_attn":        "n_attention_heads",
+    "param.n_attn.tip":    "<strong>Número de attention heads</strong> por capa. De <code>num_attention_heads</code>.",
+    "param.n_kv":          "n_kv_heads",
+    "param.n_kv.tip":      "<strong>KV heads</strong>. Si &lt; n_attention_heads → GQA (Grouped Query Attention). Reduce memoria KV pero empuja γ hacia Hagedorn.",
     "param.d_head":        "head_dim",
-    "param.n_layers":      "num_hidden_layers",
+    "param.d_head.tip":    "<strong>Dimensión por head</strong>. Típico 64, 96, 128. De <code>head_dim</code> o <code>hidden_size / num_attention_heads</code>.",
+    "param.n_layers":      "n_layers",
+    "param.n_layers.tip":  "<strong>Número de bloques transformer</strong>. De <code>num_hidden_layers</code>.",
     "param.n_params":      "n_params (ej. 8e9)",
+    "param.n_params.tip":  "<strong>Número total de parámetros</strong>. Umbral ~400M para emergencia de induction heads. Afecta memoria KV y recipes de presupuesto.",
     "param.has_swa":       "¿Tiene SWA?",
+    "param.has_swa.tip":   "<strong>Sliding Window Attention</strong>. <code>true</code> para Mistral, gemma-2, phi-3. El audit de calibración v0.5.3 desactivó la corrección histórica δ_SWA (ajuste n=1).",
     "common.yes":          "Sí",
     "common.no":           "No",
 
@@ -595,6 +797,92 @@ export const TRANSLATIONS = {
     "v053.calibration.note":      "<strong>Correction SWA désactivée</strong> — δ_SWA = -0.21 d'origine était calibrée sur n=1 modèle (données insuffisantes ; moyenne du cas unique +0.355). <strong>Correction post_IH marquée exploratoire</strong> — moyenne de groupe ≈ 0 en ré-audit (panel n=22) ne réplique pas l'ajustement OLS. <strong>Correction GQA réplique</strong> (panel +0.115 vs hardcoded +0.11). <strong>Formule D_f corrigée pour Phase B (γ&gt;1)</strong> — utilise une somme cumulative discrète au lieu d'une approximation continue. LLaMA-3, Mistral, Gemma rapportent maintenant des valeurs de compression correctes.",
     "v053.release.banner":        "🔧 v0.5.3 — Corrections issues d'audit : D_f de compression KV utilise maintenant la somme discrète (correct pour tout γ) ; δ_SWA désactivé (calibrage n=1) ; erratum du coefficient C_V paper §5.2 (1/4 → 1/12).",
 
+    // §35 v0.6 — Diagnostic γ prédit vs observé
+    "gamma_check.title":           "🔍 γ prédit vs observé",
+    "gamma_check.desc":            "Saisissez votre γ mesuré empiriquement. L'outil détecte le régime : fraude (θ gonflé) / comprimé / sur-Padé / SWA-aléatoire / normal.",
+    "gamma_check.gobs_label":      "γ_observé",
+    "gamma_check.gobs_tip":        "γ mesuré empiriquement à partir des attention scores de votre modèle. Utilisez la CLI Diagnose pour l'obtenir depuis les poids réels.",
+    "gamma_check.random_label":    "Corpus aléatoire ?",
+    "gamma_check.random_tip":      "Cochez si γ_observé a été mesuré sur des tokens aléatoires/non structurés. Distingue la signature SWA (γ_obs > 1) d'une anomalie.",
+    "gamma_check.regime":          "Régime",
+    "gamma_check.regime.normal":         "Normal",
+    "gamma_check.regime.fraud":          "Fraude (θ gonflé)",
+    "gamma_check.regime.compressed":     "Contexte comprimé",
+    "gamma_check.regime.overpade":       "Sur-Padé",
+    "gamma_check.regime.swa":            "Signature SWA (corpus aléatoire)",
+    "gamma_check.regime.unknown":        "Inconnu",
+    "gamma_check.regime.normal.desc":    "η ∈ [0.85, 1.15] : le modèle utilise son contexte nominal complet, sans anomalie.",
+    "gamma_check.regime.fraud.desc":     "η < 0.01 : θ nominal gonflé. Le modèle se comporte comme si θ ≪ annoncé. Probable inflation YaRN/marketing sans vraie extension de contexte.",
+    "gamma_check.regime.compressed.desc":"η ∈ [0.01, 0.5) : contexte comprimé (le modèle attend moins loin que ne le prédit θ nominal). Fréquent en instruction-tuned / RLHF.",
+    "gamma_check.regime.overpade.desc":  "η > 1.5 : le modèle attend plus loin que Padé ne le prédit. Régime Lerch-corrigé possible ou checkpoint précoce sous-entraîné.",
+    "gamma_check.regime.swa.desc":       "γ_obs > 1.05 sur corpus aléatoire = signature de sliding-window attention (familles Mistral / Gemma).",
+    "gamma_check.regime.unknown.desc":   "Entrées hors plage ou γ_obs > 1 sans flag corpus_aléatoire. Vérifiez la mesure.",
+    "gamma_check.glossary.title":        "ⓘ Glossaire — signification des variables",
+    "gamma_check.glossary.gamma_pade":   "<strong>γ_Padé</strong> : prédiction fermée (2−z)/(2+z), z = T√2/θ. Paper §sec:gamma_decomposition.",
+    "gamma_check.glossary.gamma_obs":    "<strong>γ_observé</strong> : mesuré empiriquement à partir des attention scores (exécutez Diagnose CLI sur poids réels).",
+    "gamma_check.glossary.theta_eff_obs":"<strong>θ_eff (observé)</strong> : inversé depuis γ_obs via T√2 / (1 − γ_obs). θ effectif impliqué par votre mesure.",
+    "gamma_check.glossary.theta_eff_pade":"<strong>θ_eff (Padé)</strong> : θ + T/√2. θ effectif prédit par la formule fermée.",
+    "gamma_check.glossary.efficiency":   "<strong>η</strong> : rapport θ_eff_obs / θ_eff_Padé. ≈1 = normal · &lt;0.01 = fraude · &lt;0.5 = comprimé · &gt;1.5 = sur-Padé.",
+    "gamma_check.glossary.delta_h":      "<strong>ΔH_Cardy</strong> : log(θ_eff_obs / θ_nominal). Variation d'entropie de Cardy. Négatif = entropie de compression. ~0 = correspondance nominale.",
+    "gamma_check.glossary.regime":       "<strong>Régime</strong> : classifieur automatique à partir de η + γ_obs + flag corpus_aléatoire.",
+
+    // §36 v0.6 — Tooltips pour icônes ⓘ inline
+    "tooltip.gamma_pade":          "<strong>γ_Padé(T_eval)</strong> : prédiction fermée (2−z)/(2+z), z = T√2/θ. Paper §sec:gamma_decomposition.",
+    "tooltip.gamma_decomposed":    "<strong>γ_décomposé</strong> : γ depuis la décomposition architecturale complète. Ligne de base Padé + shift GQA + shift post-IH (sous-ensemble répliqué dans audit calibré).",
+    "tooltip.d_horizon":           "<strong>d_horizon</strong> : horizon d'attention effectif. Au-delà, les scores tombent sous le plancher de bruit (paper §26).",
+    "tooltip.L_NIAH":              "<strong>Plafond L_NIAH</strong> : plafond prédit de fiabilité needle-in-a-haystack au d_horizon courant.",
+    "tooltip.chi":                 "<strong>χ susceptibilité</strong> : χ = 1/(1−γ). Diverge à la ligne Hagedorn γ=1.",
+    "tooltip.kv_memory":           "<strong>Mémoire KV @ T_eval (BF16)</strong> : cache KV par requête = 2 · n_layers · n_kv_heads · d_head · T_eval octets.",
+    "tooltip.theta_eff_obs":       "<strong>θ_eff (observé)</strong> : θ effectif impliqué par votre γ_observé : T√2 / (1 − γ_obs).",
+    "tooltip.theta_eff_pade":      "<strong>θ_eff (Padé)</strong> : θ effectif prédit par la formule fermée : θ + T/√2.",
+    "tooltip.efficiency":          "<strong>η = θ_eff_obs / θ_eff_Padé</strong> : ratio d'efficacité. ≈1 = normal · &lt;0.01 = fraude · &lt;0.5 = comprimé · &gt;1.5 = sur-Padé.",
+    "tooltip.delta_h_cardy":       "<strong>ΔH_Cardy</strong> : log(θ_eff_obs / θ_nominal). Variation d'entropie de Cardy. Négatif = entropie de compression. ~0 = correspondance nominale.",
+    "tooltip.verdict_aggregate":   "<strong>Verdict</strong> : pire-de toutes les recettes. ✅ GO = tout vert · ⚠ DÉGRADÉ = ≥1 jaune · ❌ NON = ≥1 rouge.",
+    "tooltip.verdict_breakdown":   "<strong>Décomposition par recette</strong> : chaque recette teste un axe de décision <em>indépendant</em> (contexte-long · budget · matériel · custom-vs-API · compression-KV). Un ❌ en X-1 signifie « utilisez l'API pour votre volume » et non « le modèle échoue » — ouvrez la section Recettes pour le contexte par axe.",
+    "tooltip.gamma_pill":          "<strong>γ vedette</strong> : γ_décomposé (ou γ_Padé en fallback). Plage (0,1) = Phase A (anti-Ising). γ ≥ 1 = Hagedorn / Phase B.",
+    "tooltip.anti_ising":          "<strong>Classe Anti-Ising</strong> : Phase A → β = γ−1 &lt; 0. Machine-verified (Sage + Lean Mathlib4). Voir §35 v0.5.",
+
+    // §37 v0.6 — Table des théorèmes Lean+Mathlib
+    "lean.table.title":            "📑 Table des théorèmes Lean+Mathlib",
+    "lean.table.desc":             "Chaque entrée ci-dessous est machine-proven contre Lean 4 + Mathlib4. Cliquez sur un lien L# pour aller à la ligne source sur GitHub. Groupé par thème — cliquez sur un en-tête pour déplier.",
+    "lean.table.theorem":          "Théorème",
+    "lean.table.claim":            "Énoncé",
+    "lean.table.tactic":           "Tactique",
+    "lean.table.source":           "Source",
+    "lean.table.lean":             "Lean",
+    "lean.findings.title":         "🔎 Findings substantiels",
+    "lean.findings.detected_by":   "Détecté par",
+    "lean.findings.fixed_by":      "Corrigé par",
+    "lean.findings.recommendation":"Recommandation",
+    "lean.meta.repo":              "Repo",
+    "lean.meta.build":             "Build",
+    "lean.meta.theorems":          "Théorèmes",
+    "lean.meta.verified":          "vérifiés",
+    "lean.meta.rejected":          "rejetés",
+    "lean.meta.sorry":             "sorry",
+    "lean.meta.findings":          "findings substantiels",
+    "lean.manifest.loading":       "Chargement du manifeste Lean…",
+    "lean.manifest.error":         "Manifeste Lean indisponible",
+
+    // Help modal — section v0.6
+    "help.v06.title":              "🆕 v0.6 — γ prédit-vs-observé + Cardy ΔH + badges Lean",
+    "help.v06.intro":              "<em>v0.6 (2026-05-06) : trois nouveaux diagnostics vivent dans la TAF Card sous <strong>🔬 Diagnostics</strong>. Tout tourne dans votre navigateur ; γ_observé provient de la Diagnose CLI sur poids réels.</em>",
+    "help.v06.layout.title":       "Disposition de la TAF Card (nouveau en v0.6)",
+    "help.v06.layout.body":        "Après avoir cliqué <strong>🚀 Générer profil complet</strong>, la carte affiche : une <strong>bande hero</strong> en haut (classe d'architecture + méta + 3 pills : verdict agrégé ✅/⚠/❌, γ vedette, 🧲 Anti-Ising si Phase A) et quatre <strong>sections pliables</strong> : <strong>📋 Recettes</strong> (ouverte par défaut — verdict par dimension), <strong>🔬 Diagnostics</strong> (nombres clés, γ prédit vs observé, explorateur what-if), <strong>✓ Vérification</strong> (cohérence algébrique Sage+Lean, falsification F1-F23), <strong>📂 Provenance &amp; partage</strong> (audit de calibration + téléchargement JSON / lien / soumission registre). Cliquez sur n'importe quel en-tête pour déplier. Chaque variable a un tooltip <strong>ⓘ</strong> inline.",
+    "help.v06.gamma_check.title":  "γ prédit vs observé",
+    "help.v06.gamma_check.body":   "Saisissez le γ mesuré empiriquement et l'outil calcule <strong>η = θ_eff_obs / θ_eff_Padé</strong> et classe en l'un de 5 régimes :",
+    "help.v06.case.normal":        "<strong>Normal</strong> (η ∈ [0.85, 1.15]) — le modèle utilise son contexte nominal complet. <em>Cas d'usage</em> : valider une nouvelle release avant adoption.",
+    "help.v06.case.fraud":         "<strong>Fraude</strong> (η &lt; 0.01) — θ nominal gonflé ; le modèle se comporte comme si θ ≪ annoncé. <em>Cas d'usage</em> : détecter inflation YaRN/marketing (motif CodeLlama / Mistral-Nemo).",
+    "help.v06.case.compressed":    "<strong>Comprimé</strong> (η &lt; 0.5) — contexte comprimé ; le modèle attend moins loin que θ nominal. <em>Cas d'usage</em> : repérer compression par RLHF/instruction-tuning (motif LLaMA-2).",
+    "help.v06.case.overpade":      "<strong>Sur-Padé</strong> (η &gt; 1.5) — le modèle attend plus loin que Padé ne le prédit. <em>Cas d'usage</em> : identifier régime Lerch-corrigé ou checkpoints précoces sous-entraînés (motif pythia-1b).",
+    "help.v06.case.swa":           "<strong>SWA corpus aléatoire</strong> (γ_obs &gt; 1.05 avec corpus_aléatoire=Oui) — signature de sliding-window attention. <em>Cas d'usage</em> : confirmer SWA Mistral / Gemma sur tokens aléatoires.",
+    "help.v06.cardy.title":        "Diagnostic Cardy ΔH",
+    "help.v06.cardy.body":         "<strong>ΔH_Cardy = log(θ_eff_obs / θ_nominal)</strong>. Variation d'entropie entre le θ effectif observé et le θ nominal. Fortement négatif = entropie de compression ; proche de zéro = correspondance nominale. Complète η pour les cas borderline.",
+    "help.v06.lean.title":         "Badges de vérification Lean + Mathlib",
+    "help.v06.lean.body":          "Les identités TAF sont formellement machine-proven en Lean Mathlib4 : <strong>37 théorèmes</strong> en 7 groupes (Padé, flot RG, Cayley, D-SAGE, résultats d'audit, erratum CV, divers) + <strong>1 résultat substantiel</strong> (facteur 2 dans la dérivée V, théorème <code>V_derivative_ne_RG_beta</code>). Source : <a href=\"https://github.com/karlesmarin/lean-taf\" target=\"_blank\">github.com/karlesmarin/lean-taf</a> (commit 25c77fd). Re-vérifier localement : <code>git clone --depth=1 https://github.com/karlesmarin/lean-taf &amp;&amp; cd lean-taf &amp;&amp; lake exe cache get &amp;&amp; lake env lean Taf/Identities.lean</code>. La pill 🧲 Anti-Ising du hero et la section Vérification renvoient à des lignes sources spécifiques.",
+    "help.v06.glossary.title":     "Glossaire des variables (également intégré dans la TAF Card)",
+    "help.v06.glossary.body":      "Chaque variable de la TAF Card a un tooltip ⓘ inline. Liste complète : γ, γ_Padé, γ_décomposé, γ_observé, θ, θ_eff_obs, θ_eff_Padé, η, ΔH_Cardy, χ, d_horizon, L_NIAH, mémoire KV, régime. Survolez n'importe quel ⓘ pour la définition + section du paper.",
+
     "hero.title":     "🔬 TAF Agent",
     "hero.tagline":   "Testez <strong>N'IMPORTE QUEL</strong> LLM transformer avant de dépenser du GPU/€.",
     "hero.subtitle":  "Tout le calcul s'exécute localement dans votre navigateur. Gratuit. Illimité. Auditable.",
@@ -705,9 +993,18 @@ export const TRANSLATIONS = {
     "falsification.col.evidence": "Preuve",
 
     "tafcard.title":           "📇 TAF Card — profil complet du modèle",
-    "tafcard.recipes_title":   "📋 Recettes (verdict par dimension)",
+    "tafcard.recipes_title":   "📋 Recettes — verdict par dimension",
+    "tafcard.recipes_count_label": "dimensions",
     "tafcard.numbers_title":   "🔢 Nombres clés (paper §26)",
-    "tafcard.fals_title":      "🔬 État de falsification (FALSIFICATION.md F1-F23)",
+    "tafcard.fals_title":      "🔬 État de falsification (F1-F23)",
+    "tafcard.fals_none":       "Aucune falsification applicable.",
+    "tafcard.diag_title":      "🔬 Diagnostics — nombres · contrôle γ · what-if",
+    "tafcard.verify_title":    "✓ Vérification — Lean + Sage + falsification",
+    "tafcard.share_title":     "📂 Provenance & partage",
+    "tafcard.whatif_title":    "🎚️ Explorateur what-if",
+    "verdict.go":              "GO",
+    "verdict.no":              "NON",
+    "verdict.degraded":        "DÉGRADÉ",
 
     "compare.title_out":       "🆚 Tableau comparatif",
 
@@ -731,12 +1028,18 @@ export const TRANSLATIONS = {
     "param.T_train.tip":   "<strong>Contexte max d'entraînement</strong>. De <code>max_position_embeddings</code>. Au-delà c'est de l'extrapolation.",
     "param.T_eval":        "T_eval (votre cible)",
     "param.T_eval.tip":    "<strong>Votre contexte d'inférence cible</strong>. La question clé : le modèle se comportera-t-il bien à CETTE longueur ?",
-    "param.n_attn":        "num_attention_heads",
-    "param.n_kv":          "num_key_value_heads",
+    "param.n_attn":        "n_attention_heads",
+    "param.n_attn.tip":    "<strong>Nombre d'attention heads</strong> par couche. De <code>num_attention_heads</code>.",
+    "param.n_kv":          "n_kv_heads",
+    "param.n_kv.tip":      "<strong>KV heads</strong>. Si &lt; n_attention_heads → GQA (Grouped Query Attention). Réduit la mémoire KV mais pousse γ vers Hagedorn.",
     "param.d_head":        "head_dim",
-    "param.n_layers":      "num_hidden_layers",
+    "param.d_head.tip":    "<strong>Dimension par head</strong>. Typique 64, 96, 128. De <code>head_dim</code> ou <code>hidden_size / num_attention_heads</code>.",
+    "param.n_layers":      "n_layers",
+    "param.n_layers.tip":  "<strong>Nombre de blocs transformer</strong>. De <code>num_hidden_layers</code>.",
     "param.n_params":      "n_params (ex. 8e9)",
+    "param.n_params.tip":  "<strong>Nombre total de paramètres</strong>. Seuil ~400M pour l'émergence d'induction heads. Affecte la mémoire KV et les recettes de budget.",
     "param.has_swa":       "A SWA ?",
+    "param.has_swa.tip":   "<strong>Sliding Window Attention</strong>. <code>true</code> pour Mistral, gemma-2, phi-3. L'audit de calibration v0.5.3 a désactivé la correction historique δ_SWA (ajustement n=1).",
     "common.yes":          "Oui",
     "common.no":           "Non",
 
@@ -862,6 +1165,92 @@ export const TRANSLATIONS = {
     "v053.calibration.note":      "<strong>SWA 修正已禁用</strong> — 原 δ_SWA = -0.21 基于 n=1 模型拟合（数据不足；唯一案例的均值为 +0.355）。<strong>post_IH 修正标记为探索性</strong> — 重审中组均值 ≈ 0（n=22 面板）未能复现 OLS 拟合。<strong>GQA 修正可复现</strong>（面板 +0.115 vs 硬编码 +0.11）。<strong>D_f 公式修正 Phase B (γ&gt;1)</strong> — 使用离散累积和代替连续近似。LLaMA-3、Mistral、Gemma 现在报告正确的压缩值。",
     "v053.release.banner":        "🔧 v0.5.3 — 审计驱动的修复：KV 压缩 D_f 现使用离散和（适用于所有 γ）；δ_SWA 禁用（n=1 校准）；论文 §5.2 C_V 系数勘误 (1/4 → 1/12)。",
 
+    // §35 v0.6 — γ 预测 vs 观测 诊断
+    "gamma_check.title":           "🔍 γ 预测 vs 观测",
+    "gamma_check.desc":            "输入你经验测量的 γ。工具自动检测体制：欺诈 (θ 虚高) / 压缩 / 超 Padé / SWA-随机 / 正常。",
+    "gamma_check.gobs_label":      "γ_观测",
+    "gamma_check.gobs_tip":        "从模型注意力分数经验测量的 γ。使用 Diagnose CLI 从真实权重获取。",
+    "gamma_check.random_label":    "随机语料？",
+    "gamma_check.random_tip":      "若 γ_观测在随机/无结构 token 上测得请勾选。区分 SWA 签名 (γ_obs > 1) 与异常。",
+    "gamma_check.regime":          "体制",
+    "gamma_check.regime.normal":         "正常",
+    "gamma_check.regime.fraud":          "欺诈 (θ 虚高)",
+    "gamma_check.regime.compressed":     "上下文压缩",
+    "gamma_check.regime.overpade":       "超 Padé",
+    "gamma_check.regime.swa":            "SWA 签名 (随机语料)",
+    "gamma_check.regime.unknown":        "未知",
+    "gamma_check.regime.normal.desc":    "η ∈ [0.85, 1.15]：模型完全利用名义上下文，无异常。",
+    "gamma_check.regime.fraud.desc":     "η < 0.01：名义 θ 虚高。模型表现如同 θ 远小于宣称值。可能是 YaRN/营销虚标，无真实上下文扩展。",
+    "gamma_check.regime.compressed.desc":"η ∈ [0.01, 0.5)：上下文压缩 (模型注意距离比名义 θ 预测更短)。常见于 instruction-tuned / RLHF 模型。",
+    "gamma_check.regime.overpade.desc":  "η > 1.5：模型注意距离超过 Padé 预测。可能是 Lerch 修正体制或欠训练早期 checkpoint。",
+    "gamma_check.regime.swa.desc":       "随机语料上 γ_obs > 1.05 = 滑动窗口注意力签名 (Mistral / Gemma 系列)。",
+    "gamma_check.regime.unknown.desc":   "输入超范围或 γ_obs > 1 但未标记随机语料。请核验测量。",
+    "gamma_check.glossary.title":        "ⓘ 词汇表 — 变量含义",
+    "gamma_check.glossary.gamma_pade":   "<strong>γ_Padé</strong>：闭式预测 (2−z)/(2+z), z = T√2/θ。论文 §sec:gamma_decomposition。",
+    "gamma_check.glossary.gamma_obs":    "<strong>γ_观测</strong>：从注意力分数经验测得 (在真实权重上运行 Diagnose CLI)。",
+    "gamma_check.glossary.theta_eff_obs":"<strong>θ_eff (观测)</strong>：由 γ_obs 反演 T√2 / (1 − γ_obs)。测量隐含的有效 θ。",
+    "gamma_check.glossary.theta_eff_pade":"<strong>θ_eff (Padé)</strong>：θ + T/√2。闭式公式预测的有效 θ。",
+    "gamma_check.glossary.efficiency":   "<strong>η</strong>：θ_eff_obs / θ_eff_Padé 比值。≈1 = 正常 · &lt;0.01 = 欺诈 · &lt;0.5 = 压缩 · &gt;1.5 = 超 Padé。",
+    "gamma_check.glossary.delta_h":      "<strong>ΔH_Cardy</strong>：log(θ_eff_obs / θ_nominal)。Cardy 熵变。负值 = 压缩熵。~0 = 与名义匹配。",
+    "gamma_check.glossary.regime":       "<strong>体制</strong>：基于 η + γ_obs + 随机语料标志的自动分类器。",
+
+    // §36 v0.6 — 内联 ⓘ 图标提示
+    "tooltip.gamma_pade":          "<strong>γ_Padé(T_eval)</strong>：闭式预测 (2−z)/(2+z), z = T√2/θ。论文 §sec:gamma_decomposition。",
+    "tooltip.gamma_decomposed":    "<strong>γ_分解</strong>：基于完整架构分解的 γ。Padé 基线 + GQA 偏移 + post-IH 偏移 (校准审计已复制子集)。",
+    "tooltip.d_horizon":           "<strong>d_horizon</strong>：有效注意力视野。超过此位置分数低于噪声底 (论文 §26)。",
+    "tooltip.L_NIAH":              "<strong>L_NIAH 上限</strong>：当前 d_horizon 下针-在-干草堆检索可靠性的预测上限。",
+    "tooltip.chi":                 "<strong>χ 易感性</strong>：χ = 1/(1−γ)。在 Hagedorn 线 γ=1 处发散。",
+    "tooltip.kv_memory":           "<strong>KV 内存 @ T_eval (BF16)</strong>：每请求 KV 缓存 = 2 · n_layers · n_kv_heads · d_head · T_eval 字节。",
+    "tooltip.theta_eff_obs":       "<strong>θ_eff (观测)</strong>：由 γ_观测 隐含的有效 θ：T√2 / (1 − γ_obs)。",
+    "tooltip.theta_eff_pade":      "<strong>θ_eff (Padé)</strong>：闭式公式预测的有效 θ：θ + T/√2。",
+    "tooltip.efficiency":          "<strong>η = θ_eff_obs / θ_eff_Padé</strong>：效率比。≈1 = 正常 · &lt;0.01 = 欺诈 · &lt;0.5 = 压缩 · &gt;1.5 = 超 Padé。",
+    "tooltip.delta_h_cardy":       "<strong>ΔH_Cardy</strong>：log(θ_eff_obs / θ_nominal)。Cardy 熵变。负值 = 压缩熵。~0 = 与名义匹配。",
+    "tooltip.verdict_aggregate":   "<strong>判定</strong>：所有配方中最差。✅ 通过 = 全绿 · ⚠ 降级 = ≥1 黄 · ❌ 否 = ≥1 红。",
+    "tooltip.verdict_breakdown":   "<strong>各配方分解</strong>：每个配方测试一个<em>独立</em>的决策轴 (长上下文 · 预算 · 硬件 · 自训 vs API · KV 压缩)。X-1 上的 ❌ 表示「按你的量级用 API」而非「模型失败」——展开 Recipes 节查看各轴上下文。",
+    "tooltip.gamma_pill":          "<strong>γ 头条</strong>：γ_分解 (或 γ_Padé 回退)。范围 (0,1) = 相位 A (反伊辛)。γ ≥ 1 = Hagedorn / 相位 B。",
+    "tooltip.anti_ising":          "<strong>反伊辛类</strong>：相位 A → β = γ−1 &lt; 0。机器证明 (Sage + Lean Mathlib4)。见 §35 v0.5。",
+
+    // §37 v0.6 — Lean+Mathlib 定理表
+    "lean.table.title":            "📑 Lean+Mathlib 定理表",
+    "lean.table.desc":             "下方每一项都已机器证明对 Lean 4 + Mathlib4。点击任意 L# 链接跳转到 GitHub 源码行。按主题分组——点击标题展开。",
+    "lean.table.theorem":          "定理",
+    "lean.table.claim":            "陈述",
+    "lean.table.tactic":           "策略",
+    "lean.table.source":           "出处",
+    "lean.table.lean":             "Lean",
+    "lean.findings.title":         "🔎 实质性发现",
+    "lean.findings.detected_by":   "检测于",
+    "lean.findings.fixed_by":      "修正于",
+    "lean.findings.recommendation":"建议",
+    "lean.meta.repo":              "仓库",
+    "lean.meta.build":             "构建",
+    "lean.meta.theorems":          "定理",
+    "lean.meta.verified":          "已验证",
+    "lean.meta.rejected":          "已拒绝",
+    "lean.meta.sorry":             "sorry",
+    "lean.meta.findings":          "项实质性发现",
+    "lean.manifest.loading":       "正在加载 Lean 清单…",
+    "lean.manifest.error":         "Lean 清单不可用",
+
+    // 帮助弹窗 — v0.6 节
+    "help.v06.title":              "🆕 v0.6 — γ 预测-vs-观测 + Cardy ΔH + Lean 徽章",
+    "help.v06.intro":              "<em>v0.6 (2026-05-06)：三个新诊断位于 TAF 卡的 <strong>🔬 诊断</strong> 下。全部在浏览器运行；γ_观测来自在真实权重上运行 Diagnose CLI。</em>",
+    "help.v06.layout.title":       "TAF 卡布局 (v0.6 新增)",
+    "help.v06.layout.body":        "点击 <strong>🚀 生成完整画像</strong> 后，卡片展示：顶部一条 <strong>hero 条</strong> (架构类 + 元信息 + 3 个 pill：聚合判定 ✅/⚠/❌、γ 头条、🧲 反伊辛若处于相位 A) 和四个 <strong>可展开节</strong>：<strong>📋 配方</strong> (默认展开 — 各维度判定)、<strong>🔬 诊断</strong> (关键数字、γ 预测 vs 观测、what-if 浏览器)、<strong>✓ 验证</strong> (Sage+Lean 代数一致性、可证伪 F1-F23)、<strong>📂 来源与分享</strong> (校准审计 + JSON 下载 / 链接 / 注册表提交)。点击任意标题展开。每个变量都有内联 <strong>ⓘ</strong> 提示。",
+    "help.v06.gamma_check.title":  "γ 预测 vs 观测",
+    "help.v06.gamma_check.body":   "输入经验测量的 γ，工具计算 <strong>η = θ_eff_obs / θ_eff_Padé</strong> 并分类到 5 种体制之一：",
+    "help.v06.case.normal":        "<strong>正常</strong> (η ∈ [0.85, 1.15]) — 模型完整使用名义上下文。<em>用例</em>：在采用前验证新发布。",
+    "help.v06.case.fraud":         "<strong>欺诈</strong> (η &lt; 0.01) — 名义 θ 虚高；模型表现如同 θ ≪ 宣称值。<em>用例</em>：检测 YaRN/营销虚标 (CodeLlama / Mistral-Nemo 模式)。",
+    "help.v06.case.compressed":    "<strong>压缩</strong> (η &lt; 0.5) — 上下文压缩；模型注意距离比名义 θ 短。<em>用例</em>：识别 RLHF/指令调优引起的压缩 (LLaMA-2 模式)。",
+    "help.v06.case.overpade":      "<strong>超 Padé</strong> (η &gt; 1.5) — 模型注意距离超过 Padé 预测。<em>用例</em>：识别 Lerch 修正体制或欠训练早期 checkpoint (pythia-1b 模式)。",
+    "help.v06.case.swa":           "<strong>SWA 随机语料</strong> (γ_obs &gt; 1.05 且 随机语料=是) — 滑动窗口注意力签名。<em>用例</em>：在随机 token 上确认 Mistral / Gemma SWA。",
+    "help.v06.cardy.title":        "Cardy ΔH 诊断",
+    "help.v06.cardy.body":         "<strong>ΔH_Cardy = log(θ_eff_obs / θ_nominal)</strong>。观测有效 θ 与名义 θ 之间的熵变。强负值 = 压缩熵；接近零 = 与名义匹配。在边界情况下补充 η。",
+    "help.v06.lean.title":         "Lean + Mathlib 验证徽章",
+    "help.v06.lean.body":          "TAF 恒等式在 Lean Mathlib4 中形式化机器证明：<strong>37 个定理</strong>分布于 7 组（Padé、RG 流、Cayley、D-SAGE、审计发现、CV 勘误、杂项）+ <strong>1 项实质性发现</strong>（V 导数 2 倍因子，定理 <code>V_derivative_ne_RG_beta</code>）。源：<a href=\"https://github.com/karlesmarin/lean-taf\" target=\"_blank\">github.com/karlesmarin/lean-taf</a>（commit 25c77fd）。本地重新验证：<code>git clone --depth=1 https://github.com/karlesmarin/lean-taf &amp;&amp; cd lean-taf &amp;&amp; lake exe cache get &amp;&amp; lake env lean Taf/Identities.lean</code>。Hero 中的 🧲 反伊辛 pill 与验证手风琴链接到具体源码行。",
+    "help.v06.glossary.title":     "变量词汇表 (亦嵌入 TAF 卡)",
+    "help.v06.glossary.body":      "TAF 卡中每个变量都有内联 ⓘ 提示。完整列表：γ、γ_Padé、γ_分解、γ_观测、θ、θ_eff_obs、θ_eff_Padé、η、ΔH_Cardy、χ、d_horizon、L_NIAH、KV 内存、体制。鼠标悬停任意 ⓘ 查看定义 + 论文章节。",
+
     "hero.title":     "🔬 TAF Agent",
     "hero.tagline":   "在花费 GPU/$ 之前，测试<strong>任意</strong> Transformer LLM。",
     "hero.subtitle":  "所有计算在您的浏览器本地运行。免费。无限制。可审计。",
@@ -972,9 +1361,18 @@ export const TRANSLATIONS = {
     "falsification.col.evidence": "证据",
 
     "tafcard.title":           "📇 TAF 卡 — 完整模型画像",
-    "tafcard.recipes_title":   "📋 配方(每个维度的判定)",
+    "tafcard.recipes_title":   "📋 配方 — 各维度判定",
+    "tafcard.recipes_count_label": "维度",
     "tafcard.numbers_title":   "🔢 关键数字 (paper §26)",
-    "tafcard.fals_title":      "🔬 可证伪状态 (FALSIFICATION.md F1-F23)",
+    "tafcard.fals_title":      "🔬 可证伪状态 (F1-F23)",
+    "tafcard.fals_none":       "无适用的可证伪。",
+    "tafcard.diag_title":      "🔬 诊断 — 数字 · γ 检验 · what-if",
+    "tafcard.verify_title":    "✓ 验证 — Lean + Sage + 可证伪",
+    "tafcard.share_title":     "📂 来源与分享",
+    "tafcard.whatif_title":    "🎚️ What-if 浏览器",
+    "verdict.go":              "通过",
+    "verdict.no":              "否",
+    "verdict.degraded":        "降级",
 
     "compare.title_out":       "🆚 比较表",
 
@@ -998,12 +1396,18 @@ export const TRANSLATIONS = {
     "param.T_train.tip":   "<strong>训练最大上下文</strong>。来自 <code>max_position_embeddings</code>。超出此范围属于外推。",
     "param.T_eval":        "T_eval (您的目标)",
     "param.T_eval.tip":    "<strong>您的目标推理上下文</strong>。关键问题: 模型在 <em>这个</em> 长度下表现是否良好?",
-    "param.n_attn":        "num_attention_heads",
-    "param.n_kv":          "num_key_value_heads",
+    "param.n_attn":        "n_attention_heads",
+    "param.n_attn.tip":    "<strong>每层 attention heads 数</strong>。来自 <code>num_attention_heads</code>。",
+    "param.n_kv":          "n_kv_heads",
+    "param.n_kv.tip":      "<strong>KV heads</strong>。若 &lt; n_attention_heads → GQA (Grouped Query Attention)。降低 KV 内存但将 γ 推向 Hagedorn。",
     "param.d_head":        "head_dim",
-    "param.n_layers":      "num_hidden_layers",
+    "param.d_head.tip":    "<strong>每 head 维度</strong>。典型 64、96、128。来自 <code>head_dim</code> 或 <code>hidden_size / num_attention_heads</code>。",
+    "param.n_layers":      "n_layers",
+    "param.n_layers.tip":  "<strong>Transformer 块数</strong>。来自 <code>num_hidden_layers</code>。",
     "param.n_params":      "n_params (例如 8e9)",
+    "param.n_params.tip":  "<strong>总参数量</strong>。约 400M 阈值出现 induction heads。影响 KV 内存和预算配方。",
     "param.has_swa":       "有 SWA 吗?",
+    "param.has_swa.tip":   "<strong>Sliding Window Attention</strong>。Mistral、gemma-2、phi-3 为 <code>true</code>。v0.5.3 校准审计禁用了历史 δ_SWA 校正 (n=1 拟合)。",
     "common.yes":          "是",
     "common.no":           "否",
 

js/lean_badges.js

@@ -0,0 +1,119 @@
+// Lean+Mathlib provenance — loads `data/lean_status.json`, exposes per-theorem
+// badge HTML + a grouped table renderer for the Verification accordion.
+// Pure browser-only: just fetches a static JSON manifest.
+
+let _manifest = null;
+let _byName = null;
+
+export async function loadLeanManifest(url = "data/lean_status.json") {
+  if (_manifest) return _manifest;
+  const res = await fetch(url, { cache: "default" });
+  if (!res.ok) throw new Error(`lean manifest fetch failed: ${res.status}`);
+  _manifest = await res.json();
+  _byName = {};
+  for (const g of _manifest.groups) {
+    for (const t of g.theorems) {
+      t._group = g.id;
+      t._url = sourceUrl(_manifest, t);
+      _byName[t.name] = t;
+    }
+  }
+  return _manifest;
+}
+
+export function getManifest() { return _manifest; }
+export function getTheorem(name) { return _byName ? _byName[name] : null; }
+
+export function sourceUrl(manifest, theorem) {
+  const repo = manifest.lean_repo;
+  return `${repo.url}/blob/${repo.default_branch}/${theorem.file}#L${theorem.line}`;
+}
+
+const escapeHtml = (s) => String(s ?? "").replace(/[&<>"]/g, c => ({"&":"&amp;","<":"&lt;",">":"&gt;",'"':"&quot;"}[c]));
+const escapeAttr = (s) => String(s ?? "").replace(/"/g, "&quot;");
+
+export function badgeHtml(theoremName, label = "✓ Lean ↗") {
+  const t = getTheorem(theoremName);
+  if (!t) return "";
+  return `<a href="${escapeAttr(t._url)}" target="_blank" rel="noopener" class="lean-badge" title="Lean theorem: ${escapeAttr(t.name)} — ${escapeAttr(t.claim)} (tactic: ${escapeAttr(t.tactic || "")})">${escapeHtml(label)}</a>`;
+}
+
+export function badgesForUiBinding(bindingKey) {
+  // Returns concatenated badges for a UI binding (single string or array of names).
+  const manifest = getManifest();
+  if (!manifest || !manifest.ui_bindings) return "";
+  const binding = manifest.ui_bindings[bindingKey];
+  if (!binding) return "";
+  const names = Array.isArray(binding) ? binding : [binding];
+  return names.map(n => badgeHtml(n, "✓ Lean")).filter(Boolean).join(" ");
+}
+
+export function renderTheoremTable() {
+  const manifest = getManifest();
+  if (!manifest) return "<div class='subtle'>Lean manifest not loaded.</div>";
+
+  const repo = manifest.lean_repo;
+  const headerHtml = `
+    <div class="lean-meta">
+      <div><strong data-i18n="lean.meta.repo">Repo</strong>: <a href="${escapeAttr(repo.url)}" target="_blank">${escapeHtml(repo.name)}</a> @ <code>${escapeHtml(repo.commit_short)}</code></div>
+      <div class="subtle"><strong data-i18n="lean.meta.build">Build</strong>: ${repo.build_jobs} jobs · ${escapeHtml(repo.lean_toolchain)} · ${repo.compile_time_seconds}s compile (warm)</div>
+      <div class="subtle"><strong data-i18n="lean.meta.theorems">Theorems</strong>: ${manifest.summary.theorems_total} <span data-i18n="lean.meta.verified">verified</span> · ${manifest.summary.lean_rejected} <span data-i18n="lean.meta.rejected">rejected</span> · ${manifest.summary.skipped_sorry} <span data-i18n="lean.meta.sorry">sorry</span> · ${manifest.summary.substantive_findings} <span data-i18n="lean.meta.findings">substantive findings</span></div>
+    </div>`;
+
+  const findingsHtml = (manifest.findings && manifest.findings.length)
+    ? `<details class="lean-findings" open>
+        <summary><strong data-i18n="lean.findings.title">🔎 Substantive findings</strong> (${manifest.findings.length})</summary>
+        ${manifest.findings.map(f => `
+          <div class="lean-finding">
+            <div><strong>${escapeHtml(f.id)} — ${escapeHtml(f.title)}</strong>
+              <span class="lean-pill ${f.severity === "substantive" ? "v-deg" : ""}">${escapeHtml(f.severity)}</span></div>
+            <div class="subtle" style="margin-top:0.3em;">${escapeHtml(f.summary)}</div>
+            <div style="margin-top:0.3em;">
+              <span class="subtle"><span data-i18n="lean.findings.detected_by">Detected by</span>:</span> ${badgeHtml(f.detected_by, f.detected_by + " ↗")}
+              ${f.fixed_by && f.fixed_by.length ? ` · <span class="subtle"><span data-i18n="lean.findings.fixed_by">Fixed by</span>:</span> ${f.fixed_by.map(n => badgeHtml(n, n + " ↗")).join(" ")}` : ""}
+            </div>
+            <div class="subtle" style="margin-top:0.3em;"><strong data-i18n="lean.findings.recommendation">Recommendation</strong>: ${escapeHtml(f.recommendation)}</div>
+          </div>
+        `).join("")}
+      </details>`
+    : "";
+
+  const groupsHtml = manifest.groups.map(g => `
+    <details class="lean-group">
+      <summary><strong>${escapeHtml(g.title)}</strong> <span class="subtle">(${g.theorems.length})</span></summary>
+      <div class="lean-table-wrap">
+        <table class="lean-table">
+          <thead>
+            <tr>
+              <th data-i18n="lean.table.theorem">Theorem</th>
+              <th data-i18n="lean.table.claim">Claim</th>
+              <th data-i18n="lean.table.tactic">Tactic</th>
+              <th data-i18n="lean.table.source">Source</th>
+              <th data-i18n="lean.table.lean">Lean</th>
+            </tr>
+          </thead>
+          <tbody>
+            ${g.theorems.map(t => `
+              <tr>
+                <td><code>${escapeHtml(t.name)}</code></td>
+                <td>${escapeHtml(t.claim)}</td>
+                <td><code class="subtle">${escapeHtml(t.tactic || "")}</code></td>
+                <td class="subtle">${t.source ? renderSource(t.source) : "—"}</td>
+                <td>${badgeHtml(t.name, "L" + t.line + " ↗")}</td>
+              </tr>`).join("")}
+          </tbody>
+        </table>
+      </div>
+    </details>`).join("");
+
+  return `${headerHtml}${findingsHtml}<div class="lean-groups">${groupsHtml}</div>`;
+}
+
+function renderSource(src) {
+  const parts = [];
+  if (src.doc) parts.push(`<code>${escapeHtml(src.doc)}</code>`);
+  if (src.section) parts.push(escapeHtml(src.section));
+  if (src.line) parts.push(`L${src.line}`);
+  if (src.label) parts.push(`<em>${escapeHtml(src.label)}</em>`);
+  return parts.join(" · ");
+}

js/main.js

@@ -9,6 +9,8 @@
 
 import { initI18n, setLang, t } from "./i18n.js";
 import { initPhaseDiagram } from "./phase_diagram.js";
+import { gammaCheckAll, REGIME_META } from "./gamma_check.js";
+import { loadLeanManifest, badgeHtml, badgesForUiBinding, renderTheoremTable, getManifest } from "./lean_badges.js";
 
 const TAF_BROWSER_URL = "python/taf_browser.py";
 const ENABLE_WEBLLM = true;
@@ -1087,75 +1089,173 @@ function renderProfile(p, params) {
     </div>
   `).join("");
 
+  // Reusable tooltip helper — keeps tooltip pattern uniform across the card
+  const ttip = (key, fallback) =>
+    `<span class="info"><span class="tooltip" data-i18n="${key}">${fallback}</span></span>`;
+
   const numbersHtml = `
-    <div class="num-row"><span class="num-label">γ_Padé(T_eval)</span><span class="num-value">${formatN(kn.gamma_pade)}</span></div>
-    <div class="num-row"><span class="num-label">γ_decomposed</span><span class="num-value">${formatN(kn.gamma_decomposed)}</span></div>
-    <div class="num-row"><span class="num-label">d_horizon</span><span class="num-value">${formatN(kn.d_horizon)}</span></div>
-    <div class="num-row"><span class="num-label">L_NIAH ceiling</span><span class="num-value">${formatN(kn.L_NIAH_ceiling)}</span></div>
-    <div class="num-row"><span class="num-label">χ susceptibility</span><span class="num-value">${formatN(kn.chi_susceptibility)}</span></div>
-    <div class="num-row"><span class="num-label">KV memory @ T_eval (BF16)</span><span class="num-value">${formatN(kn.kv_memory_per_request_GB)} GB</span></div>
+    <div class="num-row"><span class="num-label">γ_Padé(T_eval) ${ttip("tooltip.gamma_pade", "Closed-form prediction (2−z)/(2+z), z = T√2/θ. Paper §sec:gamma_decomposition.")}</span><span class="num-value">${formatN(kn.gamma_pade)}</span></div>
+    <div class="num-row"><span class="num-label">γ_decomposed ${ttip("tooltip.gamma_decomposed", "γ from full architectural decomposition: Padé baseline + GQA shift + SWA shift + post-IH shift.")}</span><span class="num-value">${formatN(kn.gamma_decomposed)}</span></div>
+    <div class="num-row"><span class="num-label">d_horizon ${ttip("tooltip.d_horizon", "Effective attention horizon at T_eval. Beyond this, attention scores fall below the noise floor (paper §26).")}</span><span class="num-value">${formatN(kn.d_horizon)}</span></div>
+    <div class="num-row"><span class="num-label">L_NIAH ceiling ${ttip("tooltip.L_NIAH", "Predicted ceiling for needle-in-a-haystack retrieval reliability at the current d_horizon.")}</span><span class="num-value">${formatN(kn.L_NIAH_ceiling)}</span></div>
+    <div class="num-row"><span class="num-label">χ susceptibility ${ttip("tooltip.chi", "Susceptibility exponent χ = 1/(1−γ). Diverges at the Hagedorn line γ=1.")}</span><span class="num-value">${formatN(kn.chi_susceptibility)}</span></div>
+    <div class="num-row"><span class="num-label">KV memory @ T_eval (BF16) ${ttip("tooltip.kv_memory", "Per-request KV cache memory at T_eval in BF16 = 2 · n_layers · n_kv_heads · d_head · T_eval bytes.")}</span><span class="num-value">${formatN(kn.kv_memory_per_request_GB)} GB</span></div>
   `;
 
   const falsHtml = (p.falsification_status || []).map(f =>
     `<div class="taf-falsification"><strong>${escapeHtml(f.id)}</strong> — ${escapeHtml(f.claim)}: ${escapeHtml(f.status)}</div>`
   ).join("");
 
+  // Per-verdict count breakdown — recipes test orthogonal axes (long-context,
+  // budget, hardware, custom-vs-API, KV-compression). Worst-of-N would conflate
+  // a "use API" recommendation with a long-context failure, so we show counts.
+  const verdictCounts = Object.values(p.recipes).reduce((acc, r) => {
+    const c = verdictClass(r.verdict);
+    acc[c] = (acc[c] || 0) + 1;
+    return acc;
+  }, {});
+  const nYes = verdictCounts["v-yes"] || 0;
+  const nDeg = verdictCounts["v-deg"] || 0;
+  const nNo  = verdictCounts["v-no"]  || 0;
+  const breakdownCls = nNo ? "v-no" : nDeg ? "v-deg" : "v-yes";
+  const gammaForPill = kn.gamma_decomposed ?? kn.gamma_pade;
+  const recipeCount = Object.keys(p.recipes).length;
+
   $("profile-box").innerHTML = `
     <div class="taf-card">
-      <div class="taf-card-summary">
-        <div style="font-size:1.2rem; font-weight:700;">${escapeHtml(ms.architecture_class)}</div>
-        <div class="subtle">
+      <div class="taf-hero">
+        <div class="hero-arch">${escapeHtml(ms.architecture_class)}</div>
+        <div class="hero-meta">
           n_params=${formatN(ms.n_params)} ·
           T_train=${ms.T_train} · T_eval=${ms.T_eval} ·
           θ=${formatN(ms.rope_theta)} ·
           ${ms.has_GQA ? "GQA" : "MHA"}${ms.has_SWA ? " + SWA" : ""}
         </div>
-        ${(kn.gamma_decomposed ?? kn.gamma_pade) > 0 && (kn.gamma_decomposed ?? kn.gamma_pade) < 1
-          ? `<div class="taf-anti-ising-badge" style="margin-top:0.4em; display:inline-block; padding:0.25em 0.6em; border-radius:4px; background:rgba(110,80,200,0.15); border:1px solid rgba(110,80,200,0.4); font-size:0.85em;" data-i18n="v05.antiising.badge">
-              🧲 Anti-Ising class (β=γ−1&lt;0, machine-verified)
-            </div>`
-          : ''}
+        <div class="hero-row">
+          <span class="hero-pill ${breakdownCls}">✅ ${nYes} · ⚠ ${nDeg} · ❌ ${nNo} ${ttip("tooltip.verdict_breakdown", "Per-recipe breakdown across the orthogonal axes (long-context, budget, hardware, custom-vs-API, KV-compression). Recipes are independent decisions — a ❌ on X-1 means \"use API\" not \"model fails\". Open the Recipes section for per-axis verdict.")}</span>
+          ${gammaForPill !== null && gammaForPill !== undefined
+            ? `<span class="hero-pill">γ = ${formatN(gammaForPill)} ${ttip("tooltip.gamma_pill", "γ_decomposed (full architectural decomposition) or γ_Padé as fallback. Range (0,1) = Phase A (anti-Ising). γ ≥ 1 = Hagedorn / Phase B.")}</span>`
+            : ''}
+          ${gammaForPill > 0 && gammaForPill < 1
+            ? `<span class="hero-pill" style="background:rgba(110,80,200,0.15); border-color:rgba(110,80,200,0.45);"><span data-i18n="v05.antiising.badge">🧲 Anti-Ising (β=γ−1&lt;0, machine-verified)</span> ${ttip("tooltip.anti_ising", "Phase A class: β = γ−1 &lt; 0 (anti-Ising). Machine-verified by Sage Groebner basis + Lean Mathlib4. See §35 v0.5.")} ${badgesForUiBinding("anti_ising_pill")}</span>`
+            : ''}
+        </div>
       </div>
 
-      <h3 data-i18n="tafcard.recipes_title">📋 Recipes (verdict per dimension)</h3>
-      <div class="taf-recipes-grid">${recipesHtml}</div>
-
-      <h3 data-i18n="tafcard.numbers_title">🔢 Key numbers (paper §26)</h3>
-      <div class="taf-key-numbers">${numbersHtml}</div>
-
-      <details class="v053-audit-banner" style="margin:0.8em 0; padding:0.6em 0.8em; border:1px solid rgba(241,196,15,0.5); border-radius:6px; background:rgba(241,196,15,0.07); font-size:0.88em;">
-        <summary style="cursor:pointer; font-weight:600;" data-i18n="v053.calibration.title">🔬 v0.5.3 — Calibration audit (2026-05-02)</summary>
-        <div style="margin-top:0.5em; line-height:1.45;" data-i18n="v053.calibration.note"></div>
+      <details class="taf-section" open>
+        <summary>
+          <span data-i18n="tafcard.recipes_title">📋 Recipes — verdict per dimension</span>
+          <span class="section-count">${recipeCount} ${t("tafcard.recipes_count_label", "dimensions")}</span>
+        </summary>
+        <div class="taf-section-body">
+          <div class="taf-recipes-grid">${recipesHtml}</div>
+        </div>
       </details>
 
-      <div id="whatif-container" class="whatif-box"></div>
+      <details class="taf-section">
+        <summary>
+          <span data-i18n="tafcard.diag_title">🔬 Diagnostics — numbers + γ check + what-if</span>
+        </summary>
+        <div class="taf-section-body">
+          <h4 style="margin-top:0.3em;" data-i18n="tafcard.numbers_title">🔢 Key numbers (paper §26)</h4>
+          <div class="taf-key-numbers">${numbersHtml}</div>
+
+          <h4 style="margin-top:1.2em;" data-i18n="gamma_check.title">🔍 γ predicted vs observed</h4>
+          <div class="recipe-desc" data-i18n="gamma_check.desc">
+            Enter your empirically measured γ. Tool detects regime: fraud (θ inflated) / compressed / over-Padé / SWA-random / normal.
+          </div>
+          <div class="form-grid" style="margin:0.5em 0 0.6em;">
+            <div class="form-field">
+              <label><span data-i18n="gamma_check.gobs_label">γ_observed</span>
+                <span class="info"><span class="tooltip" data-i18n="gamma_check.gobs_tip">Empirically measured γ from your model's attention scores. Use the Diagnose CLI to obtain this from real weights.</span></span>
+              </label>
+              <input type="number" id="gc-gobs" step="0.0001" value="${formatN(kn.gamma_decomposed ?? kn.gamma_pade)}" />
+            </div>
+            <div class="form-field">
+              <label><span data-i18n="gamma_check.random_label">Random corpus?</span>
+                <span class="info"><span class="tooltip" data-i18n="gamma_check.random_tip">Tick if γ_observed was measured on random/unstructured tokens. Distinguishes SWA signature (γ_obs &gt; 1) from anomaly.</span></span>
+              </label>
+              <select id="gc-random">
+                <option value="false" selected data-i18n="common.no">No</option>
+                <option value="true" data-i18n="common.yes">Yes</option>
+              </select>
+            </div>
+          </div>
+          <div id="gamma-check-results"></div>
+
+          <h4 style="margin-top:1.2em;" data-i18n="tafcard.whatif_title">🎚️ What-if explorer</h4>
+          <div id="whatif-container" class="whatif-box"></div>
+        </div>
+      </details>
 
-      <h3 data-i18n="tafcard.fals_title">🔬 Falsification status (FALSIFICATION.md F1-F23)</h3>
-      ${falsHtml || '<div class="subtle">No falsifications applicable.</div>'}
+      <details class="taf-section">
+        <summary>
+          <span data-i18n="tafcard.verify_title">✓ Verification — Lean + Sage + falsification</span>
+        </summary>
+        <div class="taf-section-body">
+          <h4 style="margin-top:0.3em;" data-i18n="lean.table.title">📑 Lean+Mathlib theorem table</h4>
+          <div style="margin-bottom: 0.6em; opacity: 0.85; font-size: 0.92em;" data-i18n="lean.table.desc">
+            Every entry below is machine-proven against Lean 4 + Mathlib4. Click any L# link to jump to the source line on GitHub. The table is grouped by topic; click a header to expand.
+          </div>
+          <div id="lean-table-host"></div>
+
+          <h4 style="margin-top:1.2em;" data-i18n="v05.consistency.title">🔬 Algebraic consistency (Sage + Lean v0.5)</h4>
+          <div style="margin-bottom: 0.6em; opacity: 0.85; font-size: 0.92em;" data-i18n="v05.consistency.desc">
+            Verifies 12 D-SAGE algebraic identities of TAF critical exponents (machine-proof Sage Groebner basis + Lean Mathlib4). Pass = framework intact. Fail = bf16 outlier / quantization artifact.
+          </div>
+          <div class="lean-badges-row">${badgesForUiBinding("algebraic_consistency_check")}</div>
+          <button class="secondary" id="verify-consistency-btn" data-i18n="v05.consistency.btn">
+            🔬 Verify algebraic consistency
+          </button>
+          <div id="consistency-result" style="margin-top: 0.8em;"></div>
+
+          <h4 style="margin-top:1.2em;" data-i18n="tafcard.fals_title">🔬 Falsification status (F1-F23)</h4>
+          ${falsHtml || '<div class="subtle" data-i18n="tafcard.fals_none">No falsifications applicable.</div>'}
+        </div>
+      </details>
 
-      <h3 style="margin-top: 1.5em;" data-i18n="v05.consistency.title">🔬 Algebraic consistency check (Sage + Lean v0.5)</h3>
-      <div style="margin-bottom: 0.6em; opacity: 0.85; font-size: 0.92em;" data-i18n="v05.consistency.desc">
-        Verifies 12 D-SAGE algebraic identities of TAF critical exponents (machine-proof
-        Sage Groebner basis + Lean Mathlib4). Pass = framework intact. Fail = bf16 outlier
-        / quantization artifact.
-      </div>
-      <button class="secondary" id="verify-consistency-btn" data-i18n="v05.consistency.btn">
-        🔬 Verify algebraic consistency
-      </button>
-      <div id="consistency-result" style="margin-top: 0.8em;"></div>
-
-      <div class="share-bar">
-        <button class="secondary" id="profile-share-btn" data-i18n="share.btn">🔗 Copy share link</button>
-        <button class="secondary" id="profile-download-btn" data-i18n="share.download">💾 Download JSON</button>
-        <button class="secondary" id="profile-submit-btn" data-i18n="share.submit">📤 Submit to registry</button>
-        <span id="profile-share-status" class="subtle"></span>
-      </div>
+      <details class="taf-section">
+        <summary>
+          <span data-i18n="tafcard.share_title">📂 Provenance & share</span>
+        </summary>
+        <div class="taf-section-body">
+          <details style="margin:0.4em 0 0.8em; padding:0.6em 0.8em; border:1px solid rgba(241,196,15,0.5); border-radius:6px; background:rgba(241,196,15,0.07); font-size:0.88em;">
+            <summary style="cursor:pointer; font-weight:600;" data-i18n="v053.calibration.title">🔬 v0.5.3 — Calibration audit (2026-05-02)</summary>
+            <div style="margin-top:0.5em; line-height:1.45;" data-i18n="v053.calibration.note"></div>
+          </details>
+
+          <div class="share-bar">
+            <button class="secondary" id="profile-share-btn" data-i18n="share.btn">🔗 Copy share link</button>
+            <button class="secondary" id="profile-download-btn" data-i18n="share.download">💾 Download JSON</button>
+            <button class="secondary" id="profile-submit-btn" data-i18n="share.submit">📤 Submit to registry</button>
+            <span id="profile-share-status" class="subtle"></span>
+          </div>
+        </div>
+      </details>
     </div>
   `;
 
   // Render the what-if slider for interactive exploration
   renderWhatIfSlider(p, params, $("whatif-container"));
 
+  // Render Lean+Mathlib theorem table (graceful no-op if manifest missed).
+  // Loaded async at bootstrap; if Profile clicked before fetch resolves we
+  // wait once and then render.
+  const renderLeanTable = () => {
+    const host = $("lean-table-host");
+    if (!host) return;
+    if (getManifest()) {
+      host.innerHTML = renderTheoremTable();
+      if (window.__taf_applyTranslations) window.__taf_applyTranslations();
+    } else {
+      host.innerHTML = `<div class="subtle" data-i18n="lean.manifest.loading">Loading Lean manifest…</div>`;
+      loadLeanManifest()
+        .then(() => { host.innerHTML = renderTheoremTable(); if (window.__taf_applyTranslations) window.__taf_applyTranslations(); })
+        .catch(err => { host.innerHTML = `<div class="subtle" data-i18n="lean.manifest.error">Lean manifest unavailable: ${err.message}</div>`; });
+    }
+  };
+  renderLeanTable();
+
   // Re-apply translations to dynamically inserted buttons
   if (window.__taf_applyTranslations) window.__taf_applyTranslations();
 
@@ -1175,6 +1275,49 @@ function renderProfile(p, params) {
     setTimeout(() => $("profile-share-status").textContent = "", 6000);
   });
 
+  // v0.6: γ predicted-vs-observed panel — interactive
+  const updateGammaCheck = () => {
+    const gObs = parseFloat($("gc-gobs").value);
+    const isRandom = $("gc-random").value === "true";
+    const r = gammaCheckAll({ theta: params.theta, T: params.T_eval, gObs, isRandom });
+    const meta = REGIME_META[r.regime] || REGIME_META.unknown;
+    const fmt = (x, d=4) => (x === null || x === undefined || Number.isNaN(x))
+      ? "n/a"
+      : (!Number.isFinite(x) ? "∞" : Number(x).toLocaleString(undefined, { maximumFractionDigits: d }));
+    $("gamma-check-results").innerHTML = `
+      <div class="taf-key-numbers">
+        <div class="num-row"><span class="num-label">γ_Padé(T_eval) ${ttip("tooltip.gamma_pade", "Closed-form prediction (2−z)/(2+z), z = T√2/θ.")}</span><span class="num-value">${fmt(r.gammaPade)}</span></div>
+        <div class="num-row"><span class="num-label">θ_eff (observed) ${ttip("tooltip.theta_eff_obs", "Effective θ implied by your γ_observed: T√2 / (1 − γ_obs).")}</span><span class="num-value">${fmt(r.thetaEffObs, 1)}</span></div>
+        <div class="num-row"><span class="num-label">θ_eff (Padé) ${ttip("tooltip.theta_eff_pade", "Effective θ predicted by closed-form: θ + T/√2.")}</span><span class="num-value">${fmt(r.thetaEffPade, 1)}</span></div>
+        <div class="num-row"><span class="num-label">η = θ_eff_obs / θ_eff_Padé ${ttip("tooltip.efficiency", "Efficiency ratio. ≈1 = normal · &lt;0.01 = fraud · &lt;0.5 = compressed · &gt;1.5 = over-Padé.")}</span><span class="num-value">${fmt(r.efficiency)}</span></div>
+        <div class="num-row"><span class="num-label">ΔH_Cardy = log(θ_eff_obs / θ_nominal) ${ttip("tooltip.delta_h_cardy", "Cardy entropy shift. Negative = compression entropy. ~0 = nominal match.")}</span><span class="num-value">${fmt(r.deltaHCardy)}</span></div>
+      </div>
+      <div class="taf-recipe-tile ${meta.cls}" style="margin-top:0.6em;">
+        <div class="tile-header">
+          <span data-i18n="gamma_check.regime">Regime</span>
+          <span class="tile-verdict">${meta.emoji} <span data-i18n="gamma_check.regime.${r.regime}">${r.regime}</span></span>
+        </div>
+        <div class="tile-reason" data-i18n="gamma_check.regime.${r.regime}.desc"></div>
+      </div>
+      <details style="margin-top:0.6em;">
+        <summary style="cursor:pointer; font-weight:600;" data-i18n="gamma_check.glossary.title">ⓘ What do these mean?</summary>
+        <ul class="gc-glossary" style="margin:0.5em 0 0 1.2em; line-height:1.55;">
+          <li data-i18n="gamma_check.glossary.gamma_pade"></li>
+          <li data-i18n="gamma_check.glossary.gamma_obs"></li>
+          <li data-i18n="gamma_check.glossary.theta_eff_obs"></li>
+          <li data-i18n="gamma_check.glossary.theta_eff_pade"></li>
+          <li data-i18n="gamma_check.glossary.efficiency"></li>
+          <li data-i18n="gamma_check.glossary.delta_h"></li>
+          <li data-i18n="gamma_check.glossary.regime"></li>
+        </ul>
+      </details>
+    `;
+    if (window.__taf_applyTranslations) window.__taf_applyTranslations();
+  };
+  $("gc-gobs").addEventListener("input", updateGammaCheck);
+  $("gc-random").addEventListener("change", updateGammaCheck);
+  updateGammaCheck();
+
   // v0.5.1: Algebraic consistency check button
   $("verify-consistency-btn").addEventListener("click", () => {
     const gammaVal = kn.gamma_decomposed ?? kn.gamma_pade;
@@ -1667,6 +1810,9 @@ document.addEventListener("DOMContentLoaded", () => {
       if (file) importJSON(file, document.getElementById("import-status"));
     });
   }
+  // Lean+Mathlib manifest — load in parallel with everything else; badges
+  // appear once it resolves, but app stays usable if it fails.
+  loadLeanManifest().catch(err => console.warn("Lean manifest unavailable:", err));
 });
 
 // ════════════════════════════════════════════════════════════════════

style.css

@@ -590,3 +590,182 @@ footer a:hover { text-decoration: underline; }
   margin: 0.6em 0;
   overflow-x: auto;
 }
+
+/* ─── TAF Card accordion sections (v0.6 — UX restructuring) ─── */
+.taf-section {
+  margin: 0.7em 0;
+  border: 1px solid var(--border);
+  border-radius: 6px;
+  background: rgba(255,255,255,0.018);
+  overflow: hidden;
+}
+.taf-section > summary {
+  cursor: pointer;
+  list-style: none;
+  padding: 0.7em 0.95em;
+  font-weight: 600;
+  font-size: 1.02em;
+  user-select: none;
+  display: flex;
+  align-items: center;
+  gap: 0.5em;
+  transition: background 0.12s;
+}
+.taf-section > summary:hover { background: rgba(255,255,255,0.04); }
+.taf-section > summary::-webkit-details-marker { display: none; }
+.taf-section > summary::before {
+  content: "▶";
+  display: inline-block;
+  font-size: 0.7em;
+  color: var(--fg-dim);
+  transition: transform 0.15s ease;
+  width: 0.8em;
+  text-align: center;
+}
+.taf-section[open] > summary::before { transform: rotate(90deg); }
+.taf-section > summary .section-count {
+  margin-left: auto;
+  font-size: 0.82em;
+  color: var(--fg-dim);
+  font-weight: 500;
+}
+.taf-section-body {
+  padding: 0.4em 1em 1em 1em;
+  border-top: 1px solid var(--border);
+  background: var(--bg);
+}
+/* Hero strip — always-visible top-line summary */
+.taf-hero {
+  padding: 0.9em 1em;
+  border: 1px solid var(--border);
+  border-radius: 6px;
+  background: linear-gradient(135deg, rgba(110,80,200,0.06), rgba(255,255,255,0.02));
+  margin-bottom: 0.4em;
+}
+.taf-hero .hero-arch { font-size: 1.15rem; font-weight: 700; }
+.taf-hero .hero-meta { color: var(--fg-dim); font-size: 0.88em; margin-top: 0.25em; }
+.taf-hero .hero-row {
+  display: flex; flex-wrap: wrap; gap: 0.5em 1em;
+  align-items: center; margin-top: 0.5em;
+}
+.taf-hero .hero-pill {
+  display: inline-flex; align-items: center; gap: 0.35em;
+  padding: 0.2em 0.6em; border-radius: 999px;
+  font-size: 0.85em; font-weight: 600;
+  background: var(--bg-input);
+  border: 1px solid var(--border);
+}
+.taf-hero .hero-pill.v-yes { color: var(--success); border-color: var(--success); }
+.taf-hero .hero-pill.v-no  { color: var(--danger);  border-color: var(--danger); }
+.taf-hero .hero-pill.v-deg { color: var(--warning); border-color: var(--warning); }
+
+/* ─── Lean+Mathlib provenance (v0.6) ─── */
+.lean-badge {
+  display: inline-block;
+  padding: 0.08em 0.45em;
+  margin: 0 0.15em;
+  border: 1px solid rgba(110,80,200,0.45);
+  background: rgba(110,80,200,0.10);
+  border-radius: 4px;
+  color: var(--accent, #b48cff);
+  text-decoration: none;
+  font-size: 0.78em;
+  font-family: monospace;
+  vertical-align: middle;
+  white-space: nowrap;
+}
+.lean-badge:hover {
+  background: rgba(110,80,200,0.22);
+  text-decoration: none;
+}
+.lean-badges-row {
+  margin: 0.4em 0 0.6em;
+  line-height: 1.9;
+}
+.lean-meta {
+  font-size: 0.88em;
+  margin-bottom: 0.6em;
+  padding: 0.5em 0.7em;
+  background: rgba(255,255,255,0.02);
+  border-left: 3px solid var(--accent);
+  border-radius: 4px;
+}
+.lean-meta a { color: var(--accent); }
+.lean-findings {
+  margin: 0.6em 0 0.8em;
+  padding: 0.5em 0.7em;
+  border: 1px solid rgba(241,196,15,0.4);
+  background: rgba(241,196,15,0.06);
+  border-radius: 6px;
+}
+.lean-findings > summary {
+  cursor: pointer;
+  font-size: 1em;
+}
+.lean-finding {
+  margin: 0.6em 0;
+  padding: 0.6em 0.7em;
+  border-left: 3px solid var(--warning);
+  background: rgba(255,255,255,0.025);
+  border-radius: 0 4px 4px 0;
+}
+.lean-pill {
+  display: inline-block;
+  margin-left: 0.4em;
+  padding: 0.05em 0.45em;
+  font-size: 0.75em;
+  border-radius: 999px;
+  border: 1px solid var(--border);
+  text-transform: uppercase;
+  letter-spacing: 0.04em;
+}
+.lean-pill.v-deg { color: var(--warning); border-color: var(--warning); }
+.lean-groups .lean-group {
+  margin: 0.4em 0;
+  border: 1px solid var(--border);
+  border-radius: 4px;
+  background: var(--bg);
+}
+.lean-group > summary {
+  cursor: pointer;
+  padding: 0.5em 0.7em;
+  user-select: none;
+  font-weight: 600;
+  list-style: none;
+}
+.lean-group > summary::-webkit-details-marker { display: none; }
+.lean-group > summary::before {
+  content: "▶ ";
+  font-size: 0.7em;
+  color: var(--fg-dim);
+  transition: transform 0.15s;
+}
+.lean-group[open] > summary::before {
+  content: "▼ ";
+}
+.lean-table-wrap {
+  max-height: 380px;
+  overflow: auto;
+  border-top: 1px solid var(--border);
+}
+.lean-table {
+  width: 100%;
+  border-collapse: collapse;
+  font-size: 0.85em;
+}
+.lean-table th, .lean-table td {
+  padding: 0.4em 0.6em;
+  text-align: left;
+  vertical-align: top;
+  border-bottom: 1px solid var(--border);
+}
+.lean-table th {
+  position: sticky;
+  top: 0;
+  background: var(--bg-input);
+  color: var(--accent);
+  font-family: monospace;
+  z-index: 1;
+}
+.lean-table tbody tr:hover { background: rgba(255,255,255,0.03); }
+.lean-table code { font-size: 0.95em; }