Dev

.github/ISSUE_TEMPLATE/bug_report.yml

@@ -69,7 +69,7 @@ body:
     attributes:
       label: ogdoad version
       description: "`cargo pkgid` (Rust) or `pip show ogdoad` (Python), or the commit SHA."
-      placeholder: 1.0.2
+      placeholder: version or commit SHA
     validations:
       required: true
 

.github/ISSUE_TEMPLATE/config.yml

@@ -2,7 +2,7 @@ blank_issues_enabled: false
 contact_links:
   - name: Open research problems
     url: https://github.com/a9lim/ogdoad/blob/main/docs/OPEN.md
-    about: Arbitrary-graph FIFO linking and the universal transfinite nim-excess rule are known open problems, not bugs. See docs/OPEN.md before filing.
+    about: FIFO linking, transfinite nim-excess, and natural finite-misere realization are research problems, not bugs. See docs/OPEN.md before filing.
   - name: Security vulnerability
     url: https://github.com/a9lim/ogdoad/security/policy
     about: Please report security issues privately (see SECURITY.md).

.github/ISSUE_TEMPLATE/feature_request.yml

@@ -12,9 +12,11 @@ body:
           Clifford algebra needs a commutative scalar *ring*, and the full game
           group is only an abelian group. New scalar worlds must be commutative
           rings.
-        - The genuine open problems (arbitrary-graph FIFO linking and the
-          universal transfinite nim-excess rule) live in `docs/OPEN.md`. Those are research
-          questions, not feature requests — open a discussion instead.
+        - The open mathematical fronts (arbitrary-graph isolated-dummy FIFO
+          linking, the universal transfinite nim-excess `0/1/4` rule, and
+          natural-ruleset realization of finite misere quotients) live in
+          `docs/OPEN.md`. Those are research questions, not feature requests —
+          open a discussion instead.
 
         New backends, invariants, cross-pillar bridges, and binding/docs
         ergonomics are all in scope and welcome.

.github/PULL_REQUEST_TEMPLATE.md

@@ -8,22 +8,21 @@
 
 ## Test plan
 
-- [ ] `cargo test` passes
-- [ ] `cargo clippy --all-targets` is warning-clean
-- [ ] `cargo fmt --check` is clean
-- [ ] If this touched `src/py/` or any core API the bindings call: `cargo check --features python` **and** `cargo clippy --features python --all-targets`
-- [ ] If this touched `clifford/` or `scalar/big/surreal/`: rebuilt (`maturin develop`) and ran `demo.py` — Display changes don't surface in `cargo test`
-- [ ] If this touched any doc comment (`//!` / `///`): ran `cargo doc --no-deps` **cold** (`RUSTDOCFLAGS="-D warnings"`) and it's link-clean
-- [ ] If this added a new operation: there's a test pinning it to an independent oracle (the `associativity_*` / `general_product_reproduces_*` style)
+- [ ] `cargo fmt --all --check`
+- [ ] `cargo test --workspace`
+- [ ] `cargo clippy --workspace --all-targets -- -D warnings`
+- [ ] `RUSTDOCFLAGS="-D warnings" cargo doc --no-deps --workspace`
+- [ ] If this touched `src/py/` or a core API used by Python: `cargo check -p ogdoad --features python`, the matching Clippy gate, and `python scripts/generate_stubs.py --check`
+- [ ] If this touched Lean or a load-bearing proof claim: `(cd formal && lake build --wfail)`
+- [ ] If this touched a paper or bibliography: `npm ci` and `python scripts/check_writeups.py`
+- [ ] If this added a generic operation: a focused test pins it to an independent oracle
 
 ## Claim level
 
 <!-- If this changes prose / comments / examples, label the claims per AGENTS.md:
-     standard math · implemented and tested · interpretation · open. New "X is
-     true" math statements should be backed by a test or cited, not asserted. -->
+     standard/cited · implemented and tested · proved here · open. -->
 
 ## Notes
 
-<!-- Anything reviewers should know. If this touches the metric/product, confirm
-     q and b stay independent and signs go through the scalar's neg() — the two
-     load-bearing char-2 invariants (see Hard rules in AGENTS.md). -->
+<!-- Anything reviewers should know. For metric/product changes, confirm that q,
+     b, and optional a stay distinct and generic signs use Scalar::neg. -->

.github/workflows/release.yml

@@ -14,12 +14,9 @@ permissions:
   contents: read
 
 jobs:
