Dev

AGENTS.md

@@ -63,7 +63,14 @@ presentation<multiform<value strata with outcome-as-observation, dyadic
 literals, mutual `=:` systems, self-contained equation-system display,
 word conditionals, Display v4, errors, the three-part conformance suite);
 implementation.md — the runtime architecture + resource-guard contract;
-README.md — the transcript-first tour. The
+README.md — the transcript-first tour;
+stance.md — non-normative (2026-07-19): the design tradition named —
+total/codata (Turner, Agda-kin), lazy exactly where the objects are
+coinductive, **⊥ refused** (divergence is a budgeted error, never a
+value); cyclic vs productive coinduction split (loopy graphs =
+eventually-periodic, 0.3.8 w/ Honsell–Lenisa; productive streams = 1.0.0
+higher-order, `ω` genetically needs a generator); Haskell the
+acknowledged cousin, not the semantics. The
 **ladder** — 0.3.7 structural rung → 0.3.8 loopy-envelope completion +
 release dress → 0.4.0 = the public release → 1.0.0 higher-order — lives
 in CONTINUATIONS.md;
@@ -77,7 +84,8 @@ and `writeups/`
 including the Tier-2 no-go/construction program; `excess.tex` — the
 consolidated note on the transfinite nim excess problem;
 `game_exterior_deformation.tex` — the checked game-generator Clifford deformation;
-`thermo_newton.tex` — the thermography ↔ Newton-polygon tropical bridge).
+`thermo_newton.tex` — the resolved thermography/Newton separation theorem: one
+filtered shadow, but no faithful dyadic-unital tropical ring).
 
 ## Claim levels and non-claims
 
@@ -262,13 +270,22 @@ realizer's *mechanism* is reduced (2026-06-10 second pass,
 `experiments/linking_game.py`, goldarf §8 `sec:linking`): the σ-game is the
 odd-close parity game on the support graph, and the linking theorem — an isolated
 coin forces flips even, hence exactness for all m — is machine-verified on every
-graph class k ≤ 7 with a strictly-verified two-mode defender strategy; only the
-general-n induction is open.
+graph class through k = 8 real coins plus dummy (12,346 classes at k = 8, both
+seats). The original prevention/debt menu is strictly complete only through k = 7;
+two k = 8 witnesses require proactive debt, while the broader no-self-flip/debt
+envelope is strictly complete across the full k = 8 census. The block-turn and
+live-degree identities sharpen the proof route; the general-n induction remains
+open.
 
 Appendix-grade shipped layers that should not be mistaken for new Gold/Arf claims:
 tropical thermography (`Semiring` + dual `Tropical<MaxPlus/MinPlus>`) plus
-game-valued heating/overheating/Norton operators (infrastructure for `under`, not
-the associated-graded product theorem), the source-pinned (OEIS A380496) ordinal
+game-valued heating/overheating/Norton operators and the proved positive-numeric-unit
+regrading `gr_τ -> gr_{uτ+u-δ}`. The completed `under` theorem proves that the
+game and place consumers are two tropical objects: `gr_0`'s nonzero `[*]`
+2-torsion forbids a lift-compatible action by any full dyadic object
+(ordinary or graded initial-form), and the exact nonnegative
+Norton composition defect forbids a multiplicative dyadic action even after
+any temperature-preserving residue refinement. The source-pinned (OEIS A380496) ordinal
 nim Kummer tower below `ω^(ω^ω)`, the characteristic-2
 Artin-Schreier local-global layer over `F_{2^m}(t)` including the Aravire-Jacob wild
 summand, and the integral lattice/genus/mass/Leech/Niemeier/theta/code/Weil chain. These are

CONTRIBUTING.md

