Exact finite coefficient data accompanying:
On the local geometry of the tight 39-point code in the octonionic projective plane
Robert R. MacGregor, November 2026

Source: https://github.com/macgregor-sudo/tight-39-code
Revision: 46f01c135aacea9003435e7f1dc99b4a69568e83
The first-party coefficient definitions were transcribed into native-data.json.
Their original source package is offered under Apache License 2.0 to the extent
of rights held or authorized. LICENSE.txt reproduces that license. This notice
does not relicense third-party material or assert exclusive copyright in
AI-generated output. The source file hashes are recorded in the JSON provenance.
Within this deposit the file is distributed under the licence of the deposit.

The mathematical decoding is given in Appendix C of the paper. The data include
1280 H entries, 2988 Laurent T entries, 576 real-operator entries and 4248 seed
column entries. All indices are zero-based. The exact coefficient, orientation,
row and native-coordinate conventions are explicit in the paper and the data.
The explanatory strings inside native-data.json keep the letter names of the
source repository; Appendix C of the paper gives the dictionary to its notation.

The export was checked against the pinned source definitions and decoded row
labels. The formal verification of the identities belongs to the registered
source.

finite-identities.py (Python 3, standard library only) replays the finite
identities of the paper (the proposition "Finite identities" and Appendix C)
from native-data.json in exact arithmetic, for all parameters at once:
    python3 finite-identities.py native-data.json
It was written for this paper and is distributed under the licence of the
deposit. It does not compare the paper's formulas with the Lean definitions.
