promoted from
data/fprd-lab/fold-look/wfl-weak-fold-look-model.mdon 2026-07-28 — status: unverifiedWFL: one deliberately weak fold-and-look model. Unit cells, integer creases, at most one site per cell centre, and radius strictly between 0 and 1/2. Proposition W1 proves the four geometric hypotheses (GP)(NC)(IN)(UF); positivity of the radius is part of the model. Thus all five standing conditions hold structurally, the incidence normal form is unconditional in WFL, and order-preservation is automatic. Machine-checked over 4000 positive-radius programs.
WFL: one deliberately weak fold-and-look model
Status: consolidation. Proved here; the point of the model is that it proves less than its predecessor while assuming nothing. Role note. This lane is now consolidation and adversarial checking. It is not choosing the next abstraction and is not proposing a theory.
Contents
1. Why a weak model, and which weakness
The independent audit refuted Theorem 1 because hypothesis (UF) — uniform overlay — was missing. (UF) is checkable but it is an assumption, and an assumption that had to be discovered by counterexample is exactly the kind a lower-bound programme should not rest on.
A deliberately weak model earns its keep by converting fragile hypotheses into structural facts. WFL does that for all four geometric hypotheses and pins the fifth condition, , in the model definition.
2. The model
WFL. A presentation consists of:
- a strip of unit cells, original addresses ;
- at most one site per cell, at the cell centre , with punch radius fixed globally;
- one control literal per site — , , , or ;
- an input-independent program of simple folds whose crease lies at an integer image coordinate;
- no
Cut, noPunch, noUnfold; one finalLook.
Restrictions relative to : crease positions are integral rather than arbitrary; site positions are forced rather than chosen; one site per cell rather than many; the punch radius is global.
3. The four hypotheses become theorems
Proposition W1. In WFL, (GP), (NC), (IN) and (UF) hold for every legal presentation.
Proof. By the enumerator lane’s Theorems A and B, after any sequence of complexity-1 folds is piecewise with , and every piece boundary lies in of a crease line. Since creases are at integer image coordinates and maps integers to integers with unit slope, every piece endpoint has integer original and image coordinate.
(NC). A punch spans , which contains no integer, hence no piece boundary.
(UF). Piece-endpoint images are integers. The punch image is an interval of radius about a half-integer, so it contains no integer. Hence no layer boundary lies inside a punch image, which is precisely (UF).
(GP). Within a piece is an isometry, so distinct site images are at distance . Across pieces, images are half-integers, so two site images are equal or differ by at least 1.
(IN). The footprint has integer endpoints and every punch image lies inside an open unit interval between consecutive integers, at distance from the footprint boundary.
Machine-checked over 4 000 random WFL programs (, ): zero violations of any of the four.
Corollary W2. In WFL, the incidence normal form (Theorem 1) holds unconditionally, and with it and .
This is the consolidation the model exists for. The theorem that was false in is true in WFL with no side conditions to verify.
4. What WFL gives up, stated plainly
- The palindrome construction transfers (rescale so cells are unit and the fold line is a cell boundary), so nothing proved about palindrome is lost.
- The unrestricted statement fails for constant , a definitional mismatch rather than a geometric one. For nonconstant , Theorem 1 supplies the exact DNF and proves .
- Hypothesis (OP), order preservation, is automatic in WFL — sites are at cell centres in index order — so Theorem 19 and the LIS separation apply without the encoder hypothesis that the audit demolished in its (PF) form.
- Constructions needing sub-cell site placement or non-integer creases are outside the model. Whether any target needs them is open and is not something this lane will decide.
5. Status
Proved here: W1, W2. Inherited: Theorems A and B (enumerator lane), which hold for arbitrary complexity-1 folding steps and therefore cover WFL a fortiori.
Not claimed: that WFL is the right model, that it is maximal among weak models, or that anything outside it is unrealizable.