From 643efc86501b43fe2d68d46b1ccdc2e4e9b9d791 Mon Sep 17 00:00:00 2001
From: Lilleman auf Larv <lilleman@larvit.se>
Date: Mon, 5 Oct 2026 15:59:32 +0200
Subject: [PATCH] Answer prose round 1: the restructure in three named parts,
 Category.Folders and proven.Facts for one meaning per name, plainer
 builtinfunc and datafiles comments, and no false iban rationale

---
 README.md                                |  2 +-
 calc.go                                  |  5 ++-
 data.go                                  |  2 +-
 docs/decisions.md                        |  2 +-
 format.go                                |  4 +--
 internal/builtinfunc/builtinfunc.go      | 22 ++++++------
 internal/builtinfunc/builtinfunc_test.go |  2 +-
 internal/builtinfunc/builtins.go         |  8 ++---
 internal/builtinfunc/checksum.go         |  4 +--
 internal/builtinfunc/transform.go        |  2 +-
 internal/datafiles/datafiles.go          | 20 +++++------
 internal/datafiles/datafiles_test.go     |  4 +--
 internal/proven/proven.go                | 44 ++++++++++++------------
 internal/proven/proven_test.go           |  6 ++--
 struct.go                                |  2 +-
 valueproof.go                            | 34 +++++++++---------
 16 files changed, 79 insertions(+), 84 deletions(-)

diff --git a/README.md b/README.md
index dbcf2da..82cafd7 100644
--- a/README.md
+++ b/README.md
@@ -975,7 +975,7 @@ data.go         the load path: the categories internal/datafiles hands over, com
 cmd/fejkdata/   the fejkdata CLI
 internal/builtinfunc/ the {name()} functions: their checks and draws, checksums, date and time layouts, transforms and calc arithmetic
 internal/datafiles/ the walk of a data tree: its folders, its category files and the rows files beside them
-internal/datatype/ what a record column holds, which DataType aliases
+internal/datatype/ the datatype a record column holds; the root's DataType is an alias of it
 internal/drawstate/ the seeded randomness and the {seq()} counters a generator draws through
 internal/grammar/ how the template language is written: format tokens, paths and selectors, reference sigils, names, calc syntax, and whether an argument is a template or a path
 internal/invariant/ the one phrase every package panics with when an invariant breaks
diff --git a/calc.go b/calc.go
index c013ad5..df8ba61 100644
--- a/calc.go
+++ b/calc.go
@@ -11,9 +11,8 @@ import (
 	"github.com/larvit/fejkdata/internal/invariant"
 )
 