-  # The gate. Reads the version from Cargo.toml (the source of truth — pyproject
-  # and the maturin build inherit it) and decides whether there is anything to
-  # ship. The pipeline is DORMANT while the version is the 0.0.0 placeholder;
-  # bumping the version is what arms it. Each publish target is also probed
-  # independently so a partial-failure run resumes cleanly: a step is skipped
-  # only when its own artifact already exists, never gated on a sibling.
+  # The gate. Cargo.toml is the version source of truth; pyproject and maturin
+  # inherit it. Each publish target is probed independently so a partial-failure
+  # run can resume without republishing a completed sibling artifact.
   guard:
     runs-on: ubuntu-latest
     outputs:
@@ -43,12 +40,8 @@ jobs:
           VERSION: ${{ steps.v.outputs.version }}
           GH_TOKEN: ${{ github.token }}
         run: |
-          # Dormant until the version is bumped off the 0.0.0 placeholder; after
-          # that, the git tag is the completion marker — an existing tag means a
-          # version was fully shipped and there is nothing to do.
-          if [ "$VERSION" = "0.0.0" ]; then
-            echo "should_release=false" >> "$GITHUB_OUTPUT"
-          elif git rev-parse -q --verify "refs/tags/v$VERSION" >/dev/null; then
+          # The git tag is the completion marker for the current version.
+          if git rev-parse -q --verify "refs/tags/v$VERSION" >/dev/null; then
             echo "should_release=false" >> "$GITHUB_OUTPUT"
           else
             echo "should_release=true" >> "$GITHUB_OUTPUT"

AGENTS.md

@@ -41,8 +41,9 @@ crate-private. Their public modules re-export children shallowly.
   build.
 - `grundy/` is an unpublished workspace crate depending only on Ogdoad's public
   API.
-- `formal/` is a separately pinned Lean project. It proves named ingredients;
-  paper-level syntheses must state what Lean does and does not check.
+- `formal/` is a separately pinned Lean project. It proves named components
+  and selected end-to-end finite constructions; paper-level syntheses must
+  state what Lean does and does not check.
 
 ## Non-negotiable mathematical invariants
 
@@ -85,10 +86,6 @@ The current open fronts are exactly:
 - arbitrary-graph isolated-dummy FIFO linking;
 - the universal `0/1/4` transfinite nim-excess rule, including its selected
   nim-reciprocity program;
-- quasi-linear multiplication in canonical finite-nimber coordinates;
-- game-valued Witt realization over `F_2(t)`;
-- stable quadratic-form invariants over the supertropical and Hessenberg
-  semirings;
 - natural-ruleset realization of finite misère quotients, including the exact
   quotient of misère Grundy's game.
 
@@ -97,6 +94,9 @@ matching-plus-isolates theorem and does not depend on general FIFO linking.
 The full `On_2` classification is a mathematical theorem after scalar
 extension; it does not make the finite `Nimber(u128)` backend algebraically
 closed or make the partial `Ordinal` backend construct every root.
+Quasi-linear multiplication in canonical finite-nimber coordinates has an
+explicit proved transform; its arbitrary-width implementation and crossover
+measurement are engineering work in `docs/ROADMAP.md`.
 
 ## Code conventions
 

Cargo.toml

@@ -3,7 +3,7 @@ members = ["grundy"]
 
 [package]
 name = "ogdoad"
-version = "1.0.5"
+version = "1.0.6"
 edition = "2021"
 description = "Clifford algebras and quadratic forms over exact, finite, local, transfinite, and game-adjacent scalar backends."
 license = "AGPL-3.0-or-later"

README.md

@@ -50,7 +50,7 @@ Representation limits are part of the API:
 | --- | --- |
 | `src/scalar/` | coefficient traits and exact, finite, valued, global, surreal, and ordinal backends |
 | `src/clifford/` | metrics, blades, multivectors, products, versors, spinors, and geometric-algebra constructions |
-| `src/forms/` | quadratic-form classification, Witt/Brauer theory, Springer and local--global arithmetic |
+| `src/forms/` | quadratic-form classification, Clifford centers, Witt/Brauer and low Milnor-symbol theory, Springer and local--global arithmetic |
 | `src/forms/integral/` | lattices, discriminant forms, codes, theta series, genera, neighbors, and Weyl bridges |
 | `src/games/` | impartial, partizan, misere, loopy, thermographic, Witt--FIFO/Brown, octal-certificate, Hackenbush, and game-exterior constructions |
 | `src/py/` | optional per-backend PyO3 bindings; scalar worlds never mix at runtime |
@@ -91,6 +91,12 @@ assert e0 * e1 + e1 * e0 == A.scalar(og.Nimber(1))
 S = og.SurrealAlgebra(q=[og.omega(), og.epsilon()])
 assert (S.gen(0) * S.gen(1)) ** 2 == S.scalar(og.Surreal.from_int(-1))
 
