decision 14: no application in term position, spec example rewritten flat

3 files changed, 58 insertions, 4 deletions

diff --git a/README.org b/README.org
index 40d59e2..cd6149c 100644
--- a/README.org
+++ b/README.org
@@ -70,7 +70,10 @@ It covers:
   with checkers verified in Rocq;
 - the catalog as ordinary queryable relations;
 - subtyping as proven relation inclusion, intensional relation
-  identity, and canonical representatives for quotient domains.
+  identity, and canonical representatives for quotient domains;
+- applications as propositions everywhere: no relation application
+  in term position, statements about results written flat as
+  membership.
 
 ** Core Design Principles and Pipeline Specification
 
diff --git a/docs/language-specification.org b/docs/language-specification.org
index 9158130..639e8d6 100644
--- a/docs/language-specification.org
+++ b/docs/language-specification.org
@@ -1152,12 +1152,20 @@ For example:
 #+BEGIN_SRC sol
 [ForAll variable: X
         quantifier: [Integer value: X]
-        body:
-          [Equal left: [Plus left: X right: 0] right: X]]
+        body: [Plus left: X right: 0 result: X]]
 #+END_SRC
 
+This says that the tuple ={left: X, right: 0, result: X}= belongs to
+=Plus= for every integer =X=: the identity law stated as membership.
+Note what it is not written as: =[Equal left: [Plus left: X right: 0]
+right: X]=, with an application nested in term position. That form is
+rejected. A block is a proposition, never a value; treating it as a
+value would require privileging one attribute as "the" result, and a
+relation has no distinguished output. The flat membership form is
+both the honest one and the shorter one.
+
 This should be proved symbolically, by the algebraic properties of
-=Plus= and =Equal=, not by checking every integer.
+=Plus=, not by checking every integer.
 
 If Sol cannot prove such a universal symbolically, it must reject the
 program, keep it as an unproven obligation, or require an explicit
diff --git a/docs/sakura-RNT-integration.org b/docs/sakura-RNT-integration.org
index 145c01e..8207ee5 100644
--- a/docs/sakura-RNT-integration.org
+++ b/docs/sakura-RNT-integration.org
@@ -735,6 +735,49 @@ BEAM, and wire clients in any language.
 - C. OCaml for compiler and VM; Rocq with extraction for the
   verified core.
 
+* Decision 14: No Application in Term Position
+
+** The decision
+
+A block =[Relation ...]= is a proposition, never a term. Nested
+application as a value, as in =[Equal left: [Plus left: X right: 0]
+right: X]=, is rejected from the language. Statements about the
+results of relations are written flat, as membership:
+
+#+BEGIN_SRC sol
+[Plus left: X right: 0 result: X]
+#+END_SRC
+
+** The argument
+
+- P1 (delimiter law). Each delimiter has exactly one role. An
+  application that is a proposition in one position and a value in
+  another reintroduces the position-dependent meaning the delimiter
+  law exists to forbid.
+- P2 (relations are not functions). Elaborating an application into
+  a term requires knowing which attribute is "the" result, but a
+  relation is a set of labeled tuples with no distinguished output;
+  label symmetry and mode freedom are core doctrine. The sugar would
+  smuggle function orientation into the semantics, and it is only
+  coherent at modes where the relation happens to be single valued:
+  a partial, mode-dependent elaboration hidden behind innocent
+  syntax.
+- P3 (the motivation dissolves). The nested form is a functional
+  accent, not expressive power: =Equal(Plus(X, 0), X)= is exactly
+  =Plus(X, 0, X)=, which is shorter and states the law as
+  membership, which is what Sol says everything is.
+- C. Applications are propositions, everywhere.
+
+** The one honest future door
+
+If ergonomic pressure ever genuinely demands nested applications,
+they are admissible only as sugar over relations whose catalog
+schema *declares* a principal result attribute and a single
+valuedness capability at the relevant mode, with a published
+elaboration (fresh variable plus flat conjunct). The privilege must
+be explicit and queryable, never assumed from position. Until a real
+program hurts without it, it is not built.
+
 * Consequences for the Pending Documents
 
 - =docs/core-design-and-pipeline.org= must treat transition relations