-// checkCalcFields refuses a calc operand a field holds that is never a number, and a division
-// by a constant zero. An operand no field holds is left for a name to answer, and
-// checkCalcNames checks it once names link.
+// checkCalcFields runs checkOperands over the calc operands fields hold. An operand no field
+// holds is left for a name, which checkCalcNames checks once names link.
 func checkCalcFields(args []string, fields map[string]node) error {
 	return checkOperands(args[0], builtinfunc.ParsedCalc(args[0]), func(name string) []node {
 		if n, ok := fields[name]; ok {
diff --git a/data.go b/data.go
index 6baa542..a084356 100644
--- a/data.go
+++ b/data.go
@@ -32,7 +32,7 @@ func compileInto(place func(dir []string) *folder) func(datafiles.Category) erro
 		if err != nil {
 			return err
 		}
-		place(c.Dir).children[c.Name] = n
+		place(c.Folders).children[c.Name] = n
 		return nil
 	}
 }
diff --git a/docs/decisions.md b/docs/decisions.md
index 09ffaba..3aae46a 100644
--- a/docs/decisions.md
+++ b/docs/decisions.md
@@ -827,7 +827,7 @@ Valid while names are read only inside the category binding them.
 
 ## comprehension floor: every dimension and the overall at 7.0 or above; item 5 scores the restructure, which ships unscored: every `{…}` drawing afresh, the moves into `internal/`, and items 101, 102 and 104 to 106
 
-2026-10-04, Lilleman auf Larv. Serves goal 3. The nine-seat panels in `todo.md`'s git history, 2026-09-22 to 2026-09-30, held the score between 5.2 and 6.1, with Locality lowest at every seat. The hardest units were the draw fences, which the change making every `{…}` draw afresh deleted. The change making every `{…}` draw afresh, the moves of the draw state, the grammar, `DataType`, the value proof, the builtins and the reading of data files into `internal/`, and `todo.md` items 101, 102 and 104 to 106 delete or move what the earlier chunks of the below-floor round touched, so a scoring run before item 106 merges would score code about to go; the calc change accepting a name as an operand shipped unscored on 2026-10-05 for that reason. These are the restructure the maintainer approved, which `AGENTS.md`'s comprehension rule lets merge below the floor. No scoring run or panel runs until item 5, which runs the nine-seat panel and larv-review's scoring run. The scoring run writes this entry's first scores. Valid until `todo.md` item 5 runs.
+2026-10-04, Lilleman auf Larv. Serves goal 3. The nine-seat panels in `todo.md`'s git history, 2026-09-22 to 2026-09-30, held the score between 5.2 and 6.1, with Locality lowest at every seat. The hardest units were the draw fences, which the change making every `{…}` draw afresh deleted. The restructure deletes or moves what the earlier chunks of the below-floor round touched. It is three things: the change making every `{…}` draw afresh; the moves of the draw state, the grammar, `DataType`, what a proof knows of a value, the builtins and the reading of data files into `internal/`; and `todo.md` items 101, 102 and 104 to 106. A scoring run before item 106 merges would score code about to go. The calc change accepting a name as an operand shipped unscored on 2026-10-05 for that reason. These are the restructure the maintainer approved, which `AGENTS.md`'s comprehension rule lets merge below the floor. No scoring run or panel runs until item 5, which runs the nine-seat panel and larv-review's scoring run. The scoring run writes this entry's first scores. Valid until `todo.md` item 5 runs.
 
 ## The template engine stays the root package until item 107; what reads no engine type sits in `internal/`, and items 101 and 102 move a table's rows there
 
diff --git a/format.go b/format.go
index 04ae748..b2e4cd6 100644
--- a/format.go
+++ b/format.go
@@ -8,8 +8,8 @@ import (
 	"github.com/larvit/fejkdata/internal/grammar"
 )
 
-// checkFunc validates a call at compile time: a known builtin, its args, and for calc the
-// operands fields holds.
+// checkFunc validates a call at compile time: a known builtin, its args, and, for calc, the
+// operands held in fields.
 func checkFunc(tok grammar.Token, fields map[string]node) error {
 	err := builtinfunc.Check(tok.Fn, tok.Args)
 	if err == nil && tok.Fn == builtinfunc.CalcName {
diff --git a/internal/builtinfunc/builtinfunc.go b/internal/builtinfunc/builtinfunc.go
index 0a5c00f..ea206c0 100644
--- a/internal/builtinfunc/builtinfunc.go
+++ b/internal/builtinfunc/builtinfunc.go
@@ -17,12 +17,9 @@ import (
 // values of the operands it named, which the caller read for it.
 type Call func(s *drawstate.State, emitted string, operands []string) string
 
-// builtin is a format-string function invoked as {name(args)}. It receives the
-// draw state, the output emitted so far in the current expansion (for derivations
-// such as a checksum over preceding digits), and the values of the operands it named
-// (calc and the transforms name them). All must stay pure over (draw state, emitted, operands) so
-// seeded output is reproducible. arity is the exact arg count, or -1 for variadic (then
-// checkArgs does all the validation).
+// builtin is a format-string function invoked as {name(args)}. Its Call stays pure over its
+// inputs, so seeded output is reproducible. arity is the exact arg count, or -1 for variadic,
+// where checkArgs does all the validation.
 type builtin struct {
 	arity int
 	// prep parses validated args once, at compile time, into the closure a render calls.
@@ -36,15 +33,15 @@ type builtin struct {
 	// proveNumber bounds the number a call's text reads as, token its body, and says which
 	// datatypes that text is not; set it where every render reads as a finite number, which
 	// makes the call a calc operand, and leave it nil otherwise.
-	proveNumber func(token string, prints datatype.DataType, args []string) proven.Value
+	proveNumber func(token string, prints datatype.DataType, args []string) proven.Facts
 	// prints is the datatype a call's text is, handed to proveNumber: datatype.String where it
 	// reads as a number no column should type, as digits' leading zeros; unset where
 	// proveNumber is nil.
 	prints datatype.DataType
 }
 
-// CalcName is the builtin whose operands the engine checks and proves, since only the engine
-// holds their nodes.
+// CalcName is the builtin whose operands package fejkdata checks and proves, since only it
+// holds the nodes they read.
 const CalcName = "calc"
 
 // rng is the randomness a builtin sample draws from, which *drawstate.State satisfies.
@@ -92,11 +89,12 @@ func IsTransform(name string) bool {
 }
 
 // ProveNumber proves a call whose every render reads as a finite number, token its body;
-// false for any other call. A calc's proof reads its operands, which the caller proves.
-func ProveNumber(name, token string, args []string) (proven.Value, bool) {
+// false for any other call, calc included: proven.OfCalc proves a calc from its operands,
+// which only the caller holds.
+func ProveNumber(name, token string, args []string) (proven.Facts, bool) {
 	b := builtins[name]
 	if b.proveNumber == nil {
-		return proven.Value{}, false
+		return proven.Facts{}, false
 	}
 	return b.proveNumber(token, b.prints, args), true
 }
diff --git a/internal/builtinfunc/builtinfunc_test.go b/internal/builtinfunc/builtinfunc_test.go
index 7a3d5dc..a9afc0c 100644
--- a/internal/builtinfunc/builtinfunc_test.go
+++ b/internal/builtinfunc/builtinfunc_test.go
@@ -29,7 +29,7 @@ func TestNoRefOperandsMatchesTheOperandGrammar(t *testing.T) {
 			continue
 		}
 		if takesRef := slices.ContainsFunc(b.operands([]string{"/x"}), grammar.IsRef); b.noRefOperands == takesRef {
-			t.Errorf("%s: noRefOperands = %v, but its operands func reads a reference: %v", name, b.noRefOperands, takesRef)
+			t.Errorf("%s: noRefOperands = %v, yet a reference /x read as an operand: %v", name, b.noRefOperands, takesRef)
 		}
 	}
 }
diff --git a/internal/builtinfunc/builtins.go b/internal/builtinfunc/builtins.go
index bc27abe..c2cb05f 100644
--- a/internal/builtinfunc/builtins.go
+++ b/internal/builtinfunc/builtins.go
@@ -35,7 +35,7 @@ var builtins = withTransforms(map[string]builtin{
 	"ulid":   {arity: 0, prep: sample(ulid)},
 	"nanoid": {arity: 1, checkArgs: posIntArg, prep: chars(nanoidAlphabet)},
 	"hex":    {arity: 1, checkArgs: posIntArg, prep: chars(hexDigits)},
-	"digits": {arity: 1, checkArgs: posIntArg, prep: chars("0123456789"), prints: datatype.String, proveNumber: func(token string, prints datatype.DataType, a []string) proven.Value {
+	"digits": {arity: 1, checkArgs: posIntArg, prep: chars("0123456789"), prints: datatype.String, proveNumber: func(token string, prints datatype.DataType, a []string) proven.Facts {
 		return proven.Printing(token, prints, proven.Bounded(0, math.Pow(10, float64(atoi(a[0])))-1, true))
 	}},
 	"upper": {arity: 1, checkArgs: posIntArg, prep: chars("ABCDEFGHIJKLMNOPQRSTUVWXYZ")},
@@ -49,7 +49,7 @@ var builtins = withTransforms(map[string]builtin{
 	"int": {arity: 2, checkArgs: intRangeArgs, prep: func(a []string) Call {
 		lo, span := atoi(a[0]), atoi(a[1])-atoi(a[0])+1
 		return func(s *drawstate.State, _ string, _ []string) string { return strconv.Itoa(lo + s.IntN(span)) }
-	}, prints: datatype.Integer, proveNumber: func(token string, prints datatype.DataType, a []string) proven.Value {
+	}, prints: datatype.Integer, proveNumber: func(token string, prints datatype.DataType, a []string) proven.Facts {
 		return proven.Printing(token, prints, proven.Bounded(float64(atoi(a[0])), float64(atoi(a[1])), true))
 	}},
 	"float": {arity: 3, checkArgs: floatArgs, prep: func(a []string) Call {
@@ -57,7 +57,7 @@ var builtins = withTransforms(map[string]builtin{
 		return func(s *drawstate.State, _ string, _ []string) string {
 			return formatFloat(lo+s.Float64()*(hi-lo), dp)
 		}
-	}, prints: datatype.Number, proveNumber: func(token string, _ datatype.DataType, a []string) proven.Value {
+	}, prints: datatype.Number, proveNumber: func(token string, _ datatype.DataType, a []string) proven.Facts {
 		return proven.PrintedNumber(token, proven.Bounded(atof(a[0]), atof(a[1]), false), atoi(a[2]))
 	}},
 	"iban": {arity: 1, checkArgs: ibanArg, prep: func(a []string) Call {
@@ -78,7 +78,7 @@ var builtins = withTransforms(map[string]builtin{
 		return func(s *drawstate.State, _ string, _ []string) string {
 			return strconv.FormatUint(s.Seq(key), 10)
 		}
-	}, prints: datatype.Integer, proveNumber: func(token string, prints datatype.DataType, _ []string) proven.Value {
+	}, prints: datatype.Integer, proveNumber: func(token string, prints datatype.DataType, _ []string) proven.Facts {
 		return proven.Printing(token, prints, proven.Bounded(1, math.MaxInt64, true))
 	}},
 })
diff --git a/internal/builtinfunc/checksum.go b/internal/builtinfunc/checksum.go
index 16dd5f0..c1fab09 100644
--- a/internal/builtinfunc/checksum.go
+++ b/internal/builtinfunc/checksum.go
@@ -72,9 +72,7 @@ func ibanArg(a []string) error {
 	return nil
 }
 
-// iban generates a structurally valid IBAN for cc: a numeric BBAN of the right
-// length, then mod-97 check digits. Real bank/branch structure isn't modelled —
-// the result passes length and checksum validation, which is what fake data needs.
+// iban generates an IBAN for cc: a numeric BBAN of the right length, then mod-97 check digits.
 func iban(r rng, cc string) string {
 	bban := make([]byte, ibanLen[cc]-4)
 	for i := range bban {
diff --git a/internal/builtinfunc/transform.go b/internal/builtinfunc/transform.go
index 5affb4b..01e65cd 100644
--- a/internal/builtinfunc/transform.go
+++ b/internal/builtinfunc/transform.go
@@ -48,7 +48,7 @@ func unwrapTransform(arg string) (leaf string, chain []func(string) string, err
 	}
 }
 
-// transformArg proves a transform's chain.
+// transformArg checks that each call nested in the arg is a transform taking one arg.
 func transformArg(a []string) error {
 	_, _, err := unwrapTransform(a[0])
 	return err
diff --git a/internal/datafiles/datafiles.go b/internal/datafiles/datafiles.go
index 139a7d0..baff9ee 100644
--- a/internal/datafiles/datafiles.go
+++ b/internal/datafiles/datafiles.go
@@ -32,14 +32,14 @@ func FS(fsys fs.FS, base string) Source { return Source{fsys: fsys, base: base}
 // Category is one category file: the folders above it from the source's base, its name,
 // and its parsed JSON.
 type Category struct {
-	Dir  []string
-	Name string
-	JSON any
-	rows *rowsFiles
+	Folders []string
+	Name    string
+	JSON    any
+	rows    *rowsFiles
 }
 
-// ReadRows reads a rows file beside the category. Reading a file is what names it, so no
-// file is named and left unread.
+// ReadRows reads a rows file beside the category and marks it as named; Walk refuses a rows
+// file no category read.
 func (c Category) ReadRows(name string) (string, error) { return c.rows.read(name) }
 
 func (s Source) labelled(p string) string {
@@ -87,7 +87,7 @@ func (s Source) walkDir(dir []string, compile func(Category) error) (bool, error
 	rows := newRowsFiles(s, full, entries)
 	handed := false
 	for _, e := range entries {
-		if strings.HasPrefix(e.Name(), ".") { // hidden: a checkout or an editor's file, never data
+		if strings.HasPrefix(e.Name(), ".") {
 			continue
 		}
 		var holds bool
@@ -109,7 +109,7 @@ func (s Source) walkDir(dir []string, compile func(Category) error) (bool, error
 	return handed, nil
 }
 
-// walkFolder walks a subfolder, and refuses its name once it holds a category.
+// walkFolder walks a subfolder, and refuses its name if it holds a category.
 func (s Source) walkFolder(dir []string, compile func(Category) error) (bool, error) {
 	holds, err := s.walkDir(dir, compile)
 	if err != nil || !holds {
@@ -121,7 +121,7 @@ func (s Source) walkFolder(dir []string, compile func(Category) error) (bool, er
 	return true, nil
 }
 
-// Load hands compile the one category file name in the folder dir.
+// Load hands compile the category file name.json in the folder dir.
 func (s Source) Load(dir []string, name string, compile func(Category) error) error {
 	full := s.dirPath(dir)
 	entries, err := fs.ReadDir(s.fsys, full)
@@ -151,7 +151,7 @@ func (s Source) compileFile(dir []string, file string, rows *rowsFiles, compile
 	if err := json.Unmarshal(b, &raw); err != nil {
 		return false, fmt.Errorf("%s: %w", s.labelled(full), err)
 	}
-	if err := compile(Category{Dir: dir, Name: name, JSON: raw, rows: rows}); err != nil {
+	if err := compile(Category{Folders: dir, Name: name, JSON: raw, rows: rows}); err != nil {
 		return false, fmt.Errorf("%s: %w", s.labelled(full), err)
 	}
 	return true, nil
diff --git a/internal/datafiles/datafiles_test.go b/internal/datafiles/datafiles_test.go
index 41d62b1..5f20f14 100644
--- a/internal/datafiles/datafiles_test.go
+++ b/internal/datafiles/datafiles_test.go
@@ -20,7 +20,7 @@ func walk(t *testing.T, src Source) ([]handed, error) {
 	t.Helper()
 	var got []handed
 	err := src.Walk(func(c Category) error {
-		got = append(got, handed{c.Dir, c.Name, c.JSON})
+		got = append(got, handed{c.Folders, c.Name, c.JSON})
 		return nil
 	})
 	return got, err
@@ -134,7 +134,7 @@ func TestLoadHandsOneCategoryAndItsRows(t *testing.T) {
 	var got handed
 	var rows string
 	err := src.Load([]string{"sub"}, "t", func(c Category) error {
-		got = handed{c.Dir, c.Name, c.JSON}
+		got = handed{c.Folders, c.Name, c.JSON}
 		var err error
 		rows, err = c.ReadRows("t.tsv")
 		return err
diff --git a/internal/proven/proven.go b/internal/proven/proven.go
index 2f9e499..00dfa15 100644
--- a/internal/proven/proven.go
+++ b/internal/proven/proven.go
@@ -14,9 +14,9 @@ import (
 	"github.com/larvit/fejkdata/internal/invariant"
 )
 
-// Value is what a proof knows of every render of a node: bounds on the number each
+// Facts is what a proof knows of every render of a node: bounds on the number each
 // reads as, and per datatype why some render's text is not one ("" when none).
-type Value struct {
+type Facts struct {
 	Lo, Hi     float64
 	NonZero    float64 // every value is at least this far from zero; 0 when one can be zero
 	Integral   bool
@@ -33,7 +33,7 @@ const ShortestDecimals = -1
 const limit = 1e300
 
 // Or is what a proof knows of a render that is either v or w.
-func (v Value) Or(w Value) Value {
+func (v Facts) Or(w Facts) Facts {
 	v.Lo, v.Hi, v.NonZero = min(v.Lo, w.Lo), max(v.Hi, w.Hi), min(v.NonZero, w.NonZero)
 	v.Integral, v.Nullable = v.Integral && w.Integral, v.Nullable || w.Nullable
 	if v.NotOperand == "" {
@@ -48,7 +48,7 @@ func (v Value) Or(w Value) Value {
 }
 
 // OfCalc bounds a calc expression from its operands, or says why it cannot.
-func OfCalc(expr grammar.CalcNode, operand func(name string) Value) (Value, string) {
+func OfCalc(expr grammar.CalcNode, operand func(name string) Facts) (Facts, string) {
 	v, doubt := bound(expr, operand)
 	if doubt == "" && !(magnitude(v) <= limit) {
 		doubt = grammar.CalcText(expr) + " is not proven within 1e300"
@@ -56,7 +56,7 @@ func OfCalc(expr grammar.CalcNode, operand func(name string) Value) (Value, stri
 	return v, doubt
 }
 
-func bound(n grammar.CalcNode, operand func(name string) Value) (Value, string) {
+func bound(n grammar.CalcNode, operand func(name string) Facts) (Facts, string) {
 	switch n := n.(type) {
 	case grammar.CalcNum:
 		v := float64(n)
@@ -64,9 +64,9 @@ func bound(n grammar.CalcNode, operand func(name string) Value) (Value, string)
 	case grammar.CalcVar:
 		v := operand(n.Name)
 		if v.NotOperand != "" {
-			return Value{}, fmt.Sprintf("operand %q: %s", n.Name, v.NotOperand)
+			return Facts{}, fmt.Sprintf("operand %q: %s", n.Name, v.NotOperand)
 		}
-		return Value{Lo: v.Lo, Hi: v.Hi, NonZero: v.NonZero, Integral: v.Integral}, ""
+		return Facts{Lo: v.Lo, Hi: v.Hi, NonZero: v.NonZero, Integral: v.Integral}, ""
 	case grammar.CalcNeg:
 		v, doubt := bound(n.X, operand)
 		v.Lo, v.Hi = -v.Hi, -v.Lo
@@ -86,8 +86,8 @@ func bound(n grammar.CalcNode, operand func(name string) Value) (Value, string)
 }
 
 // combine bounds one operation from the bounds of its sides.
-func combine(n grammar.CalcBin, l, r Value) (Value, string) {
-	var v Value
+func combine(n grammar.CalcBin, l, r Facts) (Facts, string) {
+	var v Facts
 	integral := l.Integral && r.Integral
 	switch n.Operator {
 	case '+':
@@ -102,7 +102,7 @@ func combine(n grammar.CalcBin, l, r Value) (Value, string) {
 			return v, fmt.Sprintf("divides by %s, which is not proven nonzero", grammar.CalcText(n.R))
 		}
 		m := magnitude(l) / r.NonZero
-		v = Value{Lo: -m, Hi: m, NonZero: l.NonZero / magnitude(r)}
+		v = Facts{Lo: -m, Hi: m, NonZero: l.NonZero / magnitude(r)}
 	}
 	if !(magnitude(v) <= limit) {
 		return v, grammar.CalcText(n) + " is not proven within 1e300"
@@ -111,8 +111,8 @@ func combine(n grammar.CalcBin, l, r Value) (Value, string) {
 }
 
 // Bounded is a number in [lo, hi], its distance from zero read off the bounds.
-func Bounded(lo, hi float64, integral bool) Value {
-	v := Value{Lo: lo, Hi: hi, Integral: integral}
+func Bounded(lo, hi float64, integral bool) Facts {
+	v := Facts{Lo: lo, Hi: hi, Integral: integral}
 	switch {
 	case lo > 0:
 		v.NonZero = lo
@@ -122,10 +122,10 @@ func Bounded(lo, hi float64, integral bool) Value {
 	return v
 }
 
-func magnitude(v Value) float64 { return math.Max(math.Abs(v.Lo), math.Abs(v.Hi)) }
+func magnitude(v Facts) float64 { return math.Max(math.Abs(v.Lo), math.Abs(v.Hi)) }
 
 // PrintedNumber is what a token printing v to dp decimals holds.
-func PrintedNumber(token string, v Value, dp int) Value {
+func PrintedNumber(token string, v Facts, dp int) Facts {
 	if dp == ShortestDecimals {
 		if v.Integral { // a whole value prints with no point
 			return printedInteger(token, v)
@@ -133,14 +133,14 @@ func PrintedNumber(token string, v Value, dp int) Value {
 		return Printing(token, datatype.Number, v)
 	}
 	half, _ := strconv.ParseFloat("5e-"+strconv.Itoa(dp+1), 64)
-	v = Value{Lo: v.Lo - half, Hi: v.Hi + half, NonZero: math.Max(0, v.NonZero-half), Integral: v.Integral || dp == 0}
+	v = Facts{Lo: v.Lo - half, Hi: v.Hi + half, NonZero: math.Max(0, v.NonZero-half), Integral: v.Integral || dp == 0}
 	if dp == 0 {
 		return printedInteger(token, v)
 	}
 	return Printing(token, datatype.Number, v)
 }
 
-func printedInteger(token string, v Value) Value {
+func printedInteger(token string, v Facts) Facts {
 	v = Printing(token, datatype.Integer, v)
 	if !(magnitude(v) < math.MaxInt64) {
 		v.Not[datatype.Integer] = fmt.Sprintf("{%s} is not proven within int64", token)
@@ -150,7 +150,7 @@ func printedInteger(token string, v Value) Value {
 
 // Printing is v for a token whose every render is text of datatype prints, with a reason
 // against each datatype that text is not.
-func Printing(token string, prints datatype.DataType, v Value) Value {
+func Printing(token string, prints datatype.DataType, v Facts) Facts {
 	for d := datatype.Integer; d < datatype.Count; d++ {
 		if prints != d && !(prints == datatype.Integer && d == datatype.Number) {
 			v.Not[d] = fmt.Sprintf("{%s} prints %s, not %s", token, datatype.Noun(prints), datatype.Noun(d))
@@ -160,8 +160,8 @@ func Printing(token string, prints datatype.DataType, v Value) Value {
 }
 
 // Unproven is a render no datatype and no calc can take, for why.
-func Unproven(why string) Value {
-	v := Value{NotOperand: why}
+func Unproven(why string) Facts {
+	v := Facts{NotOperand: why}
 	for d := datatype.Integer; d < datatype.Count; d++ {
 		v.Not[d] = why
 	}
@@ -174,8 +174,8 @@ var (
 )
 
 // Literal proves fixed text: the number calc reads it as, and each datatype it is.
-func Literal(text string) Value {
-	var v Value
+func Literal(text string) Facts {
+	var v Facts
 	if f, err := strconv.ParseFloat(strings.TrimSpace(text), 64); err != nil || math.IsNaN(f) || math.IsInf(f, 0) {
 		v.NotOperand = fmt.Sprintf("%q is not a number", text)
 	} else {
@@ -196,7 +196,7 @@ func Literal(text string) Value {
 }
 
 // signedZero refuses a zero written with a sign as a typed value, naming it unsigned.
-func signedZero(text string, v Value) Value {
+func signedZero(text string, v Facts) Facts {
 	mantissa, _, _ := strings.Cut(strings.ToLower(text), "e")
 	if !strings.HasPrefix(text, "-") || v.NotOperand != "" || strings.Trim(mantissa, "-0.") != "" {
 		return v
diff --git a/internal/proven/proven_test.go b/internal/proven/proven_test.go
index 87b172a..b1fdb0e 100644
--- a/internal/proven/proven_test.go
+++ b/internal/proven/proven_test.go
@@ -42,8 +42,8 @@ func TestOrKeepsTheBoundsOfBothAndTheFirstReason(t *testing.T) {
 }
 
 func TestOfCalcBoundsAnExpressionFromItsOperands(t *testing.T) {
-	operand := func(name string) Value {
-		return map[string]Value{"a": Bounded(1, 9, true), "b": Bounded(0, 9, true), "big": Bounded(0, 1e299, true), "word": Unproven("it is text")}[name]
+	operand := func(name string) Facts {
+		return map[string]Facts{"a": Bounded(1, 9, true), "b": Bounded(0, 9, true), "big": Bounded(0, 1e299, true), "word": Unproven("it is text")}[name]
 	}
 	for expr, want := range map[string]string{
 		"a * 2 + 1": "",
@@ -69,7 +69,7 @@ func TestOfCalcBoundsAnExpressionFromItsOperands(t *testing.T) {
 		}
 	}
 	lone, _ := grammar.ParseCalc("x")
-	if _, doubt := OfCalc(lone.Expr, func(string) Value { return Bounded(0, 1e301, true) }); doubt != "x is not proven within 1e300" {
+	if _, doubt := OfCalc(lone.Expr, func(string) Facts { return Bounded(0, 1e301, true) }); doubt != "x is not proven within 1e300" {
 		t.Errorf("OfCalc(x) doubts %q, want a lone operand held to the limit", doubt)
 	}
 }
diff --git a/struct.go b/struct.go
index d1f1c49..7b1d199 100644
--- a/struct.go
+++ b/struct.go
@@ -310,7 +310,7 @@ var columnKinds = map[reflect.Kind]columnKind{
 
 // holds reports whether a field of this kind holds every value v proves. An integer prints
 // whole, so its bounds round inward first.
-func (k columnKind) holds(v proven.Value) bool {
+func (k columnKind) holds(v proven.Facts) bool {
 	switch k.datatype {
 	case DataTypeString, DataTypeBoolean:
 		return true
diff --git a/valueproof.go b/valueproof.go
index 163b9a0..968a7f4 100644
--- a/valueproof.go
+++ b/valueproof.go
@@ -12,8 +12,8 @@ import (
 
 // valueProof proves what typed columns and their calc operands hold, each node once per scope.
 type valueProof struct {
-	memo       map[node]proven.Value
-	columnMemo map[node]proven.Value
+	memo       map[node]proven.Facts
+	columnMemo map[node]proven.Facts
 }
 
 // checkDatatype rejects a typed column item some render of which is not text of its datatype,
@@ -65,7 +65,7 @@ func (p *valueProof) checkField(label string, ft reflect.Type, column node) erro
 }
 
 // proveColumnItem proves a column item: what it renders, or, when it is a column it reads, that column.
-func (p *valueProof) proveColumnItem(t *template) proven.Value {
+func (p *valueProof) proveColumnItem(t *template) proven.Facts {
 	if t.link.readsColumn == nil {
 		return p.prove(t)
 	}
@@ -74,15 +74,15 @@ func (p *valueProof) proveColumnItem(t *template) proven.Value {
 
 // proveColumn proves a column over what its items draw, a null item marking it null rather than
 // rendering "".
-func (p *valueProof) proveColumn(n node) proven.Value {
+func (p *valueProof) proveColumn(n node) proven.Facts {
 	if v, done := p.columnMemo[n]; done {
 		return v
 	}
 	if p.columnMemo == nil {
-		p.columnMemo = map[node]proven.Value{}
+		p.columnMemo = map[node]proven.Facts{}
 	}
 	items, nullable := columnItems(n)
-	var v proven.Value
+	var v proven.Facts
 	for i, it := range items {
 		if w := p.proveColumnItem(it); i == 0 {
 			v = w
@@ -95,14 +95,14 @@ func (p *valueProof) proveColumn(n node) proven.Value {
 	return v
 }
 
-func (p *valueProof) prove(n node) proven.Value {
+func (p *valueProof) prove(n node) proven.Facts {
 	if v, done := p.memo[n]; done {
 		return v
 	}
 	if p.memo == nil {
-		p.memo = map[node]proven.Value{}
+		p.memo = map[node]proven.Facts{}
 	}
-	var v proven.Value
+	var v proven.Facts
 	switch n := n.(type) {
 	case *choice:
 		v = p.proveUnion(n.items)
@@ -124,10 +124,10 @@ func (p *valueProof) prove(n node) proven.Value {
 }
 
 // proveCells proves a table column over every cell it may render.
-func (p *valueProof) proveCells(c *tableColumn) proven.Value {
-	var v proven.Value
+func (p *valueProof) proveCells(c *tableColumn) proven.Facts {
+	var v proven.Facts
 	for r := 0; r < c.t.rowCount(); r++ {
-		var w proven.Value
+		var w proven.Facts
 		if cell := c.t.cellTemplate(r, c.i); cell != nil {
 			w = p.prove(cell)
 		} else {
@@ -142,7 +142,7 @@ func (p *valueProof) proveCells(c *tableColumn) proven.Value {
 	return v
 }
 
-func (p *valueProof) proveUnion(nodes []node) proven.Value {
+func (p *valueProof) proveUnion(nodes []node) proven.Facts {
 	v := p.prove(nodes[0])
 	for _, n := range nodes[1:] {
 		v = v.Or(p.prove(n))
@@ -152,7 +152,7 @@ func (p *valueProof) proveUnion(nodes []node) proven.Value {
 
 // proveTemplate proves a template that renders one value: fixed text, or a format that is
 // one token alone.
-func (p *valueProof) proveTemplate(t *template) proven.Value {
+func (p *valueProof) proveTemplate(t *template) proven.Facts {
 	lit, fixed := t.fixedText()
 	switch {
 	case t.repeat != 1:
@@ -181,13 +181,13 @@ func (p *valueProof) proveTemplate(t *template) proven.Value {
 	if v, numeric := builtinfunc.ProveNumber(name, body, args); numeric {
 		return v
 	}
-	return proven.Printing(body, DataTypeString, proven.Value{NotOperand: fmt.Sprintf("{%s} prints text, not a number", body)})
+	return proven.Printing(body, DataTypeString, proven.Facts{NotOperand: fmt.Sprintf("{%s} prints text, not a number", body)})
 }
 
-func (p *valueProof) proveCalc(o op) proven.Value {
+func (p *valueProof) proveCalc(o op) proven.Facts {
 	body, args := o.Body, o.Args
 	nodes := operandNodes(o)
-	v, doubt := proven.OfCalc(builtinfunc.ParsedCalc(args[0]).Expr, func(name string) proven.Value { return p.proveUnion(nodes(name)) })
+	v, doubt := proven.OfCalc(builtinfunc.ParsedCalc(args[0]).Expr, func(name string) proven.Facts { return p.proveUnion(nodes(name)) })
 	if doubt != "" {
 		return proven.Unproven(fmt.Sprintf("{%s}: %s", body, doubt))
 	}