Render square Wang solutions as hexagons

README.md

@@ -56,8 +56,9 @@ benchmark case. It does not require a GPU.
 ## Current status
 
 The implemented components cover the square pipeline from `.cm13` input
-through a verified solution document and the separate diagnostic PNG command.
-Hex translation and parallel solving remain future work.
+through a verified solution document, the default square diagnostic PNG, and
+the checked presentation-only square-to-hex view selected by `--hex`. Parallel
+solving remains future work.
 
 | Capability | Status |
 | --- | --- |
@@ -69,8 +70,8 @@ Hex translation and parallel solving remain future work.
 | Wang Z3 oracle | Implemented over copied `Region + TILESET` |
 | Boolean–Wang witness correspondence | Implemented; exhaustive evidence covers all 1,701 canonical formulas through three variables and 27,044 constrained native solves |
 | Verified square solution export | Implemented as the closed `wang-solution-v1` contract and deterministic exporter |
-| Wang square diagnostic renderer | Implemented as a separate presentation-only CLI in the isolated `renderer/` project |
-| Square-to-hex translation and verification | Not implemented; the two Python modules are empty placeholders |
+| Wang diagnostic renderer | Implemented as one presentation-only CLI with byte-stable square default and explicit `--hex` mode in the isolated `renderer/` project |
+| Square-to-hex presentation port | Implemented as a pure in-memory Basire/Culik mapping with a raster-independent checker; no hex solver, schema, or core model |
 | Native C JSON layer | Not implemented; `src/io/json.c` is a placeholder |
 | `TaskPlan` and native OpenMP solver | Not implemented; only the build scaffold exists |
 
@@ -108,13 +109,17 @@ The implemented paths are:
                           copied tiling + Python checker
                                      |
                                      v
-                          wang-solution-v1 --> square PNG
+                          wang-solution-v1 --> square PNG (default)
+                                     \
+                                      +--> pure hex port/check --> hex PNG (--hex)
 ```
 
 The witness bridge relates exact Boolean assignments to the variable cells of
 the same live Yang–Zhang reduction. Its precise scope and evidence are recorded
 in the [witness correspondence design](docs/designs/2026-08-21-witness-extension-design.md).
-The square-to-hex and OpenMP stages are not part of the implemented diagram.
+The square-to-hex branch changes presentation only; it consumes the same
+square witness after verification. OpenMP is not part of the implemented
+diagram.
 
 ## Correctness boundaries
 
@@ -130,6 +135,9 @@ The square-to-hex and OpenMP stages are not part of the implemented diagram.
   independent formula checker.
 - Witness correspondence does not claim a unique tiling for each assignment or
   that extending an extracted assignment reproduces the original tiling.
+- The hex port is a bijection over the image tile table, not a second solver or
+  correctness oracle. Its pure checker proves translation equivalence while
+  leaving source solution validation upstream.
 - OpenMP is introduced only after the serial path is correct and measurable.
 - Project conventions must be distinguished from claims inherited from the
   Yang–Zhang paper.
@@ -138,12 +146,10 @@ The square-to-hex and OpenMP stages are not part of the implemented diagram.
 
 Planned work remains separated into independently reviewed changes:
 
-1. formalize, implement, and independently verify square-to-hex translation,
-   then add the explicit hex mode to the existing Wang renderer command;
-2. evaluate MRV indexing on weakly constrained search and build a separate
+1. evaluate MRV indexing on weakly constrained search and build a separate
    hard-UNSAT corpus before making parallelism claims;
-3. harden allocation and cleanup failure paths before concurrent execution;
-4. define and validate a minimal serial `TaskPlan` before implementing OpenMP.
+2. harden allocation and cleanup failure paths before concurrent execution;
+3. define and validate a minimal serial `TaskPlan` before implementing OpenMP.
 
 The implementation follows a deliberately small design rule: each datum has one
 owner, derived state is computed when needed, and future metadata is not added to
@@ -166,7 +172,7 @@ make check
 
 The imported renderer remains a separate locked Python project. Its Pillow and
 NumPy dependencies are not installed by the root project or exercised by
-`make check`. Run its 189-test combined suite independently:
+`make check`. Run its 213-test combined suite independently:
 
 ```sh
 cd renderer
@@ -177,7 +183,7 @@ CI mirrors that command in a separate read-only Python 3.14 job. Snapshot
 provenance and update instructions are recorded in
 [`renderer/UPSTREAM.md`](renderer/UPSTREAM.md).
 
-To exercise the Wang square renderer on the versioned solution fixture:
+To exercise the Wang renderer on the versioned square solution fixture:
 
 ```sh
 cd renderer
@@ -186,8 +192,20 @@ uv run --locked python wang_square.py \
   output/wang-square.png
 ```
 
