refactor(skills): orthogonalize formalize-coarse and formalize-fine

gaia/_skills/_shared/formalize-atomicity.md

@@ -0,0 +1,130 @@
+# Claim atomicity
+
+Shared reference for `gaia-formalize-coarse` and `gaia-formalize-fine`. Both
+skills decompose a paper into atomic claims; this file is the single canonical
+statement of what "atomic" means and how to test for it. Reference, not
+procedure — it has no frontmatter and is not itself a skill.
+
+A claim's *mechanics* — whether it is held in working notes or written
+straight to DSL, what label it gets, which module it lands in — belong to the
+calling skill. This file owns only the question: **is this one claim, or
+several?**
+
+## The principle
+
+Each claim states **exactly one thing**: it answers exactly one citable
+epistemic question about the paper — one new bound, one new relation, one new
+procedure, one new measured value, one new comparison outcome, one new causal
+attribution, one new generalization result. If a candidate body answers two,
+split it into two claims.
+
+The rule is **field-agnostic**. The same one-question-per-claim discipline
+applies whether the paper is a theorem in pure mathematics, a clinical-trial
+endpoint in medicine, a benchmark result in machine learning, a causal
+estimate in social science, or a measurement in experimental physics.
+
+## Two corollaries that catch most violations
+
+The most common atomicity failures are two specific fusion patterns. Each is
+just the one-question test applied to a recurring shape.
+
+### Separate theory from experiment
+
+A theoretical prediction and the experimental measurement it is compared
+against are **two claims, never one**. They answer different citable
+questions, carry different evidence, and have different weak points. A claim
+that fuses them also cannot be wired to a verification relation later.
+
+```python
+# BAD — theory and experiment fused
+result = claim("The model predicts X, the experimental value is Y, deviation Z%.")
+
+# GOOD — two independently judgeable claims
+prediction  = claim("Based on method M, the model predicts quantity Q = X.")
+measurement = claim("The experimental measurement of quantity Q is Y.")
+```
+
+### Separate method from result
+
+A method or procedure description and the value that applying it produced are
+**two claims**. The method is a contribution a later paper could reuse for a
+different outcome; the value is an empirical result a different method could
+equally have produced.
+
+```python
+# BAD — method and result fused
+result = claim("Using method M to compute Q yields Z.")
+
+# GOOD
+method = claim("Method M employs ... strategy ...")
+result = claim("The numerical result for Q is Z ± δ.")
+```
+
+## Common under-splitting traps
+
+Each trap is illustrated with examples from different fields to make clear
+that the trap is structural, not domain-specific.
+
+- **Definition + headline result.** A new bound (e.g. "the scheme is
+  parametrically valid when $\omega_D \ll E_F$, $\omega_c^2 \ll \omega_p^2$,
+  $T \ll \omega_c$") and the downstream result that uses it are *two* claims —
+  the bound is a citable regime claim on its own. Outside physics, the same
+  trap appears in a clinical RCT that introduces a new operational criterion
+  alongside its prevalence: "the protocol's prespecified no-disease-activity
+  criterion at week 24 (combining OCT central-subfield thickness, BCVA,
+  hemorrhage status, and investigator judgment) is met by 65% of treated
+  participants" is two claims — the criterion is a methodological
+  contribution citable by anyone designing a similar regimen, separate from
+  the empirical prevalence it yielded in this cohort.
+- **Procedure + the value it produced.** "Cluster-DiagMC achieves
+  γ~$10^5$ at $n=6$ and reproduces $P(0,0)=0.0504(3)$" is two claims: the
+  algorithm's measured speedup, and the agreement with the polarization
+  baseline. Each has different evidence and different weak points. Outside
+  physics, the same trap appears in a clinical RCT conclusion that bundles
+  regimen with outcome: "faricimab dosed every 16 weeks after a four-monthly
+  loading phase produces +11.4 ETDRS letters at week 52 with a mean of 6.2
+  injections" is two — the dosing regimen is a methodological contribution
+  downstream trials could reuse for a different outcome, and the measured
+  BCVA change is an empirical efficacy result a different regimen could
+  equally have produced.
+- **Theorem + worked example.** A general formal claim and the explicit
+  worked-example calculation that motivates it (e.g. "the third-order
+  four-diagram cancellation drops by $\sim 3.48 \times 10^{-3}$") are two
+  claims when the worked example is a separate quantitative finding. Outside
+  physics, the same trap appears in causal-inference methodology papers: a
+  new identifiability theorem for an estimand under stated assumptions, and a
+  worked example applying the resulting estimator to a specific
+  competing-events dataset to produce a numerical estimate, are two claims —
+  the theorem is a formal contribution citable by anyone working with that
+  estimand class, and the worked example is an empirical instantiation.
+- **Mechanism + benchmark.** "The downfolded Migdal–Eliashberg equation
+  reproduces the toy-model $T_c$ to within $0.2\%$" — the mechanism (the
+  equation) is one claim; the benchmark agreement is another. Outside
+  physics, the same trap appears in algorithmic system papers: "DVL
+  pre-integration is linearized in the rotation update, avoiding full
+  re-integration inside the nonlinear solver, and AQUA-SLAM achieves lower
+  translation RMSE than five baselines on the WaveTank dataset" is two — the
+  linearization mechanism is a methodological contribution downstream SLAM
+  systems could adopt with a different baseline set, and the WaveTank RMSE
+  comparison is an empirical benchmark result.
+
+## Two tests
+
+**Split test.** After writing a candidate body, ask: *if I deleted any one
+clause, would I lose an answer to a distinct citable question?* If yes, split
+that clause off. If the body merely loses an aside that does not answer its
+own citable question, it is one claim.
+
+**Standalone-citation test.** Would each candidate stand on its own as a
+sentence the paper could have published as a stand-alone bullet in the
+abstract? If yes, it is atomic. If two candidates can only be cited together
+(one is an aside of the other), they are one.
+
+## Do not pre-classify while splitting
+
+Atomicity is only about the one-question split. While splitting, do **not**
+pre-classify a claim by "type" (analytical / empirical / methodological) and
+do **not** pre-assign it a weak-point pattern. A single claim typically rests
+on several reasoning patterns at once; type and weak-point classification
+happen later, per the calling skill's own workflow. Atomicity work has
+exactly one job: enforce the one-question-per-claim split.

gaia/_skills/_shared/formalize-extract-conclusions.md

@@ -0,0 +1,137 @@
+# Extracting a paper's conclusions
+
+Shared reference for `gaia-formalize-coarse` and `gaia-formalize-fine`. Both
+skills begin by reading the paper and identifying its genuine new
+contributions as claims; this file is the canonical statement of *what* to
+extract and *how each extracted claim must read*. Reference, not procedure —
+no frontmatter, not itself a skill.
+
+This file does **not** own extraction mechanics — working notes vs incremental
+DSL, module layout, the `note` / `question` node kinds, label minting — those
+belong to the calling skill. Atomicity (one claim = one question) has its own
+file, `formalize-atomicity.md`.
+
+## What counts as a conclusion
+
+A conclusion is **new author-asserted knowledge that would not exist if this
+paper had not been written**:
+
+- a newly derived formula, theoretical relation, or analytical result;
+- a quantitatively new numerical or experimental value, scaling law, phase
+  boundary, or benchmark;
+- a newly proposed algorithm, computational scheme, or experimental method.
+
+It is **not**:
+
+- a restatement of prior work;
+- a trivial corollary of the paper's own assumptions;
+- a rhetorical claim of importance, motivation, or future work;
+- a reformulation that adds no information.
+
+## Fidelity to the paper
+
+The paper text is the only source of truth. While extracting:
+
+- Do not strengthen heuristic claims into established facts.
+- Do not supply missing derivations or repair broken arguments.
+- Do not import outside knowledge, even to "fix" an undefined symbol — leave
+  it undefined and surface the gap.
+- Preserve the authors' epistemic hedging exactly: regimes, error bars,
+  speculative qualifiers, modal force ("suggests" stays "suggests").
+
+## Write every claim self-contained
+
+Each claim body must be a complete proposition a reviewer can judge without
+reading the paper or any other claim:
+
+- **Symbols** — every mathematical symbol gets a brief meaning on first use in
+  that body (`$\alpha$ (ratio of XX to YY)`), not bare (`$\alpha \ll 1$`).
+  Each claim is independent; re-explain a symbol even if another claim already
+  did.
+- **Acronyms** — expanded on first use in that body, every time.
+- **Setup** — the system / model / dataset / regime is described inside the
+  proposition, not assumed.
+- **Concrete subject** — every sentence's subject is the model, the
+  estimator, the measurement — never "the paper" or "this work".
+- **No bare comparatives** — not "significantly larger than X" or "nearly
+  exact agreement"; give both numbers.
+- **Inline values, not pointers** — write the equation, the value, the setup
+  into the body; never "Eq. (3)" or "Fig. 4" (see "No paper-internal
+  pointers" below).
+
+## Content format
+
+Claim bodies support Markdown — use it for structure:
+
+- **Tables** — Markdown tables for structured data.
+- **Math** — `$...$` inline, `$$...$$` display. LaTeX, not Unicode math
+  symbols.
+- **Lists** — bullets to enumerate conditions or items.
+- **Emphasis** — bold / italic for key values or terms.
+
+## Figures and tables → inline as prose
+
+The paper Markdown does not carry figure pixels. When the paper's argument
+relies on what a figure or table shows, transcribe the quantitative content
+into the claim body: the specific values, the curve shape, the trend, the
+comparison.
+
+```python
+tc_data = claim(
+    "Measured superconducting transition temperatures:\n\n"
+    "| Material | $T_c$ (K) | Pressure (GPa) |\n"
+    "|----------|-----------|----------------|\n"
+    "| LaH10    | 250       | 200            |\n"
+    "| H3S      | 203       | 150            |",
+    title="Tc measurements",
+)
+```
+
+The claim body carries everything needed for judgement. A figure/table
+reference in `metadata` is for **traceability only**, never for conveying
+information the body omitted.
+
+## No paper-internal pointers; refs whitelist
+
+Structural pointers into the paper — `Eq. (5)`, `Fig. 3`, `Table I`,
+`Sec. II`, `Appendix A`, `Theorem 2`, `Lemma M`, footnotes — must not appear
+inside a claim body. Resolve every such pointer by inlining its content.
+
+For traceability, note the figures / tables / equations / external citations
+that primarily evidence each conclusion. The **only three** pointer kinds that
+may be retained (as `refs` metadata) are:
+
+- **`figure`** — a figure or table (`Fig. 2`, `Table I`).
+- **`equation`** — an equation referenced by number (`Eq. (5)`).
+- **`citation`** — an external bibliographic reference. Convert the paper's
+  numeric citations (`[33]`, `Ref. 5`) to a key of first-author surname plus
+  year (`Smith2020`); the same key goes into `references.json`.
+
+Section / appendix / paragraph / theorem / lemma / footnote pointers are
+**not** legitimate `refs` entries — inline their content instead.
+
+## Citation form in prose
+
+External citations in any prose (claim bodies, rationales) use the `[@key]`
+form, where `key` matches an entry in `references.json`
+(`<FirstAuthorSurname><Year>`, e.g. `[@Smith2020]`). Never leave numeric
+paper-style citations (`[33]`, `Ref. 5`, `Smith et al., 2020`) in prose;
+convert at write time. If a key cannot be derived from the paper's
+bibliography, use bare `@unknown_<n>` (**no brackets** — bracketed
+`[@unknown_n]` fails the compiler's strict-reference check; bare `@key` is
+opportunistic) and surface the gap. The full citation contract lives in
+`docs/for-users/language-reference.md`.
+
+## Extract both sides of every comparison
+
+When the paper compares a theoretical prediction against an experimental
+observation, extract **both** as separate claims (atomicity requires this too
+— see `formalize-atomicity.md`), so the verification relation can be wired
+later. When several competing theories are compared against one observation,
+extract **each** competing prediction as its own claim.
+
+When the paper argues one general rule is confirmed by repeated independent
+observations (multiple samples, labs, conditions), extract **each
+observation** as its own claim plus the candidate rule as its own claim. The
+wiring — and the independence judgement those observations must satisfy — is
+covered in `formalize-reasoning-chains.md` and `formalize-independence.md`.

gaia/_skills/_shared/formalize-independence.md

@@ -0,0 +1,125 @@
+# Evidence independence — no double counting
+
+Shared reference for `gaia-formalize-coarse` and `gaia-formalize-fine`. Both
+skills must ensure each reasoning relation they emit encodes a genuinely
+independent constraint. This file is the canonical statement of the
+independence check. Reference, not procedure — no frontmatter, not itself a
+skill.
+
+## The principle
+
+Gaia runs exact inference (Junction Tree) — given any factor graph it computes
+correct posteriors. There is no algorithmic double counting. Every issue here
+is about whether the **model** matches reality: each relation must represent a
+constraint that brings genuinely new information no other relation already
+provides. When the same evidence enters a conclusion twice, the model claims
+two independent constraints where only one exists, and beliefs inflate.
+
+When an implicit dependency exists, make it **explicit** as a node in the
+graph so inference can reason about it correctly.
+
+The independence check applies to whatever relation verbs a skill emits — a
+`derive`-only reduced model and a full `derive` / `infer` / `compute` /
+`decompose` model are both subject to it. Patterns below that name a specific
+verb apply only to skills that emit that verb.
+
+## Pattern 1 — Redundant relations (same reasoning expressed twice)
+
+```python
+# 1a. Exact duplicate — the same support stated standalone and inside a wider relation
+derive(law, given=[obs])
+derive(law, given=[obs_a, obs_b, obs])   # re-uses obs
+# FIX: drop the standalone relation, or fold it into the wider one.
+
+# 1b. Transitive shortcut — an A→B→C chain plus an A→C that is just the chain compressed
+derive(B, given=[A]); derive(C, given=[B]); derive(C, given=[A])
+# FIX: drop the shortcut, OR confirm it is a genuinely different argument.
+
+# 1c. Derived-premise redundancy — A→B, then C given [A, B] where A reaches C only through B
+derive(B, given=[A]); derive(C, given=[A, B])
+# FIX: drop A from C's premises → derive(C, given=[B]).
+```
+
+## Pattern 2 — Hidden evidence in rationale text
+
+Two relations with identical premises but different `rationale` prose: the
+differing prose contains evidence not captured as a premise. Extract it.
+
+```python
+# BEFORE — same premises, different reasoning angles
+derive(law, given=[sample, obs_R], rationale="Zero resistance = SC hallmark")
+derive(law, given=[sample, obs_R], rationale="Transition width < 0.5 K = bulk SC")
+
+# AFTER — the hidden "transition width" evidence becomes its own claim
+transition_sharpness = claim("Resistivity transition width < 0.5 K")
+derive(law, given=[sample, obs_R], rationale="Zero resistance = SC hallmark")
+derive(law, given=[sample, transition_sharpness], rationale="Sharp transition = bulk SC")
+```
+
+## Pattern 3 — Unmodelled shared dependencies
+
+Two observations share a common cause (same sample, same instrument) but the
+cause is not in the graph: the model treats them as unconditionally
+independent and loses their correlation.
+
+```python
+# BEFORE — shared sample quality implicit, correlation lost
+derive(law, given=[obs_R, obs_chi])
+
+# AFTER — extract the shared cause; correlation preserved
+sample_quality = claim("Sample A is a high-quality single crystal, confirmed by XRD")
+derive(obs_R,   given=[sample_quality])
+derive(obs_chi, given=[sample_quality])
+derive(law,     given=[obs_R, obs_chi], rationale="Conditionally independent given sample_quality")
+```
+
+You cannot create new experiments — you formalize what the paper provides:
+
+| Observation relationship | Modelling approach |
+|---|---|
+| Truly independent (different samples / labs) | Use the observations directly as parallel premises |
+| Partially independent (shared dependency + independent components) | Extract the shared dependency as an explicit claim |
+| Completely redundant (same data rephrased) | Merge into a single claim |
+
+## Pattern 4 — `equal` plus separate relations (structural-verb skills only)
+
+When `equal(a, b)` couples two claims and both sides also relate to the same
+target, check each relation brings information beyond what `equal` already
+propagates.
+
+```python
+equal(claim_A, claim_B)
+derive(law, given=[claim_A]); derive(law, given=[claim_B])
+# Does B→law add anything A→law + equal does not already give?
+# NO  → drop B→law.   YES → extract the extra information as a new premise.
+```
+
+## Shared-factor extraction
+
+If two supports on the same target share an underlying factor — same
+approximation, same dataset, same lemma, same external assumption — extract
+the shared factor as its own claim and let both supports depend on that one
+factor, rather than letting the factor's uncertainty enter the target twice.
+
+## Repeated observations must be independent
+
+When a general rule is supported by several observations, each must provide
+**independent** evidence. If they share a sample, instrument, or pipeline,
+that shared dependency is a Pattern 3 case — extract it as an explicit claim
+before treating the observations as parallel support.
+
+## How to check
+
+1. List every claim with 2+ incoming relations.
+2. For each pair of relations into it: does each bring genuinely independent
+   new information?
+3. For each relation over multiple observations: do the observations share an
+   unmodelled dependency?
+4. For each `equal`: do both sides need their own relation to the same target?
+5. For every relation: does the `rationale` prose contain evidence not
+   captured as a premise?
+
+After any independence fix, re-run inference and compare beliefs. A
+significant belief drop after removing a relation confirms the previous value
+was inflated by double counting. For reading the resulting beliefs, see
+`bp-interpretation.md`.