@@ -68,11 +68,11 @@ asserted.
 ## Releasing
 
 The version in `Cargo.toml` is the single source of truth (pyproject and the
-maturin build inherit it). The release workflow is **dormant** while the version is
-`0.0.0`; bumping it arms the pipeline, which on the next push to `main` publishes to
-crates.io and PyPI (both via OIDC trusted publishing), tags `vX.Y.Z`, and cuts a
-GitHub release. Each target is checked independently, so a partial-failure run
-resumes cleanly.
+maturin build inherit it). On a push to `main` carrying a new version, the release
+workflow publishes to crates.io and PyPI (both via OIDC trusted publishing), tags
+`vX.Y.Z`, and cuts a GitHub release. Each target is checked independently, so a
+partial-failure run resumes cleanly. The unpublished `grundy/` workspace member
+(`publish = false`) is deliberately outside the pipeline.
 
 ## License
 

Cargo.toml

@@ -3,7 +3,7 @@ members = ["grundy"]
 
 [package]
 name = "ogdoad"
-version = "1.0.0"
+version = "1.0.1"
 edition = "2021"
 description = "Clifford algebras (with nilpotents) over the field-like subclasses of combinatorial games: nimbers, surreals, surcomplex."
 license = "AGPL-3.0-or-later"

README.md