+The same command produces the checked pointy-top axial presentation only when
+the explicit flag is present:
+
+```sh
+uv run --locked python wang_square.py \
+  ../tests/fixtures/wang_solution_v1_square_sat.json \
+  output/wang-hex.png \
+  --hex
+```
+
 The [square solution contract](docs/wang_solution_v1.md) includes the producer
-API for exporting a verified native result before rendering it.
+API for exporting a verified native result before rendering it. The
+[square-to-hex reference](docs/wang_square_to_hex.md) defines the mapping,
+inverse proof, checker boundary, and integer axial raster convention.
 
 Useful individual targets:
 
@@ -270,8 +288,8 @@ python/native/   C ABI adapters and ownership boundaries
 python/formats/  versioned solution validation and deterministic export
 python/crosscheck/ scoped native/Z3 witness orchestration
 python/oracles/  independent Z3 oracles and witness checks
-python/hex/      empty square-to-hex placeholders
-renderer/        isolated legacy and Wang square PNG rendering
+python/hex/      deliberately unused empty hex-core placeholders
+renderer/        isolated legacy and square/default, hex/explicit Wang rendering
 tests/           C, Python, and instance regressions
 benchmarks/      fixed reference corpus and profiling runner
 docs/            theory and architecture references
@@ -294,8 +312,8 @@ The [GitHub Pages documentation](https://xtraid.github.io/tiling-foundry/)
 organizes the technical material by reader interest:
 
 - **Architecture and correctness** covers module ownership, the serial solver,
-  independent verification, Boolean–Wang witness correspondence, and the
-  square solution data contract.
+  independent verification, Boolean–Wang witness correspondence, the square
+  solution data contract, and the presentation-only square-to-hex proof.
 - **Yang–Zhang reduction** covers geometry, formula-to-region construction,
   proof obligations, and primary references.
 - **Solver optimization** separates the current methodology from dated,

docs/development_principles.md

@@ -96,7 +96,8 @@ A module is implemented when it has:
 | `python/crosscheck` | Scoped composition of adapters, Z3, and independent checkers | Persistent native state and duplicated reduction semantics |
 | `python/oracles` | Independent solvers and checkers over pure models | Parsing, filesystem I/O, and reduction construction |
 | `python/formats` | Square solution validation and deterministic export | Native lifetimes, solving, and presentation |
-| `renderer/wang_square.py` | Structural presentation projection and square rasterization | Semantic verification and solver access |
+| `renderer/wang_hex_port.py` | Pure square-to-hex mapping, inverse checks, and matching-equivalence checks | Raster geometry, semantic verification, and solver access |
+| `renderer/wang_square.py` | Structural presentation projection and square/default or hex/explicit rasterization | Semantic verification and solver access |
 
 `include/wang/task_plan.h`, `src/parallel/solver_openmp.c`, and the two modules
 under `python/hex/` are placeholders. `src/io/json.c` is also a placeholder;
@@ -124,7 +125,12 @@ models. No ctypes pointer reaches those models or their consumers.
        immutable Python models       generic native solver
           /              \
          v                v
-   Python oracles    checkers / exporter --> square renderer
+   Python oracles    checkers / exporter --> Wang renderer
+                                             |       \
+                                             |        +--> pure hex port/check
+                                             v                    |
+                                       square PNG                 v
+                                                            hex PNG
 ```
 
 The formula adapter uses `cm13_formula_load_path(...)`, the path-based external
@@ -201,7 +207,15 @@ produces the closed square-only `wang-solution-v1` document. The
 [data contract]({{ '/wang-solution-v1/' | relative_url }}) is authoritative for
 schema, semantic validation, deterministic serialization, and metadata rules.
 
-The isolated square renderer consumes only that document. It projects the
-fields needed to choose pixels and produces a diagnostic PNG. Rendering is
-presentation, not proof, and cannot replace either semantic validation or the
-independent verifier. Hex translation and hex rendering are not implemented.
+The isolated Wang renderer consumes only that document. Its default path
+projects the fields needed for the existing square diagnostic PNG. Explicit
+`--hex` mode applies the pure in-memory
+[square-to-hex port]({{ '/wang-square-to-hex/' | relative_url }}), runs its
+raster-independent checker, and then composes a pointy-top axial PNG. The port
+preserves the square table, selected IDs, coordinates, holes, boundary, and
+matching truth values; it does not create a hex schema or core model.
+
+Rendering is presentation, not proof. The port checker establishes translation
+equivalence but deliberately does not require the source matching relations to
+be true, so neither raster path can replace semantic validation or the
+independent verifier.

docs/historical_architecture.md

@@ -31,13 +31,14 @@ than the early `vars`/`clause` sketch. The current public headers and tests are
 authoritative for behavior.
 
 The serial and optimized solvers are implemented and measured. The Python
-square solution contract, exporter, and presentation-only square renderer are
-also implemented. Native C JSON remains a placeholder, while `TaskPlan`, the
-native OpenMP solver, and square-to-hex translation remain future work.
+square solution contract, exporter, presentation-only square renderer, and
+checked square-to-hex presentation port are also implemented. Native C JSON,
+`TaskPlan`, and the native OpenMP solver remain future work.
 
 Current boundaries and status are documented in the
 [architecture page]({{ '/development_principles/' | relative_url }}), the
-[solution contract]({{ '/wang-solution-v1/' | relative_url }}), and the
+[solution contract]({{ '/wang-solution-v1/' | relative_url }}), the
+[square-to-hex reference]({{ '/wang-square-to-hex/' | relative_url }}), and the
 [solver optimization methodology]({{ '/solver_performance_scope/' | relative_url }}).
 
 ## Document metadata

docs/wang_solution_v1.md

@@ -134,11 +134,13 @@ the internal consistency of the serialized witness, but it is neither a solver
 nor the independent application verifier. The integration boundary must run
 the independent verifier before presenting a solution as correct.
 
-The renderer remains a presentation-only consumer. It must not import this
-formats module, replace the independent verifier, or decide correctness from a
-successful render. `load_wang_solution()` additionally rejects malformed JSON,
-duplicate object members, and non-finite numeric extensions accepted by some
-JSON parsers.
+The renderer remains a presentation-only consumer. Its explicit hex mode uses
+the same square document through the in-memory
+[square-to-hex port]({{ '/wang-square-to-hex/' | relative_url }}); it does not
+extend this schema. Neither raster mode may import this formats module, replace
+the independent verifier, or decide correctness from a successful render.
+`load_wang_solution()` additionally rejects malformed JSON, duplicate object
+members, and non-finite numeric extensions accepted by some JSON parsers.
 
 ## Metadata boundary
 

docs/wang_square_to_hex.md

@@ -0,0 +1,173 @@
+---
+layout: page
+title: Square-to-hex presentation port
+permalink: /wang-square-to-hex/
+description: Algebra, coordinate convention, inverse proof, and raster boundary for the verified presentation-only square-to-hex port.
+section: Architecture and correctness
+document_kind: Technical reference
+status: Current specification
+updated: 2026-08-26
+nav_order: 32
+---
+
+# Square-to-hex presentation port
+
+## Scope and attribution
+
+This port turns an already selected square Wang presentation into a pointy-top
+hexagonal presentation. It is not a solver, a second solution format, or a new
+core geometry. The input remains the square-only
+[Wang solution v1 contract]({{ '/wang-solution-v1/' | relative_url }}), and the
+hexagonal value exists only in renderer memory.
+
+Section 4 and Figure 13 of Sky Basire's 2022 report describe the construction
+principle: transfer the four square edge colors and give the two additional
+hexagon sides one common color. The report is available through its
+[institutional record](https://ir.canterbury.ac.nz/items/0f6603bb-28d2-4012-a1ec-06e0248d1c92),
+[DOI](https://doi.org/10.26021/14719), and
+[PDF](https://ir.canterbury.ac.nz/bitstreams/c69151f2-cf3b-4158-9f6b-b4e80013e440/download).
+Basire cites Karel Culik II's
+[*Small Aperiodic Sets of Triangular and Hexagonal Tiles*](https://link.springer.com/chapter/10.1007/978-3-642-60207-8_27)
+for the underlying square-tile simulation result.
+
+The exact edge tuple, coordinate convention, deterministic fresh-color rule,
+and finite-region bijection below are Tiling Foundry's formalization of that
+construction. They are not attributed to either source's diagram notation.
+
+## Project convention
+
+The source stores square edges as `(N,E,S,W)`. Its dense row-major coordinates
+increase to the east with `x` and to the south with `y`. The port uses
+pointy-top axial coordinates
+
+```text
+(q,r) = (x,y)
+```
+
+and stores hex edges clockwise as `(E,SE,SW,W,NW,NE)`. The corresponding axial
+neighbors are:
+
+| Hex side | Neighbor | Square relation |
+| --- | --- | --- |
+| `E` | `(q+1,r)` | `(x+1,y)`, square `E` |
+| `SE` | `(q,r+1)` | `(x,y+1)`, square `S` |
+| `SW` | `(q-1,r+1)` | additional axis |
+| `W` | `(q-1,r)` | `(x-1,y)`, square `W` |
+| `NW` | `(q,r-1)` | `(x,y-1)`, square `N` |
+| `NE` | `(q+1,r-1)` | additional axis |
+
+Let `C` be the finite set of all colors in the square tile table. The table is
+nonempty, so the renderer chooses the deterministic fresh color
+
+```text
+kappa = max(C) + 1.
+```
+
+Nonnegative integer colors are unbounded in the v1 contract. Therefore
+`kappa` is defined and is not in `C`. Each square tile maps as
+
+```text
+H(N,E,S,W) = (E,S,kappa,W,N,kappa)
+               E SE  SW    W NW  NE
+```
+
+Tile-table order is unchanged, so `tile_id` remains the positional index. The
+boundary tuple maps independently as
+
+```text
+B(N,E,S,W) = (E,S,null,W,N,null).
+```
+
+A null boundary entry for a hole remains null. No constraint is invented on
+the added axis; its tile edges are still both `kappa`.
+
+## Equivalence and inverse
+
+The map has a left inverse on its image:
+
+```text
+P(E,SE,SW,W,NW,NE) = (NW,E,SE,W).
+```
+
+For every square tile `t`, `P(H(t)) = t`. Thus `H` is injective, preserves the
+tile-table cardinality, and introduces no tile choice.
+
+Consider two active source positions. At `(x,y)` and `(x+1,y)`, square
+east/west matching is
+
+```text
+t(x,y).E = t(x+1,y).W.
+```
+
+Those positions become axial east/west neighbors, and `H` puts the same two
+colors on hex `E` and `W`. At `(x,y)` and `(x,y+1)`, square south/north
+matching becomes hex `SE/NW` matching for the same reason. Every active pair
+on the third axial direction compares `kappa` with `kappa`, so that axis adds a
+tautology and cannot remove a square witness.
+
+Conversely, take a valid hex tiling whose tile table is exactly the image of
+`H`. Project every tile with `P`. Hex `E/W` matching gives square `E/W`
+matching; hex `SE/NW` matching gives square `S/N` matching; the remaining axis
+contains no projected information. This recovers one and only one square
+tiling.
+
+The pointwise maps preserve inclusive coordinates, dense row-major indices,
+active cells, holes, boundary values, and selected tile IDs. They therefore
+form a bijection between square witnesses and witnesses over the image table
+on the corresponding axial region. Existence and nonexistence are preserved,
+as is the number of witnesses. The serialized v1 format is SAT-only, so an
+UNSAT result has no document or renderer invocation; UNSAT preservation is a
+property of the reduction, not a claimed JSON feature.
+
+## Independent port checker
+
+`renderer/wang_hex_port.py` contains the pure reducer and checker. It imports
+only the Python standard library. The checker does not call the reducer and
+does not use pixel coordinates. Before hex rasterization it checks:
+
+- exact coordinate, table, assignment, hole, and boundary preservation;
+- all six edges of every mapped tile and freshness of `kappa`;
+- the inverse projection for every positional tile ID;
+- equality of square and hex matching truth values on both meaningful axes;
+- `kappa/kappa` matching on every active pair along the additional axis;
+- equality of boundary-matching truth values after direction mapping.
+
+The truth-value comparison is deliberate. If a structurally present input has
+an invalid square adjacency, the corresponding hex adjacency remains invalid;
+the checker establishes translation equivalence without turning the renderer
+into another solution validator. Contract validation and the independent
+tiling verifier remain upstream obligations.
+
+## Raster boundary
+
+The existing `renderer/wang_square.py` command remains the only Wang renderer
+command. Without a geometry flag it follows the unchanged square path. With
+`--hex`, it reduces and checks the same in-memory presentation before composing
+hex pixels:
+
+```sh
+uv run --locked python wang_square.py \
+  ../tests/fixtures/wang_solution_v1_square_sat.json \
+  output/wang-hex.png \
+  --hex
+```
+
+For hex mode, `--pixels-per-cell s` is the integer axial raster radius. Centers
+use
+
+```text
+pixel_x = 2*s*q + s*r
+pixel_y = (s + floor(s/2))*r.
+```
+
+Integer vertices and a normalized bounding box make negative coordinates and
+pixel placement deterministic. The same injective palette is extended with
+`kappa`; because `kappa` is greater than every square color, existing logical
+colors retain their square RGB assignments. Holes use the neutral checkerboard
+inside the same pointy-top mask. The committed fixture golden is RGB 337×177
+at the default radius and margin.
+
+The raster consumes the checked result but proves nothing about SAT,
+adjacency, boundary validity, or solver behavior. It loads no native library or
+Z3 module, writes no intermediate hex serialization, and leaves the root
+`python/hex/` placeholders untouched.