| title | Model | ||||
|---|---|---|---|---|---|
| description | What a Beloch program talks about. States, values, and the operations on both. | ||||
| tableOfContents |
|
This document defines what a Beloch program talks about: the set of states,
the values a program can name, and the operations on both. BELOCH.md
says how the language is written; this document says what it means. How the
kernel realizes it is the subject of KERNEL.md, which refers to the
statements here by their ids; this document does not refer back.
The document grows in steps. Each definition is stated with its intuition first, then its formal content. Statements are numbered within their section: a Definition introduces a term, a Lemma is a consequence with a proof or a pointer to one, a Corollary follows from a lemma without further argument, a Remark is unproven commentary, a Condition is a named requirement that a later definition collects, an Open point is a decision still to be made and is part of the contract until closed. Each statement carries the terms it defines, the statements it uses and the statements that use it. Every word used in a technical sense is listed under Terms with a link to where it is defined; the first use in the text links there too.
Before reading. The text uses set notation and plane geometry at first-course level, and folding words (crease, flap, layer, mountain, valley) the way folders use them. Everything it needs from flat-folding theory is restated where it is used; the full account is Hull [@hull2020, chapter 6].
Review status. Section 1 read and accepted. Section 2 rewritten on
review (2026-09-17): the state is a triple,
Intuition: a sheet of paper is a flat shape whose points keep their identity no matter how the sheet is folded. Everything Beloch names is a point of the sheet, a line drawn on the sheet, or a set of such things.
::: {.definition #def-sheet name="sheet" defines="term-paper-frame"}
A sheet is a simple polygon
::: {.term #term-paper-frame name="paper frame"}
The plane the sheet
The sheet may be non-convex. Convexity belongs to the faces of a state
([#def-flat-state]): a non-convex sheet is decomposed into convex faces joined
by flat hinges (angle
Holes are excluded because the tortilla conditions of [#def-noncrossing] are stated for regions without holes [@hullzakharevich2023, §2.1] and because the existence of a folding motion is proven for simple polygons only [@demaine2007, sec. 11.6, Theorem 11.6.2].
Sources: paper as an orientable 2-manifold with boundary [@demaine2007, §11.4.1]; faces as strictly convex polygons because face division and overlap algorithms need it [@ida2020, p. 176].
::: {.open #open-sheet-shapes name="sheet shapes beyond polygons" uses="def-sheet def-flat-state"} The language design for sheets as values names the circle as a shape. A disc is no polygon and has no decomposition into finitely many convex polygons, so [#def-sheet] and [#def-flat-state] exclude it as written. The generalization is a sheet bounded by finitely many algebraic arcs and faces that are convex regions bounded by segments and arcs of the sheet boundary; convexity survives cuts by lines, so the rest of the model stands. Whether to widen the definitions now or when a circular sheet is built is open; the kernel's polygon geometry is the cost either way. :::
Intuition: a folded state records where every point of the sheet lies on the table and, wherever paper lies on paper, which layer is on top. In particular a state does not remember how it was reached.1
::: {.definition #def-flat-state name="flat folded state" uses="def-sheet def-refinement def-noncrossing" defines="term-table term-face term-layer"}
Let
-
$\mathcal{F}$ is a finite set of convex polygons, the faces, with pairwise disjoint interiors and$\bigcup \mathcal{F} = P$ : the faces cover the sheet and overlap at most along their boundaries; - for every face
$A$ there is a plane isometry$\phi_A$ , a map$\mathbb{R}^2 \to \mathbb{R}^2$ that preserves distances (every such map is a composition of translations, rotations and reflections), such that$\phi_A(p) = \phi_B(p)$ for all$p \in A \cap B$ , and$f : P \to T$ is the map with$f(p) = \phi_A(p)$ for$p \in A$ . The agreement on shared boundaries makes$f$ well defined, and since the faces are finitely many closed sets,$f$ is continuous; - with $\Omega = {(A, B) \in \mathcal{F} \times \mathcal{F} : A \neq B,
\operatorname{int} f(A) \cap \operatorname{int} f(B) \neq \emptyset}$ the set of ordered pairs of overlapping faces,$\lambda : \Omega \to {+1, -1}$ is a function with$\lambda(B, A) = -\lambda(A, B)$ , and$\lambda(A, B) = +1$ reads as "$A$ lies above$B$ ": throughout their overlap,$A$ is on the up side of$B$ ;
and
Reading the notation:
One value per pair of faces is enough because the overlap of two convex faces
is a single convex region that contains no crease of either face, and the
order of two uncreased regions is constant on their overlap [@demaine2007,
§11.4.4.3; @akitaya2016, §2, consistency]. The sign is Demaine's:
::: {.term #term-table name="table"}
The plane
::: {.term #term-face name="face"}
A convex polygon
::: {.term #term-layer name="layer, above, below"}
In a region of the table where several faces overlap, the faces are the
layers, and
::: {.figure #fig-flat-state-layers caption="The preliminary base as a flat folded state, cut along --s across the diagonal, from .e to .f. Left, the folded state with the line, and arrows that show the side the section is seen from. Middle, the crease pattern with the paper the line crosses, each piece named by the face of the pattern it lies in and each folded hinge by the two pieces it joins, with .e, .m and .f where they are on the paper and a small circle wherever another layer lands on one of them. Right, the section with the stack pulled apart, the top layer first: each piece is a horizontal strip in its color, each folded hinge a turn from one strip into the next, each point a dashed line across the stack, and a dot on the layer it belongs to. The path is closed, since the line runs round the point of the base. Between .m and .f the layers are 1, 6, 5, 9, the quarters of .a, .b, .b and .c; between .e and .m they are 3, 8, 7, 10. The top and the bottom strip run flat across the diagonal at .m, from 3 into 1 and from 10 into 9, and the quarters of .b and .d are folded in half along it." views="side" along="--s" highlight="--s .e .m .f"}
paper square
mark (through .a .c) as --ac
mark (through .b .d) as --bd
mark (map --ab onto --cd) as --h
mark (map --da onto --bc) as --v
flatten (--h & --bc) (--v & --cd) (--h & --da) (--v & --ab) (--bd & .b mountain) (--bd & .d)
.m = free on --bd from .b at 1/4
--s = (perp --bd through .m)
mark (--s) (on #[.a]) as --sm
.e = --sm * --h
.f = --sm * --v
:::
A segment of positive length shared by the boundaries of two faces
::: {.lemma #lem-hinge-cases name="a hinge is flat or folded" uses="def-flat-state" defines="term-hinge"}
Let
Proof. The isometry
::: {.term #term-hinge name="hinge"}
A boundary segment of positive length shared by two faces, with an angle of
A state relates its faces in two ways, and each relation is a graph with the
faces as nodes. In the first, two faces are joined when they share a hinge;
it lives on the paper and says how the sheet hangs together. In the second,
two faces are joined when they overlap on the table, which is a pair
::: {.figure #fig-face-graphs caption="The face graphs of the preliminary base folded by one collapse, the state of [#fig-flat-state-layers] before the line --s is marked. Left, adjacency on the paper: each face is a node inside its own polygon, numbered from 1, and each hinge a path from one face through the middle of the hinge into the other, red where the hinge is a mountain, blue where it is a valley and dashed where it is flat. The two flat hinges lie on the diagonal through .a and .c, which stays flat. Right, superposition, the top layer first: a face stands one row below the lowest face above it, and a line joins two faces only when no third face lies between them, since every other pair follows from those. The base lies in two stacks that do not overlap, 1, 4, 3, 7 and 2, 6, 5, 8, so twelve of the 28 pairs of faces overlap, and
::: {.example #ex-half-square name="a square folded in half" uses="def-flat-state lem-hinge-cases"}
Let .a .b .c .d fold (map .b onto .a): .b lands on
.a. Now turn the folded square on the table by a rotation
::: {.figure #fig-half-square caption="The square of [#ex-half-square]: on the paper .b is the right corner, on the table it lies on .a, and the crease --h is the hinge between the two faces." views="cp folded" highlight=".b --h" program="shown"}
paper square
fold (map .b onto .a) as --h
:::
::: {.remark #rem-fold-and-hinge name="folds and hinges are one reflection seen twice" uses="def-flat-state lem-hinge-cases"}
The hinge relation composes the reflection on the paper side of
::: {.definition #def-refinement name="refinement equivalence" uses="def-flat-state" defines="term-refinement"}
A split of a state
::: {.lemma #lem-refinement-overlay name="refinements have a common refinement" uses="def-refinement"} Two refinements of one state have a common refinement. Consequently "having a common refinement" is an equivalence relation on states, and "the same state" in [#def-refinement] is well defined.
Proof. Let
::: {.term #term-refinement name="refinement"} Splitting faces along flat hinges, finitely often; states with a common refinement are the same state. :::
::: {.definition #def-flap name="flap" uses="def-flat-state def-refinement" defines="term-flap"}
A flap of a state is a maximal set of faces in which any two are joined by
a chain of hinges of angle
::: {.figure #fig-flap caption="The fold leaves two flaps; the marked crease --s runs through the highlighted one and splits it into two faces, which stay one flap because the hinge between them has angle
::: {.term #term-flap name="flap"}
A maximal set of faces joined by hinges of angle
Three things follow from [#def-refinement]. Which convex decomposition a
state carries does not matter: two decompositions of the same folding have a
common refinement, so they are the same state. A mark (§5) splits a face
along a flat hinge and nothing else, so it leaves the state unchanged. And
when two programs are said to reach the same folded state, this is the
equality meant: the two routes cut the sheet differently, and they agree up
to refinement.
::: {.remark #rem-linear-extension name="linear extensions" uses="def-flat-state"}
The relation "$A$ above
Intuition:
Three of the six properties in the literature need no condition here.
Existence says that
::: {.condition #cond-order name="order condition" uses="def-flat-state"}
For faces
The next two conditions speak about folded hinges. Let
::: {.term #term-taco name="taco"} Two faces joined by a folded hinge, seen near the hinge: closed along the hinge, open away from it. :::
::: {.term #term-tortilla name="tortilla"} A face whose image covers a neighborhood of a point of a folded hinge's image without that hinge being its own edge. :::
::: {.condition #cond-taco-tortilla name="taco-tortilla condition" uses="def-flat-state cond-order" defines="term-taco term-tortilla"}
Let
::: {.condition #cond-taco-taco name="taco-taco condition" uses="def-flat-state cond-order"}
Let
The last two conditions concern
::: {.condition #cond-hinge-closure name="hinge closure condition" uses="def-flat-state"}
For every hinge between faces
::: {.condition #cond-connected name="connectivity condition" uses="def-sheet def-flat-state"} The faces, joined along their hinges, form one connected piece: every face is reachable from every other through shared edges. This restates that the decomposition covers a single sheet. :::
These five conditions are what a layer ordering needs to describe paper. Each
of the first three names one way in which paper would pass through itself; the
last two say that
::: {.definition #def-noncrossing name="non-crossing layer ordering" uses="def-flat-state cond-order cond-taco-tortilla cond-taco-taco cond-hinge-closure cond-connected" defines="term-noncrossing"}
- the order condition,
- the taco-tortilla condition, and
- the taco-taco condition.
A pair
- the hinge closure condition and
- the connectivity condition
hold. :::
::: {.term #term-noncrossing name="non-crossing"} The conditions on a layer ordering that keep the paper from passing through itself. :::
::: {.lemma #lem-noncrossing-adequate name="the conditions are necessary and sufficient" uses="def-noncrossing def-flat-state"}
Let
Proof. Cited. Necessity: whenever two crease images coincide, the faces on either side are two tacos, a taco and a tortilla, or two tortillas, and any self-intersection caused by the ordering falls into one of these three cases [@hull2020, sec. 6.5, p. 123]. Sufficiency: lift each face along the third axis by its position in the ordering and join the faces along their hinges by half-cylinders; the conditions are exactly what makes this map one-to-one [@hull2020, sec. 6.5, Proposition 6.13, p. 124]. That such a placement is reached by a continuous folding motion of unstretched paper is Demaine's theorem [@demaine2007, sec. 11.6, Theorem 11.6.2], which Hull's argument leaves open, since it deforms the paper elastically [@hull2020, p. 125]. The sheet without holes is what both results assume; with holes an additional condition on the boundary curves is needed [@hull2020, Proposition 6.14]. :::
Sufficiency is what allows the model to define a flat folded state through
The last statement of this section connects the ordering on faces to the ordering on points that the literature defines. It stands here rather than in §2 because its proof needs the conditions above.
::: {.lemma #lem-face-points name="face and point orderings agree" uses="def-flat-state def-noncrossing"}
Let
Proof. Pending. The forward direction needs the non-crossing conditions of
[#def-noncrossing]; the backward direction uses that the crease pattern of a
flat folding is a straight-line graph, so its regions refine to convex faces,
and that faces are uncreased regions, so
Sources: the six properties on points and their names [@akitaya2016, §2], with Figure 1 of Hull and Zakharevich showing the two crossing patterns [@hullzakharevich2023, §2.1]; Justin's three conditions in Hull's statement [@hull2020, sec. 6.5, p. 123].
Intuition: a program names things on the paper, points, straight pieces of paper, and pieces that lie flat as one, and asks questions about them: where is this point now, which fold carries this onto that, which piece of paper holds this point. Values are the answers, and a read is the act of asking. A read looks at the current state and computes a value; it changes nothing. If the state has no answer, the read fails, and the program stops there.
Every value is a set of paper points, and a state says where those points lie on the table. A fold therefore moves every value with the paper, and no value has to be told about it. Values come in three sorts: point, bundle and flap.
::: {.definition #def-point name="point value" uses="def-sheet def-flat-state" defines="term-point"}
A value of sort point is a paper point
::: {.figure #fig-point caption=".p keeps the paper coordinate it was named with, and the fold moves only where it sits on the table." views="cp folded" highlight=".p"}
paper square
.p = free on --ab from .a at 1/4
fold (map .a onto .c)
:::
::: {.term #term-point name="point"} A paper point, named once and carried in paper coordinates; its table position depends on the state. :::
::: {.definition #def-segment name="segment" uses="def-sheet def-flat-state def-flap" defines="term-segment"}
A segment of a state is a closed straight piece of the sheet of positive
length,
::: {.figure #fig-segment caption="--s meets each of the two flaps in a segment, and the crease --h is a segment along the hinge where the flaps join." views="cp folded" highlight="--s --h"}
paper square
--s = (map .a onto .b)
fold (map .a onto .d) as --h
:::
::: {.term #term-segment name="segment"}
A straight piece of the sheet on which
::: {.definition #def-bundle name="bundle" uses="def-flat-state def-segment def-flap" defines="term-bundle term-piece"}
A value of sort bundle is a finite union of segments, a subset
::: {.term #term-bundle name="bundle"} A finite union of segments, a set of paper points; the material of a line, or a crease. :::
::: {.term #term-piece name="piece"} A maximal segment of a bundle in a state; one straight stretch within one flap. :::
::: {.definition #def-material name="material of a table line" uses="def-flat-state def-bundle def-flap" defines="term-material"}
Let
::: {.figure #fig-line caption="The material of the table line --l is one piece per flap it crosses: on the paper the two lie on either side of the crease, on the table they land on the same stretch of --l." views="cp folded" highlight="--l"}
paper square
--l = (through .a .c)
fold (map .a onto .c)
:::
::: {.term #term-material name="material"} The paper a table line crosses in a state: a bundle with one piece per flap. :::
::: {.definition #def-line name="line of a bundle" uses="def-flat-state def-bundle def-material" defines="term-line term-straight"}
A bundle
A line is needed at two places only: as the axis of a write (§5), and as an
argument of an alignment ([#def-alignment]). Both take a bundle and use its
line, so a line off the paper never arises, and a bundle that is not
straight cannot serve. Nothing in the language holds a table line across
states: --l = (map .a onto .b), then a fold, then mark (--l) scores the
pieces of --l where they lie after the fold, bent or not.
:::
::: {.term #term-line name="line"} The table line a straight bundle lies on; a read defined exactly when the bundle is straight. :::
::: {.term #term-straight name="straight"} A bundle whose table image lies on one table line in the current state. :::
::: {.definition #def-crease name="crease" uses="def-bundle def-line def-material" defines="term-crease"} A crease is a bundle that a write of §5 scored, under a name or not. Its hinges in a state are the hinges of the state that lie in it. A write scores the material of a line, so a crease is straight when scored; a later fold across it bends it, and it stays the same bundle. :::
::: {.figure #fig-bundle caption="The crease --m is straight when marked; the fold that follows bends it: on the table its two pieces meet at a right angle, and --m is the same bundle of paper." views="cp folded" highlight="--m"}
paper square
mark (map --ab onto --cd) as --m
fold (map .a onto .c)
:::
::: {.term #term-crease name="crease"} A bundle that a write scored; its hinges in a state are those of the state that lie in it. :::
::: {.definition #def-read name="read" uses="def-flat-state def-point def-bundle def-flap" defines="term-read"}
Write
::: {.term #term-read name="read"} A partial function from the current state and some values to a value; it never changes the state. :::
The reads of the language fall into three families; the line of a bundle ([#def-line]) is a fourth read that the others use.
::: {.definition #def-alignment name="alignment" uses="def-flat-state def-point def-line" defines="term-alignment"} An alignment is an incidence on the table between two objects, each the table position of a point, the line of a bundle, or the image of one of these under the reflection across the line sought: a point onto a point, a point onto a line, a line onto a line, the line through a point, the line perpendicular to a line. :::
::: {.term #term-alignment name="alignment"} An incidence on the table that the line sought has to satisfy, with one side of it reflected across that line. :::
::: {.definition #def-selection name="selection" uses="def-read def-alignment def-bundle def-material def-line def-crease def-mark def-flap" defines="term-selection term-folding-side"}
Let x onto y of
a construction is an incidence ([#def-alignment]): x onto y and
y onto x are one alignment. Its objects are points, as their table
positions, and lines. A line is the bundle the program holds under its name
([#def-bundle]), and every read of its paper below takes that bundle, as a
finite set of table segments: a crease's scored segments
([#def-crease]), a mark's extent in the flaps it was marked on
([#def-mark]), and for a construction, a name bound to one and a paper
edge, all the paper on their line ([#def-material]). The line of the bundle
([#def-line]) is the object of the incidence.
A point
A fold along x onto y when one of three holds: onto alignments. The
landing of an object is the image under
A selection heading, a point or a line toward,
optionally with one object moving, which names the side of its first anchor point off
-
Direction. With
heading, only the$\ell \in C$ whose angle with$g$ is least remain; a tie leaves all of them to the later stages. -
Folding side. With
toward, the folding side of$\ell$ is the side opposite the one$\tau$ names, undefined where$\tau$ names none; withmovingtoo,$m$ has to name that side, or the folding side is undefined. Withmovingalone, it is the side$m$ names. With neither, it is open. -
Moved material. Only the
$\ell$ remain whose folding side is defined and whose fold with it carries out the construction, or whose folding side is open and for which a fold with either side does. A remaining line with an open folding side takes the side that alone carries the construction out, or, where both do, the side of the first object of the first alignment as the program writes it; that default belongs to the write ([#def-fold]). Where that object names no side either, the write has no default and needstowardormoving. -
Landing. With a subject
$x$ , only the$\ell$ remain whose fold gives$x$ a landing, however many remain; the others would have nothing of$x$ to measure. Withtoward, among several remaining lines only those remain whose landing lies nearest$\tau$ , measured by the distance between sets,$d(A, B) = \min_{a \in A, b \in B} |a - b|$ : the landing of$x$ with a subject, the union of the landings of all objects without.
heading;
toward and moving still pass it through stages 2 and 3.
:::
::: {.term #term-selection name="selection"}
The read that keeps one line out of the candidates of a construction: by
direction with heading, by the side that folds over with toward or
moving, by whether that fold carries out every alignment, and by where it
lands the objects of the alignments.
:::
::: {.term #term-folding-side name="folding side"}
The side of a candidate line that a fold along it moves: the one opposite
toward, the one moving names, or with neither the side that carries
the construction out.
:::
::: {.definition #def-construction name="construction" uses="def-read def-alignment def-selection def-line def-material" defines="term-construction term-candidate"}
A construction is a read of sort bundle, written as a finite set of
alignments on one sought line: finitely many solutions, and no alignment
redundant [@alperin2006, §2, Definition 8]. A construction determines no
line on its own. Its candidates
::: {.term #term-construction name="construction"} A read of sort bundle: a finite set of alignments on one sought line, whose candidates a selection narrows to the one whose material is the value. :::
::: {.term #term-candidate name="candidate"} A table line that satisfies every alignment of a construction in a state and crosses paper; a line off the paper is none. :::
::: {.figure #fig-candidates caption="map .d onto --ef through .a has two candidates, the two tangents from .a to the parabola with focus .d and directrix --ef. Both cross the paper, so no line is reached until the program selects one; with toward .c the steep one remains, the start of the largest equilateral triangle in the square [@ida2020, §2.2.3, Fig. 2.17]." views="candidates" at="choose"}
paper square
mark (map .a onto .b) as --ef
@label choose
fold (map .d onto --ef through .a) as --s
:::
::: {.figure #fig-toward-boundary caption="map .d onto --ef through .p, with .p a quarter of the way along --bd from .d: .d lands at the center under one candidate and on the top edge under the other. toward keeps the candidate whose landing lies nearer, so the points as near to both landings, dotted, cut the paper in two, and each panel shades the part where a toward point selects its candidate. .c lies above the line; a point on it selects nothing." views="candidates" at="choose"}
paper square
mark (map .a onto .b) as --ef
mark (through .b .d) as --bd
.p = free on --bd from .d at 1/4
@label choose
fold (map .d onto --ef through .p) (.d toward .c) as --s
:::
::: {.figure #fig-toward-stages caption="The program of [#fig-toward-boundary], one row per stage of [#def-selection]; the fold names no heading, so stage 1 is skipped. Both candidates cross the paper and both keep the side of .c, so the side that folds over carries .d, and each fold carries .d onto --ef. The landing stage decides: .d lands on the top edge under one candidate and at the center under the other, and the top edge lies nearer .c." views="stages" at="choose"}
paper square
mark (map .a onto .b) as --ef
mark (through .b .d) as --bd
.p = free on --bd from .d at 1/4
@label choose
fold (map .d onto --ef through .p) (.d toward .c) as --s
:::
::: {.lemma #lem-selection-defined name="a selection is a partial function" uses="def-selection def-construction"}
For every state, arguments and items, each stage of [#def-selection] is
determined, and
Proof. The candidates are finitely many ([#def-construction]), so every
stage filters a finite set. Stage 1 compares angles between lines, a
function of the lines alone. In stage 2, a point either lies on moving names is that of one point, its
first anchor point off
In the kernel the comparisons are exact: squared distances between points and segments, and squared cosines between lines, are rational functions of the coordinates, so they stay in the field the coordinates lie in.
::: {.lemma #lem-selection-carries-out name="a remaining line carries out its alignments" uses="def-selection def-alignment"}
Let onto alignment of the construction hold as an incidence of
the table positions. Conversely, an alignment whose two objects both lie
outside
Proof. x onto y ([#def-alignment]):
The lemma speaks about the half-plane fold moves is its scope ([#def-fold]): every layer on
::: {.lemma #lem-crossing-landing name="where a crossing line lands" uses="def-selection"}
Let a construction fold a line (m toward τ) measures the
landing of
- If the landing under
$b_2$ lies on the opposite ray,$\tau$ is as near to one landing as to the other exactly when$s = 0$ :$\tau$ lies on the perpendicular to$n$ through$X$ . - If it lies on the same ray, with lengths
$l_1 \le l_2$ of the two landings,$\tau$ is as near to one as to the other exactly when$l_1 = l_2$ or$s \le l_1$ .
Proof. Every point of
The squared distance from
For --v folded onto --h in the square, the figures of issue #58, both
parts of --v have length (--v toward τ) case 2 is a
tie at every point, and case 1 ties on --v itself. A bare toward
measures the landing of --h as well, which lands on the rays of --v by
the same argument with the roles of the two lines exchanged, and adds ties
of its own.
::: {.open #open-several-sought-lines name="constructions that seek more than one line" uses="def-construction def-alignment"}
[#def-construction] puts its alignments on one sought line, which is where
the seven Huzita-Justin axioms live. The same alignments distributed over two
lines sought at once give the 489 two-fold axioms [@alperin2006, §3, §4],
which packages/multifold ([[decision/0020]]) enumerates. A candidate is then a pair
of lines, a selection keeps one pair, and a write takes two axes and moves
them together, so the definitions of candidate, selection and write all widen
by the same step. Which of them the language will carry, and whether a
two-fold write is one write or a pair, is not decided.
:::
::: {.definition #def-selector name="selector" uses="def-read def-flap def-point def-bundle def-meet"} A selector is a read of sort flap or point that resolves a description by incidence in paper coordinates: the flap whose faces contain every listed point; the point where bundles meet ([#def-meet]); the point on a bundle of a single piece at a given fraction of that piece's length from a named endpoint. Each is defined exactly when the description picks out one thing. :::
::: {.definition #def-meet name="meet" uses="def-read def-sheet def-bundle" defines="term-meet"}
Let
::: {.figure #fig-meet caption="--h and --v each lie on two paper lines after the reverse folds, a scar and its mirror image, and have one point in common, the center .o." views="cp folded" highlight="--h --v .o"}
paper square
fold (map .a onto .c) as --bd
reverse (map .b onto .c) as --h
reverse (map .d onto .c) as --v
.o = --h * --v
:::
::: {.term #term-meet name="meet"} The one paper point that two or more bundles have in common; a read defined exactly when their intersection is a single point. :::
::: {.definition #def-filter name="filter" uses="def-read def-bundle def-line def-flap"}
The filters are the reads of sort bundle that form the Boolean algebra of
subsets of the pieces of a bundle
Intuition: a write takes the current state and a few values and yields the
next state, or fails. Every write of the language is built from one
construction: some faces are reflected across a table line, and the layer
ordering is rebuilt around them. Which faces move, the moving set, is what
separates folding one flap from folding through the stack; where the moved
faces come to lie, the placement, is what separates a valley fold from a
mountain fold from a tuck. mark reflects nothing, flip reflects
everything, fold reflects one block, reverse reflects two blocks in one
move, and flatten moves the sectors of a fan by different motions. This
section defines the construction once and then each write as an instance of
it, with its parameters and its domain.
::: {.definition #def-write name="write" uses="def-flat-state def-noncrossing def-read" defines="term-write"}
A write with parameter sorts
::: {.term #term-write name="write"} A partial function from the current state and some values to the next state; where it is undefined the program fails. :::
::: {.definition #def-score name="scoring" uses="def-flat-state def-refinement def-bundle" defines="term-score"}
For a state
::: {.term #term-score name="score"} Split faces along a bundle without moving anything; the state is unchanged up to refinement. :::
::: {.definition #def-effective name="effective write" uses="def-write def-score def-refinement" defines="term-effective"} A write is effective in a state when its value is a different state in the sense of [#def-refinement]. A score is exactly a write that is not effective: by [#def-score] its value is the state it was given. A read is effective nowhere, since it yields no state at all. :::
::: {.term #term-effective name="effective"} A write whose value is a different state; a score is not one, and a read is no write. :::
::: {.open #open-writes-on-the-quotient name="whether a write acts on the states read up to refinement" uses="def-effective def-refinement def-write"} A write is stated here on a state, so effective is a property of a write at a state. The stronger reading is that every write descends to the states read up to refinement ([#def-refinement]): applied to two refinements of one state, a write yields two states with a common refinement, so it induces a map there, and a score induces the identity while an effective write does not. The text argues the intuition for scoring below, that a write may score every face its axis crosses because scoring changes nothing, and [[reference/kernel]] records that the representation does not quotient. The statement is not proved here, and nothing in the model rests on it. :::
Every write below scores its axis first, so that each face lies on one side of the axis before any face moves. Because scoring changes nothing, a write may score every face the axis crosses, moving or not; the hinges that end up between two stationary faces stay flat and vanish again under refinement.
::: {.definition #def-mark name="mark" uses="def-write def-score def-line def-flap def-bundle"}
The write mark takes a line
mark is the identity on states. The read/write law of the language
sequences it as a write because it introduces a piece of material that
later reads select and later folds fold along; the model records that
material as a value in paper coordinates, and the state itself has no
memory of it. The mountain or valley intent a program may write beside a
mark is an annotation for the crease pattern output and no part of the
state or the value.
::: {.open #open-point-mark name="a mark at a point" uses="def-mark def-segment def-bundle"}
A mark whose extent is a single point yields a segment of length zero, which
[#def-segment] excludes from bundles. The language admits such a mark as a
crease whose material is one point on
::: {.definition #def-letter name="letter of a folded hinge" uses="def-flat-state" defines="term-letter term-face-up"}
Let
::: {.term #term-letter name="letter, mountain, valley"} Mountain or valley, derived for every folded hinge from which of its two faces is face up and which is above. :::
::: {.term #term-face-up name="face up, face down"} A face is face up in a state when its isometry preserves orientation; the front of the paper shows. :::
The letter is the folder's mountain and valley seen from the front of the paper, and it is a property of the state: no write takes a letter as an instruction, and every letter in an output is read off the state.
::: {.definition #def-reflection name="reflection of blocks" uses="def-flat-state def-score def-line cond-hinge-closure def-noncrossing" defines="term-block term-placement term-moving-set"}
Let
-
$f'|_F = \rho \circ f|_F$ for$F \in \mathcal M$ , and$f'|_F = f|_F$ for stationary$F$ ; - two faces of one block that overlap under
$f'$ overlapped under$f$ and reverse their relation:$\lambda'(A, B) = \lambda(B, A)$ . A rigid half turn reverses a stack; - two stationary faces keep their relation;
- a face
$F$ of a block$(M, \pi)$ and a stationary face$G$ that overlap under$f'$ are ordered by$\pi$ :$F$ is above$G$ for top and below$G$ for bottom. For over $T$,$F$ is above$G$ unless$G$ lies above every face of$T$ it overlaps, in which case$F$ is below$G$ ; for under $T$,$F$ is below$G$ unless$G$ lies below every face of$T$ it overlaps. Both placements require$T$ to cover the landing footprint: every point of$f'(F)$ lies in the image of some face of$T$ ; - faces of two different blocks are ordered as their placements are ordered
in the stack: a block placed bottom below every other block, a block
placed top above every other, a block placed at
$T$ below a block placed at$T'$ when every face of$T$ lies below every face of$T'$ it overlaps, and a block placed under $T$ below a block placed over $T$. Two blocks whose placements are not so ordered are outside the domain.
The reflection is the candidate a write returns: it is the next state when it satisfies [#def-noncrossing] and undefined otherwise. :::
::: {.term #term-block name="block"} A set of faces on one side of the axis together with the placement they receive after reflection. :::
::: {.term #term-placement name="placement"} Where a reflected block comes to lie among the stationary faces: outside above, outside below, or immediately above or below a set of stationary faces. :::
::: {.term #term-moving-set name="moving set, stationary"} The faces a write reflects; every other face is stationary. :::
Hinge closure ([#cond-hinge-closure]) is where the reflection fails when the
paper would tear: a hinge that joins a moving face to a stationary face off
the axis leaves
::: {.lemma #lem-toggle name="hinges toggle on the axis" uses="def-reflection cond-hinge-closure"}
Let
Proof. Write
The lemma is why an unfold needs no construction of its own: reflecting a
block back across a folded hinge returns that hinge to angle unfold ([#def-unfold]).
::: {.definition #def-fold name="fold" uses="def-write def-reflection def-flap def-score def-line" defines="term-anchor term-depth"}
The write fold takes a table line
- hinges off the axis: a candidate joined to a face of
$M$ by a hinge, folded or flat, whose image does not lie on$\ell$ is in$M$ , since the paper cannot tear there; with the flat hinges a flap moves as a whole ([#def-flap]); and, - outward closure: a candidate that lies above a face of
$M$ is in$M$ for top, and one that lies below a face of$M$ is in$M$ for bottom. For under $T$ a candidate outside$T$ that lies above a face of$M$ and below every face of$T$ it overlaps is in$M$ , and for over $T$ one that lies below a face of$M$ and above every face of$T$ it overlaps. The faces of$T$ and the layers beyond them stay.
The value of the write is the reflection of the single block
::: {.term #term-anchor name="anchor"} The point or flap a fold names its side by: the side of the axis its image lies on folds over. It names that side and nothing else. :::
::: {.term #term-depth name="depth"} The deepest flap a fold reaches where the program names one; the moving set grows outward from it, up to the target of a placed fold. Without one, every layer on the moving side moves. :::
The language derives moving item, or
the object a construction moves, and the side its image lies on. A point on
the axis names no side, and a flap that straddles the axis without a point
names none either; both are outside the domain. mountain is the placement
bottom and the default is top; up to names over and
under name over or under a flap, the layers outward of fold: without unfold ([#def-unfold]) turns some of the layers over such a line.
::: {.figure #fig-fold-default caption="--f folds the corner through both layers: without up to the moving set is every layer on the side of .b. The crease reads valley on the face-up layer and mountain on the face-down one." views="cp folded" highlight="--f .b"}
paper square
fold (map .b onto .a)
.p = free on --bc from .b at 1/4
.q = free on --ab from .b at 1/4
fold (through .p .q) (moving .b) as --f
:::
::: {.figure #fig-fold-depth caption="The same fold given the top layer as its depth: the moving set grows outward from the flap carrying .b, and the layer beneath it stays. The crease reads mountain because that layer lies face down." views="cp folded" highlight="--f"}
paper square
fold (map .b onto .a)
.p = free on --bc from .b at 1/4
.q = free on --ab from .b at 1/4
fold (through .p .q) (moving .b) (up to .b) as --f
:::
::: {.figure #fig-fold-op caption="The terms of --f in [#fig-fold-depth] on the state it reads: the axis dashed and the moving set filled, the corner of the top layer alone. The layer beneath it is a candidate and stays, since the moving set grows outward from the depth. On the right the state after the fold." views="op" at="f"}
paper square
fold (map .b onto .a)
.p = free on --bc from .b at 1/4
.q = free on --ab from .b at 1/4
@label f
fold (through .p .q) (moving .b) (up to .b) as --f
:::
::: {.corollary #cor-fold-letters name="letters of an outside fold" uses="def-fold def-letter def-reflection"} For a fold placed top, every hinge it scores reads valley where the face was face up before the fold and mountain where it was face down; for a fold placed bottom the other way round.
Proof. Let
A placed fold has no such rule. Its letter is read off the finished state and depends on the layer the block is inserted against: tucking a corner under a face-down layer reads valley, under a face-up layer mountain.
::: {.figure #fig-fold-tuck caption="A pocket tuck: after the sheet is folded in half, the corner .b of the top layer is placed beneath .p, into the gap between the two layers. The crease --t reads valley because the layer it goes beneath lies face down." views="cp folded" highlight="--t .b"}
paper square
fold (map .a onto .d)
.m = free on --bc from .b at 1/2
.n = free on --ab from .b at 1/2
.p = free on --ab from .a at 1/4
fold (through .m .n) (moving .b) (up to .b) (under .p) as --t
:::
::: {.remark #rem-simple-fold name="simple folds" uses="def-fold lem-noncrossing-adequate"}
A fold placed top or bottom is a some-layers simple fold in Demaine's
sense: a rigid rotation of some layers under the crease segment through
::: {.lemma #lem-fold-closed name="an outward-closed fold crosses nothing" uses="def-fold def-reflection def-noncrossing cond-hinge-closure"}
Let
Proof. Pending. The order condition holds because the relation on
stationary pairs is unchanged, the relation on moving pairs is reversed, and
every moving face lies outside every stationary face it overlaps. The two
taco conditions need the case analysis at a crease image: a new taco on
::: {.definition #def-unfold name="unfold" uses="def-write def-fold def-reflection def-flap lem-toggle"}
The write unfold takes a table line
The value of the write is the reflection of the single block
::: {.corollary #cor-unfold-opens name="an unfold opens and folds nothing" uses="def-unfold lem-toggle cond-hinge-closure"}
In the value of an unfold, every hinge on
Proof. By [#lem-toggle] a hinge on
The language takes the side moving item, else
from the flap up to names, else from the point of the toward item; up to names moving does, and toward names (moving … down) gives the placement bottom, and (moving … up), the
default, top: the direction of the moving set and the side of the stack it
lands on are one choice. The axis is a
crease the program has scored, since the hinges an unfold opens lie on the
paper already. A hinge on fold writes that.
::: {.figure #fig-unfold caption="After two folds in the same direction every layer lies beside --q. unfold turns the layer of .b back over it, with the two layers above, which would be swept through otherwise: the hinge on --q between those layers and the bottom layer opens, and the hinge on --q among the moving layers stays folded." views="cp folded" highlight="--q .b"}
paper square
fold (map .b onto .a) as --d
.m = --d * --ab
fold (map .m onto .a) as --q
unfold (--q) (moving .b)
:::
::: {.definition #def-flip name="flip" uses="def-write def-flat-state def-noncrossing"}
The write flip takes no argument. For a state
::: {.lemma #lem-flip name="flip preserves everything but the side" uses="def-flip def-letter def-noncrossing"}
The value of flip is a state. Every hinge keeps its angle and every folded
hinge keeps its letter; every face changes between face up and face down.
Proof. The order, taco-tortilla and taco-taco conditions are stated
symmetrically in above and below, so
Which reflection
::: {.figure #fig-flip caption="With the sheet turned face down, the crease --g scored by a fold placed on top reads mountain: the folder turned the paper over and made a valley on its back." views="cp folded" highlight="--g"}
paper square
flip
fold (map .a onto .c) as --g
:::
::: {.definition #def-reverse name="reverse fold" uses="def-write def-reflection def-fold def-flap def-letter def-flat-state" defines="term-tip term-opening term-block term-spine term-body"}
The write reverse takes a table line
::: {.term #term-tip name="tip"} The material a reverse fold or a flatten moves: beyond the axis or outside the stayer's wedge, and joined to the anchor. :::
::: {.term #term-opening name="opening"} The place between two layers of the tip where a reverse fold opens it: every hinge that crosses it is folded and lies on the spine. :::
::: {.term #term-block name="block"} The layers of the tip on one side of the opening, reflected as a whole. :::
::: {.term #term-spine name="spine"} The table line the hinges across the opening lie on. The reverse fold turns those hinges the other way. :::
::: {.term #term-body name="body"} The stationary faces a block of the tip is hinged to along the axis. :::
The two blocks move in one reflection and never one after the other: once one block has moved, a hinge across the opening joins a reflected face to an unreflected one along no common segment, and hinge closure fails. Inside, each block lands next to its own body in the gap between the two bodies; outside, the lower block goes under everything and the upper block on top.
A tip of one flap folded once has one opening, between its two layers. A tip of several layers can have several: the square of [#fig-reverse-open] opens between its two inner layers or below its outermost one, and the write is undefined until a letter keeps one of them. A letter names a hinge of the spine by its crease and a point on it, as a letter of a flatten names a ray.
A reverse fold is the fan ([#def-flatten]) at the point where
::: {.figure #fig-reverse caption="The preliminary base by two inside reverse folds [@ida2020, §7.4.3]: the diagonal fold makes a triangle whose spine is --bd, and each acute corner is reversed to the right-angle corner in turn." views="cp folded" highlight="--h --v --bd"}
paper square
fold (map .a onto .c) as --bd
reverse (map .b onto .c) as --h
reverse (map .d onto .c) as --v
:::
::: {.figure #fig-reverse-op caption="The terms of --h in [#fig-reverse] on the triangle it reads: the axis dashed, the spine on --bd, the two blocks of the tip hatched in two directions below the axis, where they lie on one another, and their bodies above it, each block and its body in one color. On the right the state after the reverse fold." views="op" at="h"}
paper square
fold (map .a onto .c) as --bd
@label h
reverse (map .b onto .c) as --h
reverse (map .d onto .c) as --v
:::
::: {.figure #fig-reverse-open caption="A square folded in half twice in the same direction, its lower half inside-reversed along the middle, cut along the top edge. The tip opens between its two inner layers, and the letter on the inner hinge of --e through .q keeps that opening: both hinges on the spine turn, 5|8 and 6|7, nested inside 2|3 and 1|4, and the lower half's layers read 8, 7, 6, 5 between 3 and 2. On the other edge the hinge 7|8 keeps its letter." views="side" along="--top"}
paper square
fold (map .b onto .a) as --d
fold (map --d onto --da) as --e
.q = free on --cd from .c at 1/4
reverse (map .a onto .d) (--e & .q valley) as --r
.p = free on --cd from .d at 1/4
--top = (through .d .p)
:::
::: {.figure #fig-reverse-open-outer caption="The same square with a mountain on the inner hinge: the tip opens below its outermost layer. Only the outer hinge 5|6 turns, the inner one, 7|8, keeps its letter, and the three inner layers of the lower half go in as one block, 8, 7, 6 between 2 and 5." views="side" along="--top"} paper square fold (map .b onto .a) as --d fold (map --d onto --da) as --e .q = free on --cd from .c at 1/4 reverse (map .a onto .d) (--e & .q mountain) as --r .p = free on --cd from .d at 1/4 --top = (through .d .p) :::
::: {.corollary #cor-reverse-letters name="letters of a reverse fold" uses="def-reverse def-letter cor-fold-letters def-reflection"}
Every hinge across the opening reverses its letter, and every other hinge of
the tip keeps its letter. Where a hinge across the opening crosses
Proof. Both blocks are reflected, so in each the face-up faces become face
down and the face-down ones face up. Inside a block the reflection also
reverses the order of the layers, so a hinge with both faces in one block
keeps its letter by [#cor-fold-letters]. A hinge across the opening joins a
face
::: {.definition #def-flatten name="flatten" uses="def-write def-flap def-score def-reflection def-letter def-noncrossing def-selection" defines="term-fan term-sector term-stayer term-emergent"}
The write flatten takes a point
- If
$k$ is even, the composition$\rho_1 \circ \cdots \circ \rho_k$ must be the identity; this is Kawasaki's condition that the alternating sum of the angles between consecutive rays vanishes [@hull2020, §5.3]. - If
$k$ is odd, the composition is a reflection across a line through$f(O)$ , since an odd number of reflections through a point reverses orientation and fixes the point. Each of the two rays of that line that lies strictly inside a gap between consecutive given rays is an emergent ray; adding it makes the composition close. Each choice is a candidate fan.
Call the
A hinge on a ray with a piece of
- a letter for a ray: of the hinges of the ray's crease on that ray that do not open, the one whose face on the clockwise side lies lowest has that letter;
- one sector over another: the two pieces are so ordered;
- the stayer, which only fixes where the result lies on the table.
A ray may run along hinges of
The value of the write is the one candidate state
::: {.term #term-fan name="fan, ray"} The segments from one vertex along which a flatten folds at once. :::
::: {.term #term-sector name="sector"} A piece of the tip between the hinges on the rays of a fan. It moves by the creases on its paper path from the stayer ([[decision/0044]]). :::
::: {.term #term-stayer name="stayer"} The wedge of a flatten whose pieces keep their place; it fixes where the result lies on the table. :::
::: {.term #term-emergent name="emergent ray"} The ray a flatten with an odd number of given rays has to add for the vertex to fold flat. :::
The construction is the folding map of flat-folding theory, restricted to
the hinges the fan changes [@hull2020, Def. 6.5]. On a single sheet a path
from the stayer to a piece crosses the rays between the stayer's wedge and
the piece's wedge, so every piece of a wedge moves by the composition of the
reflections across those rays, the single-vertex fan of
[@hull2020, chapter 5]. On folded paper two pieces of one wedge can move
differently: the squash of one flap of the preliminary base turns a piece of
the top layer about the vertex and reflects the piece of the second layer
beside it across the axis. Kawasaki's theorem says that the closure
condition is exactly flat-foldability of a vertex the paper surrounds, and
Maekawa's theorem, that the letters around it differ in number by two,
holds in every candidate state because a candidate state is a flat folded
state [@hull2020, §5.2, §5.3]. A layer under the fan moves with its sector
when it hangs on
::: {.figure #fig-flatten caption="The preliminary base by one collapse at the center: six rays fold, the diagonal through .a and .c stays flat, and the ordering constraint puts the a-quarter in front of the b-taco." views="cp folded" highlight=".a .c"}
paper square
mark (through .a .c) as --ac
mark (through .b .d) as --bd
mark (map --ab onto --cd) as --h
mark (map --da onto --bc) as --v
.q = free on --ab from .a at 1/4
.r = free on --ab from .b at 1/4
flatten (--h & --bc) (--v & --cd) (--h & --da) (--v & --ab) (--bd & .b) (--bd & .d) (.q over .r) (toward .q)
:::
::: {.figure #fig-flatten-op caption="The terms of the collapse in [#fig-flatten]: the vertex at the center, the six rays, and the stayer, the quarter between the rays on --h and --v that holds the diagonal to .c. Every other sector moves by the reflections across the rays between it and the stayer; on the right the state after the collapse." views="op" at="collapse"}
paper square
mark (through .a .c) as --ac
mark (through .b .d) as --bd
mark (map --ab onto --cd) as --h
mark (map --da onto --bc) as --v
.q = free on --ab from .a at 1/4
.r = free on --ab from .b at 1/4
@label collapse
flatten (--h & --bc) (--v & --cd) (--h & --da) (--v & --ab) (--bd & .b) (--bd & .d) (.q over .r) (toward .q)
:::
::: {.figure #fig-flatten-states caption="The candidate states of a four-ray vertex, the midline on both sides and the half-diagonals to .c and .b, each as its crease pattern, mountains red and valleys blue. The sectors are 45°, 135°, 135° and 45°, so opposite sectors sum to 180° and the vertex folds flat. Every state has three rays of one letter and one of the other. The three with three mountains are removed; the three with one mountain each remain, and without toward the program fails as ambiguous ([#open-flatten-selection])." views="candidates" at="vertex"}
paper square
mark (through .a .c) as --ac
mark (through .b .d) as --bd
mark (map --ab onto --cd) as --h
@label vertex
flatten (--h & --bc) (--ac & .c) (--h & --da) (--bd & .b)
:::
::: {.figure #fig-flatten-toward caption="The same vertex with toward .c: of the three states with one mountain, two put less of the material toward .c on top than the third, which remains." views="candidates" at="vertex"}
paper square
mark (through .a .c) as --ac
mark (through .b .d) as --bd
mark (map --ab onto --cd) as --h
@label vertex
flatten (--h & --bc) (--ac & .c) (--h & --da) (--bd & .b) (toward .c)
:::
::: {.open #open-flatten-selection name="what selects among the candidates of a flatten" uses="def-flatten def-selection"}
[#def-flatten] leaves toward is three rules in
sequence: the candidate whose moved material lies toward the named point,
among those the ones with the fewest mountains on the given rays, among
those the one whose material toward the point lies on top. The first is a
selection in the sense of [#def-selection]; the other two are conventions that
pick a folder's habit out of several states that are all flat folded. Whether
they belong in the model as named selections, or the language should ask for
a constraint instead when several states remain, is not decided.
:::
::: {.definition #def-squash name="squash" uses="def-write def-flatten def-flap def-letter" defines="term-vertex"}
The write squash takes a spine flatten ([#def-flatten]) at
::: {.term #term-vertex name="vertex"} The end of a squash's spine inside the paper, where the other folded hinges of its flap meet; the point of the squash's fan. :::
A squash is the step a diagram gives with one word and an arrow: the flap stands up, opens, and comes down flat with its spine on the target. On the preliminary base the flap's two layers lie on each other mirrored at the spine, so the axis is one line on the table and two creases on the paper, one per layer, and the half of the front face beyond the center line keeps its place.
::: {.figure #fig-squash caption="The squash of the front flap of the preliminary base on the side of --da: its spine on --h opens and lands on --ac; the axis --s through the closed corner folds each layer of the flap, and the other half of the front face stays." views="cp folded"}
paper square
mark (through .a .c) as --ac
mark (through .b .d) as --bd
mark (map --ab onto --cd) as --h
mark (map --da onto --bc) as --v
.q = free on --ab from .a at 1/4
.r = free on --ab from .b at 1/4
flatten (--h & --bc) (--v & --cd) (--h & --da) (--v & --ab) (--bd & .b) (--bd & .d) (.q over .r) (toward .q)
squash (--h & --da onto --ac) as --s
:::
To be written: a program as a finite sequence of states.
::: {.open #open-several-sheets name="several sheets and bodies" uses="def-sheet def-flat-state def-noncrossing cond-connected"}
The language design for sheets as values lets a program
hold several sheets and assemble them into a body. In the model a multi-sheet
program state is a family of flat folded states, one per sheet, and an
assembled body is a flat folded state of the disjoint union of its sheets: one
Each entry gives the meaning in one line and points to the definition that fixes it.
Footnotes
-
An implementation may record the history for its own purposes. Nothing in this document depends on such a record, and no operation may read it. ↩