@@ -6,21 +6,23 @@
 [![docs.rs](https://img.shields.io/docsrs/ogdoad)](https://docs.rs/ogdoad)
 [![License: AGPL v3](https://img.shields.io/badge/License-AGPL_v3-blue.svg)](https://www.gnu.org/licenses/agpl-3.0)
 
-The **Ogdoad** were eight Egyptian gods of the primordial waters, arranged in four
-pairs — the world before there was a world. This `ogdoad` keeps a smaller pantheon:
-eight number-systems, also in four pairs, also a little primordial. Surreals and
-omnific integers; p-adics and Witt vectors; rational functions and polynomials; and
-the plain old rationals and integers. Each pair is a **field beside its ring of
-integers**. Off to one side sit the finite fields and the nimbers, who are their own
-rings of integers and answer to no one. Eight, plus the loners.
-
-The conceit is that these exotic worlds are not a curiosity cabinet. They are **cells
-of one table**, and the number eight is not an accident: read the table one way and
-you get Clifford algebras, read it the other way and you get the classification of
-quadratic forms, and the *same* structures keep surfacing cell after cell with the
-characteristic and the place politely swapped. The eightfold periodicity of the real
-Clifford table, `BW(ℝ) ≅ ℤ/8`, Bott, `E₈` — it is all one spine, and the code is laid
-out to make the rhyming visible.
+Clifford algebras — **with nilpotents**: the quadratic form may be degenerate
+(`q[i] = 0` ⇒ `eᵢ² = 0`; all-zero `q` is the exterior algebra) — over the
+commutative scalar worlds adjacent to Conway's combinatorial games. A pure Rust
+engine, generic over a `Scalar` trait, whose backends are the nimbers, the
+surreals and surcomplex numbers, and a bench of comparison worlds: p-adics and
+Witt vectors, Laurent series, finite fields, the exact global function field
+`F_q(t)`, and the plain rationals and integers. On top sit a quadratic-forms
+classification layer across the characteristic trichotomy, an integral-lattice
+wing, a combinatorial-games pillar, and per-backend Python bindings.
+
+The claim behind the collection is that these worlds are not a curiosity
+cabinet. They are **cells of one table**: read the table one way and you get
+Clifford algebras, read it the other way and you get the classification of
+quadratic forms, and the *same* structures keep surfacing cell after cell with
+the characteristic and the place politely swapped. The eightfold periodicity of
+the real Clifford table, `BW(ℝ) ≅ ℤ/8`, Bott, `E₈` — it is all one spine, and
+the code is laid out to make the rhyming visible.
 
 One honest caveat up front, because it shaped everything. Conway's games, under
 disjunctive sum, form an abelian **group but not a ring**: you can add games freely,
@@ -40,7 +42,7 @@ Every backend is a cell in a table with two axes:
   is how `src/forms/` is grouped.
 
 The axes are independent. The place axis is what pairs each **field** with its **ring
-of integers** — the four pairs of the Ogdoad:
+of integers** — four such pairs, plus the finite worlds that are their own:
 
 | | field | ring of integers |
 | --- | --- | --- |
@@ -291,27 +293,70 @@ one place a traveller may wander in circles.
 
 Closing the tour now wants a *third* Scalar–Clifford span — bridges C and D are the two
 it already has. None of the pending threads supplies one: **`*2` (S–I)**, the
-Drinfeld/Carlitz mirror, would even Scalar but tip the Integral wing odd in turn; `*1`
-(the spinor genus), `*4` (the wild local symbol), and `under` (a constructive
-thermography ↔ Newton-polygon bridge) each matter on their own terms but land elsewhere
-on the map. The round trip stays open — and the obstruction has simply walked from the
-Integral shore to the Clifford one.
-
-## The research thread
-
-The narrow mathematical thread in `docs/OPEN.md` and `writeups/goldarf.tex` is *not* a
-claim of a new Clifford classification theorem. It is an investigation of game-built
-quadratic forms in the nimber backend:
+Drinfeld/Carlitz mirror, would even Scalar but tip the Integral wing odd in turn;
+`*1` (the spinor genus) and `*4` (the wild local symbol) matter on their own terms
+but land elsewhere. `under` is closed rather than pending: the game filtration has
+genuine numeric filtered transports, but its `[*]` 2-torsion and the exact Norton
+composition defect prove that it cannot carry the place axis's full dyadic
+coefficient object, even in graded initial-form form. It likewise lands elsewhere
+on the map. The round trip stays open —
+and the obstruction has simply walked from the Integral shore to the Clifford one.
+
+## The research threads
+
+The genuine open problems live in `docs/OPEN.md`, each named by a **loopy game
+value** — an open problem is a game played without a termination guarantee. The
+flagship, `tis`, is *not* a claim of a new Clifford classification theorem. It is
+an investigation of game-built quadratic forms in the nimber backend:
 
 1. Turning-Corners games realize nim multiplication.
 2. Frobenius squaring and traces are built from nim multiplication and XOR.
 3. Gold-style trace forms `Tr(λ · x^{1+2^a})` are therefore expressible from game-value
    operations.
 4. The Arf invariant gives the standard zero-count bias for a quadratic zero set.
 5. **The open question:** is there a natural, non-tautological game rule whose
-   P-positions are exactly such a zero set? Current probes span normal play, misère
-   quotient, interactive (`kernel`), loopy (Draw-set), and bent-form searches; they
-   narrow the target but do not hit it.
+   P-positions are exactly such a zero set?
+
+The current frontier (`writeups/goldarf.tex`): the linear case is both floor and
+ceiling — lexicodes show natural rules realize rich *linear* codes as P-sets,
+and Theorem A shows every Winning Ways coin-turning P-set is the kernel of an
+`F₂`-linear map — so `tis` asks precisely whether that phenomenon admits a
+quadratic refinement. A no-go ladder kills the frame-blind tier (`Sp(B)`-invariant
+rules see only orbit unions) and shows the known normal-play realizers are
+clocks. The one verified positive object is **σ-valued**: the echo-fifo+dummy
+realizer computes `Q` as a forced terminal charge, checked exhaustively at
+`m = 8` (391,680/391,680, adversarial review), and its mechanism reduces to an
+**odd-close parity game** whose isolated-coin linking theorem is machine-verified
+on all 12,346 graph classes through `k = 8`. The two load-bearing open steps:
+recast that charge readout into normal/misère/loopy outcome semantics, and prove
+the general-`m` linking theorem.
+
+The rest of the board, briefly:
+
+- **`tisn`** — a game-native quadratic deformation of the game exterior algebra.
+  The torsion obstruction is now a theorem (integer-valued deformations are blind
+  to torsion: `2* = 0` forces `Q(*)` and all pairings with `*` to zero), and the
+  surviving escapes are tautological or off-core; what is missing is a
+  **directed/noncommutative** coefficient source whose squaring remembers the
+  first-/second-player asymmetry — the same obstruction `tis` hit in misère form.
+- **`on`** — transfinite nim multiplication beyond the verified excess table.
+  Conway's Kummer carry below `ω^(ω^ω)` is `α_p = κ_{f(p)} + m_p` with `m_p`
+  Lenstra's finite excess; every source-pinned row obeys an unproved `0/1/4`
+  rule, and `writeups/excess.tex` reduces that rule *exactly* to four universal
+  order statements — the zero, ordinary-odd-spine, cubic, and exceptional arms.
+  The next unsupported carry is `α₇₁₉`.
+- **`off`** — what, if anything, replaces the finite Arf/Brauer–Wall bit for
+  Clifford metrics with genuinely transfinite ordinal-nimber coefficients, where
+  no finite trace to `F₂` exists.
+- **`over`** — whether the Brown `ℤ/8` invariant has a game reading the way the
+  Arf bit does: a natural *four*-class outcome census whose Gauss-sum phase is
+  `ζ₈^β`, lifting the two-class win-bias from `ℤ/2` to `ℤ/8`.
+- **`under`** — *resolved 2026-07-20*: thermography and the Newton-polygon stack
+  are **two** tropical objects. Temperature is an honest tropical valuation and
+  every positive dyadic Norton unit `u = m/2^k` transports the temperature
+  filtration exactly (`gr_τ → gr_{uτ+u−δ}`), but `gr₀`'s `[*]` 2-torsion and the
+  exact Norton composition defect forbid any faithful dyadic-unital graded ring
+  (`writeups/thermo_newton.tex`).
 
 If you want to play along, the open-problem examples (`interactive_kernel`, `octal_hunt`,
 `loopy_quadric`, `misere_quotient`, `bent_route`) are the doors in.

demo.py

@@ -580,6 +580,16 @@ def same_thermograph(a, b):
 norton = hot.norton_multiply(pl.Game.integer(2))
 print("  heat by 2 / Norton by 2    :", heated.temperature(), heated.mean_value(),
       norton.mean_value(), norton.canonical_string())
+u = pl.Game.integer(2)
+scale, shift = u.numeric_norton_regrade()
+pred_mean, pred_temp = hot.numeric_norton_mean_temperature(u)
+print("  numeric Norton descent u=2 :", f"regrade (scale,shift)=({scale},{shift})",
+      f" predicted (mean,temp)=({pred_mean},{pred_temp})",
+      " matches product:", (str(pred_mean), str(pred_temp)) ==
+      (str(norton.mean_value()), str(norton.temperature())))
+over = hot.overheat(u, pl.Game.integer(1))
+print("  overheat ∫_2^1 = Norton·2  :", over == norton,
+      " temp:", over.temperature())
 
 section("surreal sign-expansion & floor (the omnific bridge)")
 print("  sign expansion of 3/4    :", pl.Surreal.from_rational(3, 4).sign_expansion(), " (+ − +)")

docs/CONSISTENCY.md

@@ -75,9 +75,46 @@ Recorded so the next auditor inherits the truth, not the first read:
   `smallest_prime_factor` is a different shape — early-exit smallest factor, not a
   factor list).
 
+## Recorded 2026-07-30 — the polynomial altitude question (discussion, not audit)
+
+Prompted by "should polynomials be exposed publicly / unified into a pillar?"
+Answered in discussion and recorded here so it isn't re-litigated:
+
+- **No polynomial pillar, no preemptive public factorization.** Pillars are
+  domains, not representations; `Poly` is already public at its correct altitude
+  (a place-table row — `F_q[t]` beside `F_q(t)` — with `Scalar` +
+  `HasFractionField`, py bindings, and the grundy `fp2[t]`/`fp2(t)` worlds). The
+  one private polynomial *capability* is `forms/poly_factor.rs`, and 1.0.0 makes
+  every export a semver commitment. The trigger for exposing it: the first
+  consumer that can't reach `pub(crate)` — realistically the Python experiments
+  tier or a grundy `factor` word (nothing on the 0.3.7/0.3.8 ladder demands one).
+  When it fires, export the small honest surface (monic irreducible support),
+  keep the Cantor–Zassenhaus internals private.
+- **The pillar line, named**: operations *valued in* `Poly` (divrem, gcd,
+  factor) are ring arithmetic → `scalar/`; structures *indexed by places*
+  (residue forms, Hilbert symbols, reciprocity) → `forms/`. This sharpens
+  scalar/AGENTS.md's "per-place residues live at the forms layer" without
+  contradicting it: factorization takes a polynomial and returns polynomials, so
+  it sits on the scalar side, and its current `forms/` home is consumer-driven
+  placement (three call sites: the char-2 façade plus the two
+  `local_global/function_field*` layers).
+- **`Fpn`'s `[u128; N]` arithmetic is NOT latent `Poly` duplication** — the same
+  refusal as `cnf.rs` (shared function, not shared type): quotient-ring elements
+  with `Copy` and a static modulus on the hot finite-field path vs free-ring
+  `Vec` elements. Folding them buys allocation in `F_{p^N}` mul and a false
+  identity. A cleanup pass that "unifies" these destroys a deliberate boundary.
+- **`divrem`'s panic contract is fine until grundy consumes it.** The field-base
+  assumption is documented where it lives; the crate pattern once the language
+  becomes a consumer is a checked sibling (`Integer::div_exact` precedent).
+  Recorded, not pre-built.
+
 ## ups — still open (worth less than any number, strictly positive)
 
 - **↑·(e_s∧e_i): `ordinal-factor-fold`** — the two ordinal-local helpers above.
+- **↑·(e_s∧e_f): `poly-factor-altitude`** — move `forms/poly_factor.rs` beside
+  `scalar/poly.rs` per the pillar line above; three call sites, stays
+  `pub(crate)`. Rides with the next structural pass, not worth a dedicated
+  commit.
 - **`display-policy` — PLAYED 2026-07-02.** a9 made it policy: **every classifier
   report renders.** All 34 remaining glossary record types (the suffix net over
   `…Invariants`/`…Decomp`/`…Class`/`…Record`/`…Isotropy`/certificates plus

docs/CONTINUATIONS.md

@@ -86,7 +86,12 @@ reversal (transcript-first), `examples/grundy/*.og` gallery, the writeup
 argument, the honest CGSuite comparison), corpus split thematically +
 `stage_*` tests renamed by law; **name finalization** (the 2026-07-15
 ogham→grundy rename is provisional — confirm the name and the crate-slot
-question). Final full-surface pass gates the release.
+question). Theory citation for the loopy envelope: Honsell–Lenisa 2011
+(loopy Conway games as a final coalgebra) — the stance note
+(`grundy/docs/stance.md`, 2026-07-19) pins the data/codata reading of the
+shipped constructs; whether spec §1 states the coalgebraic identity out
+loud is a release-dress decision beside name finalization. Final
+full-surface pass gates the release.
 
 ### `grundy-0.4.0` — **the public release** (after 0.3.8's gate; not a
 feature rung). Package/version alignment, publish decision execution.
@@ -99,7 +104,13 @@ earns it through **one symmetric map/fold story over the three container
 shapes** (fixed/graded/free — the 0.3.6 container totality made this a
 three-world question, a better one than the two-world sketch). Mutual
 *function* `=:` groups land here (Function representation changes anyway;
-Element systems shipped at 0.3.6). Whatever the release soak surfaces
+Element systems shipped at 0.3.6). **Productive streams** are the codata
+face of this rung (`grundy/docs/stance.md`): `ω = {0, 1, 2, … |}`
+genetically has a non-periodic option stream — no finite cyclic
+presentation exists — so a generator is a function, and lazy transfinites
+arrive with higher-order rather than as a separate tack; the
+Escardó–Oliva selection monad is the strategy-shaped star to steer by.
+Whatever the release soak surfaces
 joins the docket. Value proposed at `4·e_o`; a9 to re-value.
 
 ---