+# A Hermitian form restricts to the ordinary quadratic form q(v)=h(v,v)
+# over the involution-fixed field; dimension doubles.
+H = og.HermitianForm.diagonal([1, -1])
+Q = H.restrict_scalars()
+assert Q.dim == 4 and og.surreal_signature(Q) == (2, 2, 0)
+
 # Checked game constructors preserve their proof and validation boundaries.
 arena = og.WittFifoArena(diagonal=[True], polar=[0], input=1)
 assert arena.quadratic_value and arena.grundy(state_budget=100_000) != 0
@@ -108,9 +114,12 @@ The Python layer monomorphizes a documented slice of the Rust backends. It
 does not provide a runtime-tagged any-scalar algebra. Its typed report surface
 includes finite quadratic modules and Nikulin criteria, extraspecial and
 Heisenberg--Weil objects, function-field Brauer--Wall classes, Niemeier data,
-finite-field Witt decompositions, lexicode turning games, conformal-algebra
-accessors, represented ordinal finite-subfield degrees, checked Witt--FIFO and
-Brown constructors, and sealed Guy--Smith periodicity certificates. Python
+finite-field Witt decompositions and numeric-invariant reports,
+characteristic-two additive spinor norms and symmetry certificates, lexicode
+turning games, conformal-algebra accessors, represented ordinal finite-subfield
+degrees, checked Witt--FIFO and Brown constructors, Hermitian restriction to
+typed ordinary quadratic backends, and sealed Guy--Smith periodicity
+certificates. Python
 `repr` delegates to canonical Rust rendering where the core provides it.
 
 ## Mathematical status
@@ -121,14 +130,19 @@ The papers under `writeups/` form one current research suite:
 | --- | --- |
 | `transfinite_arf.tex` | classification over perfect Artin--Schreier-surjective characteristic-two fields and its full-nimber specialization |
 | `goldarf.tex` | quadratic-refinement realization in normal play, Gold specialization, Brown selector, and game-exterior obstruction |
+| `witt_realization.tex` | quadratic Witt coordinates over `F_2(t)`, finite impartial realization, explicit ramified naturality, and finite-static and singular no-go theorems |
 | `thermo_newton.tex` | thermic regrading under Norton multiplication and its separation from Newton tropicalization |
+| `semiring_stability.tex` | stable quadratic-pair classification over Hessenberg and supertropical semirings, the universal scalar-extension quotient, and the thermograph wall obstruction |
 | `linking_affine.tex` | proved reductions and exact remaining obstruction for isolated-dummy FIFO linking |
-| `excess.tex` | four-arm reduction and exact remaining selected-order problem for transfinite nim excess |
-
-The last two universal claims remain open. Their concise statements and sharp
-proof boundaries are in [`docs/OPEN.md`](docs/OPEN.md). Lean checks named
-ingredients and several end-to-end finite constructions, not the open
-propositions; see [`formal/README.md`](formal/README.md).
+| `excess.tex` | exact four-arm selected-order reduction, proved arithmetic boundaries, and authoritative open status of the transfinite nim-excess `0/1/4` rule |
+| `nim_fast_multiplication.tex` | quasi-linear canonical-word multiplication via explicit affine transforms to a primitive Artin--Schreier tower |
+| `misere_natural_realization.tex` | exact octal trace calculus, finite-exception heap normal form, realization of every tame finite quotient, and exact misere Grundy quotients through heap 18 |
+
+The unresolved universal claims and their sharp proof boundaries are in
+[`docs/OPEN.md`](docs/OPEN.md). Lean checks named algebraic components and
+end-to-end finite constructions including the literal Gold--Arf root; cited
+bridges and the open propositions remain outside that boundary. See
+[`formal/README.md`](formal/README.md) for the theorem map.
 
 ## Verification
 

demo.py

@@ -140,6 +140,10 @@ def cl(qs):
 print("  WittClass metric constructor:", pl.WittClass.try_from_metric(A) == wA)
 print("  Dickson(swap)  =", pl.dickson_matrix([[0, 1], [1, 0]]), " (a reflection)")
 print("  Dickson(diag *2,*3 rotation) =", pl.dickson_matrix([[2, 0], [0, 3]]), " (in SO)")
