docs+lint: safer forms are not semantic equivalents

docs/design-principles.md

@@ -96,9 +96,13 @@ the phased build plan should be traceable back to one of these.
   volatile-default `ADD COLUMN`, `STORED` generated columns, repack). "Needs copy-and-swap? =
   No" never means "don't use the engine" — it means the engine runs the native idiom for you.
 - **Advise, never silently run the dangerous literal; force is loud and explicit.** When a
-  submitted statement is risky as written but has a safer native equivalent (`CREATE INDEX` →
+  submitted statement is risky as written but has a safer native form (`CREATE INDEX` →
   `CREATE INDEX CONCURRENTLY`, etc.), the engine surfaces the recommendation and applies the
-  safe idiom — it does **not** execute the risky literal behind the user's back. Running a
+  safe idiom — it does **not** execute the risky literal behind the user's back. The safer
+  form reaches the same end state but is not a semantic equivalent — it has different locking,
+  transactionality, and failure modes, which is exactly why the engine (not the user) owns
+  running it (see the
+  [online DDL reference](postgres-online-ddl-reference.md)). Running a
   statement exactly as submitted requires an explicit `--force`, gated by prominent DANGER/CAUTION
   output, a typed acknowledgement (not a bare `-y`), and an audit log entry. Force is an escape
   hatch, not a convenience (see

docs/high-level-design.md

@@ -185,7 +185,7 @@ diff algorithm and its safety rules are detailed in the
 ## Advisory mode: suggest the safe rewrite, don't silently run the risky one
 
 The classifier doesn't only choose an execution path — it can also act as a **suggestion
-engine**. When a submitted statement is risky *as written* but has a safer native equivalent,
+engine**. When a submitted statement is risky *as written* but has a safer native form,
 the engine's default is to **return the recommendation and stop**, rather than execute the
 literal statement:
 
@@ -202,7 +202,7 @@ literal statement:
    ┌──────────────────────────────────────────────────────────-┐
    │  RECOMMENDATION (does NOT execute):                       │
    │   you asked:   CREATE INDEX idx ON orders (customer_id)   │
-   │   run instead: CREATE INDEX CONCURRENTLY idx ON orders …  │
+   │   safer form:  CREATE INDEX CONCURRENTLY idx ON orders …  │
    │   why: a plain CREATE INDEX takes SHARE and blocks writes │
    │        for the whole build; CONCURRENTLY does not.        │
    └──────────────────────────────────────────────────────────-┘
@@ -223,10 +223,15 @@ Examples of what it suggests (the same idioms the classifier already knows):
 
 Two principles govern this:
 
-- **Never silently execute the dangerous literal.** If a safer equivalent exists, the engine
+- **Never silently execute the dangerous literal.** If a safer form exists, the engine
   surfaces it rather than running the risky form behind the user's back. This is the
   transparent, review-friendly counterpart to *classify-first* — the user still doesn't need to
-  know the idiom (the engine names it), but nothing dangerous runs unannounced.
+  know the idiom (the engine names it), but nothing dangerous runs unannounced. The safer form
+  is not a semantic equivalent: it reaches the same end state with different locking,
+  transactionality, and failure modes (a failed `CONCURRENTLY` build leaves an `INVALID` index
+  that must be detected and rebuilt — see the
+  [online DDL reference](postgres-online-ddl-reference.md)), which is why the engine owns
+  executing it rather than handing it to the user to run manually.
 - **The planned force route is loud and explicit.** Phase 3 adds a `--force`
   (run-as-submitted) flag for the rare case where the operator genuinely wants the literal
   statement. It will be gated behind

docs/low-level-design.md

@@ -297,9 +297,13 @@ For each parsed statement the classifier produces a record along the lines of:
 - `original` — the statement as the user wrote it.
 - `class` — `native-safe` · `needs-rewrite` (refused until in-house copy-and-swap lands) ·
   `refuse`.
-- `recommended` — the safe rewrite when the literal is risky but has a native equivalent
+- `recommended` — the safer native form when the literal is risky as written
   (e.g. `CREATE INDEX` → `CREATE INDEX CONCURRENTLY`; `ADD CONSTRAINT` → `ADD … NOT VALID` +
   `VALIDATE`; `ADD PRIMARY KEY` → unique index `CONCURRENTLY` + `ADD PRIMARY KEY USING INDEX`).
+  The recommendation converges on the same declared end state but is **not** a semantic
+  equivalent of the original — it carries different locking, transactionality, and failure
+  modes (a failed `CONCURRENTLY` build leaves an `INVALID` index the executor must detect via
+  `pg_index.indisvalid` and recover), so executing it is the engine's job, not the user's.
 - Richer `risk`, `reversible`, and `requires_app_coordination` metadata is a future extension.
 
 Classification belongs to `pkg/planner`; `pkg/statement` supplies typed operations and

internal/cli/diff.go

@@ -173,7 +173,7 @@ func writeChangeText(out io.Writer, ps plan.Statement) error {
 		return fmt.Errorf("write plan: %w", err)
 	}
 	if len(ps.ExecSQL) > 0 && ps.ExecSQL[0] != ps.SQL {
-		if _, err := fmt.Fprintln(out, "-- the engine would run instead:"); err != nil {
+		if _, err := fmt.Fprintln(out, "-- safer form the engine would run (not equivalent — see docs/postgres-online-ddl-reference.md):"); err != nil {
 			return fmt.Errorf("write plan: %w", err)
 		}
 		for _, safer := range ps.ExecSQL {

internal/cli/lint.go

@@ -56,7 +56,7 @@ func writeLintText(out io.Writer, report lint.Report) error {
 			return fmt.Errorf("write lint report: %w", err)
 		}
 		if len(f.Suggestion) > 0 {
-			if _, err := fmt.Fprintf(out, "  run instead: %s;\n",
+			if _, err := fmt.Fprintf(out, "  safer form (not equivalent — see docs/postgres-online-ddl-reference.md): %s;\n",
 				strings.Join(f.Suggestion, ";\n  ")); err != nil {
 				return fmt.Errorf("write lint report: %w", err)
 			}

pkg/lint/lint.go

@@ -42,7 +42,9 @@ const (
 	CodeUnsupportedOperation Code = "unsupported-operation"
 	// CodeBlockingIdiom: the submitted form blocks readers or writers and
 	// a safer native form exists; Suggestion carries it when the linter
-	// can construct one.
+	// can construct one. The safer form is not a semantic equivalent —
+	// a CONCURRENTLY build is non-transactional and a failure leaves an
+	// invalid index the engine detects and rebuilds at execution time.
 	CodeBlockingIdiom Code = "blocking-idiom"
 	// CodeTableRewrite: the operation needs a full table rewrite — only
 	// the engine's copy-and-swap path can run it online. Reason carries
@@ -70,8 +72,11 @@ type Finding struct {
 	// Reason is the classifier's typed cause, present for findings the
 	// classifier produced (blocking-idiom, table-rewrite, unsupported).
 	Reason planner.Reason `json:"reason,omitempty"`
-	// Suggestion is the ordered safer SQL to run instead, present only
-	// for blocking-idiom findings where the linter could construct it.
+	// Suggestion is the ordered safer SQL, present only for
+	// blocking-idiom findings where the linter could construct it. It is
+	// advisory: a safer form, not a semantic equivalent — running it by
+	// hand forgoes the engine's execution-time guards (invalid-index
+	// detection after a concurrent build).
 	Suggestion []string `json:"suggestion,omitempty"`
 }
 

pkg/planner/planner.go

@@ -95,7 +95,11 @@ type Decision struct {
 	Reason Reason `json:"reason"`
 	// SaferSQL is the ordered native sequence to run instead of the
 	// submitted form, present only for safer-idiom decisions where the
-	// planner could construct it.
+	// planner could construct it. It is a safer form, not a semantic
+	// equivalent: a CONCURRENTLY build runs outside a transaction and a
+	// failure leaves an invalid index that must be detected
+	// (pg_index.indisvalid) and rebuilt — the executor owns that check
+	// (see docs/postgres-online-ddl-reference.md).
 	SaferSQL []string `json:"safer_sql,omitempty"`
 }
 
@@ -210,7 +214,10 @@ func classifyOp(op statement.Op, st statement.Statement, facts Facts, sql string
 
 // concurrentlyDecision routes an operation that is online in its
 // CONCURRENTLY form: already concurrent is the idiom; otherwise native with
-// the concurrent rewrite as the safer sequence.
+// the concurrent rewrite as the safer sequence. The rewrite trades the
+// blocking lock for a different failure mode — non-transactional, and a
+// failed build leaves an invalid index — which the executor, not the
+// planner, guards.
 func concurrentlyDecision(d Decision, concurrent bool, sql string, single bool) Decision {
 	if concurrent {
 		d.Route, d.Reason = RouteNative, ReasonOnlineIdiom