Abstract
We specify Number Garden, an educational game connecting counting, arithmetic, word problems, and systems of equations. A typed semantics supports proofs of correct counting, safe rewrites, story compilation, bounded solving, and compatible gluing. A solution presheaf and its groupoid refinement retain clue structure and token symmetries. The complete manuscript and executable model include tasks with two and three unknowns. Learning effectiveness remains untested.
1. Educational scope and game
The intended audience spans approximately ages 4-10. Ages guide presentation, not fixed achievement thresholds. The youngest strand asks children to touch each object once, match collections, and connect numerals with quantities. Later strands introduce joining and separating, equal groups, relational equality, missing quantities, and optional linked-clue puzzles. Simultaneous equations are introduced through differently labeled bags, after prerequisite skills, rather than required of every child in the age range.
A scene contains objects, a question, actions, and feedback. Children predict, model, check all clues, and explain. Audio and images express the same problem. Bag identity uses shape and label, with optional color; repeated labels denote the same quantity. Assistance and concrete counters remain available. Speed is not a correctness criterion.
The progression draws on early-mathematics guidance [1], board-game [2] and early-algebra [3] studies, and elementary standards [4-6]. None evaluates Number Garden. Simultaneous equations are proposed enrichment, not a cited elementary requirement.
2. Typed quantities and problems
Definition 1. A context is a finite list $\Gamma=(x_1:u_1,\ldots,x_m:u_m)$ of distinct variables with units. Let $\mathbb N=\{0,1,2,\ldots\}$. Each unknown has an explicit domain $D_i=\{0,\ldots,B_i\}$, and $V_\Gamma=\prod_iD_i$. Terms have grammar
$$t:u::=n_u\mid x:u\mid(t:u)+(t:u)\mid k(t:u),\qquad n,k\in\mathbb N.$$
An equation compares terms of the same unit. Scalar multiplication denotes a known number of equal groups; multiplication of two unknowns is outside this linear core. Evaluation is recursive:
$$\llbracket n_u\rrbracket_\rho=n,\quad \llbracket x\rrbracket_\rho=\rho(x),\quad \llbracket t+s\rrbracket_\rho=\llbracket t\rrbracket_\rho+\llbracket s\rrbracket_\rho,\quad \llbracket kt\rrbracket_\rho=k\llbracket t\rrbracket_\rho.$$
Bounds constrain unknowns, not intermediate arithmetic: evaluation uses unbounded natural numbers. Adding bags to seeds is a type error. Three bags each containing $x$ seeds contribute $3x$ seeds, not $3+x$.
Definition 2. A problem $P=(\Gamma,D,E,q)$ consists of its context, domains, a finite conjunction $E$ of typed equations, and a question mode. Its solutions are
$$\operatorname{Sol}(P)=\{\rho\in V_\Gamma:\llbracket t\rrbracket_\rho=\llbracket s\rrbracket_\rho\text{ for all }(t=s)\in E\}.$$
Find asks for any solution. Determine asks for a target term's value in every solution, with at least one solution required. Classify distinguishes zero, one, or several solutions. Ordinary mystery-bag tasks require a unique complete assignment; investigations can intentionally have several answers or inconsistent clues.
Subtraction is relational: from $a$ objects, removing $b$ leaves $c$ means $c+b=a$. If $b>a$, there is no natural-number solution, not a result silently clamped to zero. Exact division means $kx=n$ with $k>0$. Remainders require an explicit quantity $r$ with $kx+r=n$ and domain $0\leq r<k$. Negative and fractional quantities are outside the core.
Lemma 1 (substitution). For a same-unit substitution $\sigma$ into terms over a context $\Delta$, define $\sigma^*\eta(x)=\llbracket\sigma(x)\rrbracket_\eta$. Then
$$\llbracket t[\sigma]\rrbracket_\eta=\llbracket t\rrbracket_{\sigma^*\eta}.$$
Proof. The constant and variable cases are immediate. Apply the induction hypothesis to each summand, or to the scaled subterm. These exhaust the constructors. For bounded problems, substituted values must additionally lie in the declared domains. $\square$
Terms compose by substitution; evaluation is a product-preserving interpretation in sets [7]. Cancellation belongs to the natural-number model, not every commutative monoid.
3. Counting and equivalent moves
Definition 3. A counting certificate for a finite collection $A$ and answer $n$ is a bijection $[n]\to A$, with $[n]=\{1,\ldots,n\}$. Token identifiers are stable through animation; a token already selected cannot increment the count again. Completion requires every token.
Theorem 2. A certificate proves $n=|A|$. A bijection $A\to A'$ preserves the certified number, and
$$|A\sqcup B|=|A|+|B|,\qquad |[k]\times A|=k|A|.$$
Proof. A bijection to $[n]$ defines finite cardinality, and composing bijections preserves it. Concatenate enumerations for a tagged disjoint union; enumerate the $k$ tagged copies for the product. $\square$
Overlapping selections are not disjoint collections. A join must establish distinct physical identifiers or explicitly create distinct copies. The groupoid $\mathsf{Fin}^{\simeq}$ of finite sets and bijections retains permutation witnesses; its isomorphism classes form $\mathbb N$ with the indicated operations. This groupoid is not asserted to be a topos.
Definition 4. A state consists of an immutable original problem, displayed equations, a tentative partial assignment, a representation, and a history. Ordinary equation play retains the context and domains. Four action classes have different contracts:
Rewritepreserves the whole solution set.Revealexposes an authored clue and may reduce the candidate set.Trychanges a proposal without turning it into a premise.World changeintroduces a relation between time-indexed quantities, such as $a_{t+1}+2=a_t$, instead of claiming the earlier quantity is unchanged.
Theorem 3 (rewrite soundness). Over fixed natural-number domains, the following preserve solutions: associative and commutative regrouping; distribution of a known scalar; evaluation of closed arithmetic; adding or cancelling the same term on both sides; scaling or cancelling a common positive scalar; substituting equals while retaining the justifying equality; and appending a derived equation while retaining its premises.
Proof. Fix an admissible valuation. Arithmetic identities give the first rules. Addition by a fixed natural number and multiplication by a positive integer are injective, giving both directions of the cancellation rules. A retained equality gives equal evaluations for replaced subterms, and induction on the containing term proves substitution of equals. A consequence removes no original solution, and retaining premises introduces none. Conjoin unchanged equations. $\square$
Multiplying by zero is not reversible. Replacing two equations by their sum can lose constraints. Doing the same operation on both sides is therefore not sufficient unless the operation is injective on the relevant values or the remaining constraints establish equivalence.
Lemma 4 (bounded elimination). If $E=\{x=t\}\cup F$ and $x$ is absent from $t$, projection away from $x$ bijects $\operatorname{Sol}(E)$ with valuations $\eta$ satisfying $F[t/x]$ and $\llbracket t\rrbracket_\eta\in D_x$.
Proof. Projection satisfies these conditions by Lemma 1. Conversely, extend $\eta$ by the unique value $x=\llbracket t\rrbracket_\eta$; the bound and Lemma 1 show that the extension solves $E$. The constructions are inverse. $\square$
The bound matters: for $x,y\in\{0,1\}$ and $x=y+1$, projection permits only $y=0$. Discarding the bound would falsely admit $y=1$.
Theorem 5 (no false success). Suppose accepted rewrites satisfy Theorem 3 or an independently checked finite-domain equivalence, and success is checked against the immutable original problem. Find success returns an actual solution. Determine success returns the common target value of a nonempty solution set.
Proof. Induction preserves solutions along accepted rewrites. The final checker requires a complete in-domain assignment satisfying every original equation for Find. For Determine, it requires a nonempty solution set whose target-value image is the singleton answer. These are precisely the stated semantics. All authored clues participate in the final check, and guesses never become premises. $\square$
This is mathematical safety, not a proof of understanding. Independently reasoned, assisted, and guessed answers provide different instructional evidence.
4. Controlled word problems
A story declares referents, units, a question, and a conjunction of clauses. The compiler uses the following relations:
$$\begin{array}{ll} \operatorname{join}(a,b,c)&a+b=c,\\ \operatorname{more}(a,b,n)&a=b+n,\\ \operatorname{groups}(k,a,b)&ka=b,\\ \operatorname{remove}(a,b,c)&c+b=a,\\ \operatorname{same}(a,b)&a=b. \end{array}$$
Here $n,k$ are known natural numbers. Clauses are unit checked. Joining assumes disjoint collections; removing distinguishes before and after. A mixed-species total first declares a common counting unit, such as animals. A sentence is mapped through its referents and relational structure, not by a keyword such as “more.”
Theorem 6 (compiler adequacy). Interpret each controlled clause by the stated relation and conjunction by simultaneous satisfaction. Then
$$\rho\models W\quad\Longleftrightarrow\quad\rho\in\operatorname{Sol}(C(W)).$$
Proof. Each atomic case is its displayed relation. The compiler concatenates equation lists for conjunction, and both interpretations require every conjunct. Structural induction proves the result. $\square$
The theorem is about the defined controlled language, not unrestricted English. Authors must check that wording, audio, images, and identities express the intended clauses. Generated wording is a proposal subject to that review, not an automatic correctness certificate.
5. Worked linked-clue episodes
Two bags. A triangle bag and square bag contain eight beads altogether. The triangle bag has two more beads. With their counts $x,y\in\{0,\ldots,10\}$,
$$x+y=8,\qquad x=y+2.$$
Retain the second equation and substitute into the first: $(y+2)+y=8$, hence $2y+2=6+2$, $2y=6$, and $y=3$. The retained equation gives $x=5$. Check both $5+3=8$ and $5=3+2$. A child can instead enumerate pairs using an eight-bead split tray.
Three bags. Let
$$x+y=7,\qquad y+z=5,\qquad x+z=6.$$
Append the sum of the first and third equations, retaining their premises: $2x+y+z=13$. Substitute the middle clue to obtain $2x+5=8+5$, hence $x=4$, $y=3$, and $z=2$. Check all original clues. Arbitrarily many unknowns are allowed by the finite-context definition; this three-variable case is an optional extension.
Missing information. The equations $x+y=8$ and $2x+2y=16$ have nine solutions on $\{0,\ldots,10\}^2$. Two equations do not necessarily determine two unknowns. Their total is determined even though each individual value is not. In contrast, $x+y=8$ and $x+y=9$ have no joint solution. Such investigations are explicitly distinguished from ordinary unique-answer tasks.
6. Decision procedure and generation
Theorem 7. Exhaustively enumerate $V_\Gamma$, retaining exactly the valuations that satisfy every equation. This terminates and computes $\operatorname{Sol}(P)$ exactly; it decides existence, uniqueness, partial-assignment consistency, and target determinacy.
Proof. There are $N=\prod_i(B_i+1)$ tuples, visited once each. Recursive term evaluation terminates. Retention is exactly the definition of satisfaction. Counting solutions and computing their target-value image yields the decisions. $\square$
With total equation-tree size $L$, enumeration uses $O(NL)$ arithmetic operations, not a coefficient-independent bit bound. A complete proposed answer takes $O(L)$ operations to check. Three unknowns bounded by ten give 1331 candidates.
Generate a witness first, construct true clues, then check uniqueness. For $x+y=s$, $x=y+d$, $d\geq0$, a natural solution requires $s\geq d$, even $s-d$, and in-domain values $y=(s-d)/2$, $x=(s+d)/2$; these conditions suffice. Full column rank gives at most one rational solution, not existence of a natural one. Rank deficiency can coexist with uniqueness: $x+y=0$ forces both values to zero. Instructional filters separately bound totals, vocabulary, and strategy length.
7. Presheaf and higher-categorical semantics
Fix the context, domains, and a finite set $E_*$ of authored clues. Let $\mathcal C=\mathcal P(E_*)$ have arrows $K\to L$ for $K\subseteq L$. Define
$$S:\mathcal C^{\mathrm{op}}\to\mathsf{Set},\qquad S(K)=\{\rho\in V_\Gamma:\rho\models K\}.$$
Restriction $S(L)\to S(K)$ is inclusion. Revealing a clue moves upward in information but narrows the candidate set; it is not a function choosing a new solution for every old candidate.
Proposition 8. This is a presheaf, a subobject of the constant presheaf $\Delta V_\Gamma$, and its global sections biject $S(E_*)$.
Proof. Inclusions compose and preserve identities. Component injections commute with restriction. A global section is a compatible tuple at every stage; compatibility with $K\subseteq E_*$ forces all stage values to equal its value at $E_*$. Conversely, each complete solution supplies this family. $\square$
The ordinary topos is $\operatorname{Fun}(\mathcal C^{\mathrm{op}},\mathsf{Set})$. The solution presheaf is an object, not a topos. A stage element is not a geometric point of that topos. No nontrivial Grothendieck topology is imposed here.
Let $\mathcal S$ be the $\infty$-category of spaces. The standard presheaf construction [8] gives the $\infty$-topos
$$\mathcal X=\operatorname{Fun}(N(\mathcal C)^{\mathrm{op}},\mathcal S).$$
Retain abstract counting-set symmetries by defining
$$\widetilde S(K)=\coprod_{\rho\in S(K)}\prod_{i=1}^mB\Sigma_{\rho(x_i)},$$
where $B\Sigma_n$ is the classifying space of the permutation group of $n$ objects. Runtime identifiers remain stable; these are abstract relabeling witnesses.
Proposition 9. Inclusion of solution-indexed summands defines $\widetilde S\in\mathcal X$. It is 1-truncated, with $\tau_{\leq0}\widetilde S\simeq S$ objectwise and naturally.
Proof. Restrictions preserve each solution's group factors and compose strictly. Each $B\Sigma_n$ is a connected 1-type. Finite products are connected 1-types, and their disjoint union has one component per solution. Connected components therefore recover $S(K)$, compatibly with restrictions. $\square$
The refinement adds symmetries without changing arithmetic answers. It is not claimed that 0-truncation preserves all limits. Directed operational histories are retained separately: the same answer can arise through different strategies, and groupoid completion is not used to justify undoing irreversible world changes.
8. Compatible partial solutions
On the discrete variable space $I$, assignments $A(U)=\prod_{i\in U}D_i$ form a sheaf under coordinate restriction. This is distinct from the clue-indexed presheaf above.
Theorem 10 (constraint-aware gluing). Let subsets $U_j$ cover $I$. Assign every equation to at least one $U_j$ containing its entire variable support. If each local assignment satisfies its assigned equations and all local assignments agree on overlaps, they glue to a unique global solution. Every global solution restricts to such a family.
Proof. Define each coordinate using any covering subset containing it; overlap agreement makes the choice independent. This gives the unique glued tuple. Every equation is evaluated within a subset to which it was assigned and holds there. The converse follows by restriction. $\square$
Local solvability is insufficient: $x=1$ and $x=2$ disagree on their shared variable. Coverage of variables alone is also insufficient: $x=0$ on $\{x\}$ and $y=1$ on $\{y\}$ agree on the empty overlap, but violate a cross-variable constraint $x=y$. The presheaf of restrictions of global solutions need not be a sheaf. Cooperative play must check both shared quantities and cross-group constraints.
9. Adaptation, verification, and limits
Model prerequisites by a finite partial order of skills. Maintain a downward-closed set $M$ of recorded skills; add a skill only when all its strict predecessors are in $M$. This preserves downward closure: lower elements of an old member were already present, and lower elements of the new member are present by the admission condition. This verifies a curriculum invariant, not the validity of a mastery measurement. Evidence should distinguish assisted and independent performance, familiar and novel presentations, and immediate and delayed success.
The attached reference kernel implements typed terms, story compilation, enumeration, answer checking, and finite rewrite equivalence. Its script passed 15,619 checks, including 1,296 small matrix systems, 66 generated puzzles, and 874 counting orders, plus negative cases. The supplied report and script specify the finite ranges. These are executable checks, not proof-assistant verification of the general theorems.
A production game must verify that displayed scenes represent authored relations. No classroom trial or learning-effect measurement is reported. Proposed evaluation separates formal correctness from transfer and retention, using supervised formative work before a specified comparison with matched instructional time and assistance.
Authorship uses an anonymous human byline. OpenAI Codex assisted with drafting, source retrieval, mathematical analysis, typesetting, and implementation. The commissioning author retains responsibility for final approval. Automation output is not a referee report. Preparation for this journal does not establish acceptance or peer review.
References
[1] D. Frye et al. *Teaching Math to Young Children*. NCEE 2014-4005, IES, 2013. Official guide and evidence ratings.
[2] G. B. Ramani and R. S. Siegler. Promoting broad and stable improvements in low-income children's numerical knowledge through playing number board games. *Child Development* 79(2), 375-394, 2008. DOI; verified abstract.
[3] M. Blanton, A. Stephens, E. Knuth, A. M. Gardiner, I. Isler, and J.-S. Kim. The development of children's algebraic thinking: The impact of a comprehensive early algebra intervention in third grade. *JRME* 46(1), 39-87, 2015. DOI; institutional record.
[4-6] NGA Center and CCSSO. *Common Core State Standards for Mathematics*, 2010. K.CC, 1.OA, 4.OA.
[7] F. W. Lawvere. *Functorial Semantics of Algebraic Theories* (1963), with a 1968 sequel. *Reprints in TAC* 5, 1-121, 2004. Publisher record; text.
[8] J. Lurie. *Higher Topos Theory*. Annals of Mathematics Studies 170, 2009, Chapters 5-6. Author-hosted text; arXiv.