+char2_factor = pl.factor_char2_isometry([0, 0], {(0, 1): 1}, [[0, 1], [1, 0]])
+print("  certified F2 symmetry factor:", char2_factor.factors,
+      "spinor", pl.char2_spinor_norm([0, 0], {(0, 1): 1}, [[0, 1], [1, 0]]),
+      "Clifford checked", char2_factor.clifford_verified)
 
 section("exterior algebra of the GAME group — lives where Clifford can't")
 # Λ needs only a ℤ-module; the game group is one, even for non-numbers (⋆, ↑).
@@ -257,8 +261,8 @@ def cl(qs):
 print("  ω < ω²       :", omega < pl.Ordinal.omega_pow(pl.Ordinal(2)))
 print("  ω fuzzy ω² (as nimbers):", omega.fuzzy(pl.Ordinal.omega_pow(pl.Ordinal(2))))
 print("  2 ⊗ 2 = *3   :", pl.Ordinal(2).nim_mul(pl.Ordinal(2)))
-# nim-multiplication: implemented below ω^ω via the current DiMuro/Conway
-# degree-3 tower. The old φ_{ω+1} (<ω³) case is the first layer.
+# nim-multiplication: implemented below ω^ω via the DiMuro/Conway
+# degree-3 tower. The φ_{ω+1} (<ω³) cell is its first layer.
 print("  ω ⊗ ω        =", omega.nim_mul(omega), "  (just polynomial mult)")
 omega_sq = omega.nim_mul(omega)
 print("  ω ⊗ ω ⊗ ω    =", omega_sq.nim_mul(omega), "  (the headline: ω³ = 2)")
@@ -405,10 +409,11 @@ def _matmul(a, b):
 print(f"  ⟨1,2,3⟩/F5: e0={stair.e0} (dim) e1={stair.e1} (disc) e2={stair.e2:+} (Hasse), I^{stair.stabilizes_at}=0")
 # Over ℝ the tower is infinite: eₙ reads the 2-adic expansion of the signature.
 print("  ⟨1,1,1,1⟩/ℝ (sig 4): eₙ for n=0..3 =", [pl.e_real(4, n) for n in range(4)])
-print("  numeric invariants of F5:",
-      "level", pl.level(5),
-      "pythagoras", pl.pythagoras_number(5),
-      "u", pl.u_invariant(5))
+finite_numeric = pl.finite_field_numeric_invariants(3, 2)
+print("  numeric invariants of F9:", finite_numeric,
+      "level", pl.level(3, 2),
+      "pythagoras", pl.pythagoras_number(3, 2),
+      "u", pl.u_invariant(3, 2))
 print("  WittClassG constructors:",
       pl.WittClassG.char0(3, 1), pl.WittClassG.oddchar_one(5, 0) * pl.WittClassG.oddchar_zero(5, 0),
       pl.WittClassG.char2(1).arf())
@@ -425,10 +430,21 @@ def _matmul(a, b):
 H = pl.HermitianForm.from_gram([[pl.Surcomplex(2, 0), pl.Surcomplex(0, 1)],
                                 [pl.Surcomplex(0, -1), pl.Surcomplex(2, 0)]])
 print("  Hermitian [[2,i],[-i,2]]:", H.signature(), "diagonal", H.diagonalize())
+restricted_H = pl.HermitianForm.diagonal([1, -1, 0]).restrict_scalars()
+print("  restriction to ordinary No-form:", restricted_H.dim,
+      pl.surreal_signature(restricted_H))
 print("  diagonal Hermitian ⟨1,-1,0⟩:", pl.HermitianForm.diagonal([1, -1, 0]).signature())
-finite_H = pl.FiniteHermitianForm.diagonal(3, 2, [1, 1, 0]).classify()
+finite_H_form = pl.FiniteHermitianForm.diagonal(3, 2, [1, 1, 0])
+finite_H = finite_H_form.classify()
 print("  finite Hermitian F9/F3       :", (finite_H.rank, finite_H.radical_dim,
                                            finite_H.base_field_order, finite_H.extension_field_order))
+finite_restriction = finite_H_form.restrict_scalars()
+print("  F9/F3 ordinary restriction   :", finite_restriction.dim,
+      pl.classify_finite_algebra(finite_restriction))
+char2_restriction = pl.FiniteHermitianForm.diagonal(2, 4, [1]).restrict_scalars()
+char2_restriction_class = pl.classify_finite_algebra(char2_restriction)
+print("  F16/F4 norm restriction      :", char2_restriction.dim, char2_restriction_class)
+assert char2_restriction_class.arf == 1 and char2_restriction_class.rank == 2
 print("  form Rust constructors       :",
       pl.SymplecticForm.from_gram([[0, 1], [-1, 0]]).classify().planes(),
       (lambda sig: (sig.pos, sig.neg, sig.radical))(