Public occupancy as an observation

A data structure can hide each stored share individually while revealing their joint value through its visible layout. This distinction matters when a ledger publishes both a collection of shares and the markers identifying which cells were filled by genuine insertions. The GBFPlus protocol records cross-domain transfers in ledger attestations and uses a shared word containing an adjacent-domain identifier. Alexander Richard Towell's note identifies an allowed singleton snapshot in which its occupied cells reveal that identifier directly. The note also gives a sufficient occupied-count certificate for recovering an aggregate from a larger batch. These are the two results targeted here. Towell, v1.0.0

The observer in that setting is a reader of a permissioned ledger. Public visibility means visibility to such a reader, not unrestricted Internet access. The source protocol's construction, publication rules and adjacent-domain recovery checks provide the context; the contribution is limited to the particular metadata and view analyzed in the note. Qin et al., GBFPlus

A finite honest insertion history

A snapshot is an array of $m$ cells. Each cell is either empty or occupied by a $\lambda$-bit word. An occupied all-zero word is distinguishable from an empty cell. Public parameters include the share count $\kappa$, with $1\le\kappa\le m$, and the identifier width $\ell$, with $0<\ell<\lambda$.

A row consists of a set $S_i$ of exactly $\kappa$ distinct positions, a $(\lambda-\ell)$-bit prefix $P_i$ and an $\ell$-bit adjacent-domain identifier $N_i$. Its target is their concatenation $T_i=P_i\Vert N_i$. The array starts empty. A successful insertion reserves an empty selected cell, retains existing occupied words, fills the other empty selected cells with free words, and sets the reserved cell to the residual required by the target. If every selected cell is already occupied, the insertion fails and leaves the array unchanged. These operations follow the construction preceding the note's two propositions. Towell, Section 2

An honest history is a finite sequence of attempts satisfying those rules at every step. Its successful rows and count $c$ are derived from that sequence; an independently asserted integer is not substituted for $c$. Let $O$ be the final occupied set, $w=|O|$, and $Z_j$ its occupied words. The public recovery statistic is

$$R(Z)=\operatorname{suffix}_{\ell}\!\left(\bigoplus_{j\in O}Z_j\right).$$

The statistic takes the snapshot and public widths. It does not take a secret prefix, query token, selected support or insertion history as an input.

Formalization targets

The goal is Proposition 1, singleton disclosure: for every honest history with exactly one successful row,

$$c=1\quad\Longrightarrow\quad R(Z)=N_1.$$

It quantifies over every admitted position set, prefix, pivot and free-share realization. The Lean statement names the sole row by requiring that the derived successful-row list is its singleton list. Towell, Proposition 1

The supporting milestones are:

1. Honest-history invariants: final occupancy equals the union of successful supports; every successful row still XORs to its original target; admissible failed insertions leave the state unchanged.
2. Disjoint-support certificate: the equality $w=c\kappa$ implies that the successful supports are pairwise disjoint. The support lemma also includes the empty history, where pairwise disjointness is vacuous.
3. Proposition 2, aggregate disclosure: for an honest history,

$$c\ge1\ \text{and}\ w=c\kappa \quad\Longrightarrow\quad R(Z)=\bigoplus_{i=1}^{c}N_i.$$

The positive-count condition is retained in this proposition. Its conclusion is an aggregate, not recovery of the individual identifiers or their multiset. Towell, Proposition 2 and its proof

What the formalization adds

The singleton identity identifies an adjacent-domain identifier from a complete share set exposed by occupancy. The larger-batch certificate establishes a narrower aggregate observation when the public occupied count matches the authentic successful count times the share count. It does not characterize every possible disclosure and does not estimate how often the certificate occurs. A deployment interpretation still needs the source's visibility and publication premises. Towell, Sections 1–2

Both propositions already have written proofs in the archived preprint. The accompanying source supplement provides finite computational checks. The remaining work here is to verify their universal statements from an explicit insertion model and preserve that construction-to-statement connection. The draft model has compiled concrete examples, including the published seven-cell array and an occupied zero word; the four theorem items remain open formal obligations. No new mathematical discovery or independent human proof review is claimed.

Where care is needed

The risk lies in changing what constitutes a snapshot or an honest insertion. Treating a zero word as empty changes the occupancy count. Allowing later writes to replace occupied shares can invalidate earlier row equations. Supplying an unrelated count can make the certificate appear applicable when the claimed aggregate is wrong. Assuming all final row equations as part of the definition of honesty would also remove the construction obligation that the mission is intended to check.

The recovery function must remain independent of hidden row data even though the theorem's conclusion refers to the identifier that was inserted. The model must admit genuine executions, including singleton, disjoint and overlapping histories, and must distinguish a legitimate full-support failure from an arbitrary skipped insertion.

Formalization scope

The shared namespace is GBFPlus.OccupancyDisclosure. A configuration stores positive prefix and suffix widths; their sum is $\lambda$. Words are pairs of finite coordinate vectors over $\mathbb Z/2\mathbb Z$. Componentwise addition is XOR, and concatenation places the prefix coordinates before the suffix coordinates. Cells use optional words, so occupancy is represented independently of payload value. Supports are finite sets of valid cell indices with exact cardinality $\kappa$; successful occurrences retain their multiplicity in an ordered list.

Free words and valid pivots are explicit inputs. Universal quantification covers each realization; no probability distribution is needed for these identities. Honest histories are checked transition by transition from the empty state, without assuming the conclusions. The model uses Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474.

Ledger read access, authentic publication, genuine occupancy and timeout rules admitting singleton release are external premises of the source interpretation. The formalization does not model cryptographic position derivation, authentication, ledger execution, the separate data-identifier privacy game, publisher identification, full paths, scan costs or a complete repair. Contributions closing the stated obligations or extracting reusable finite-share and occupancy lemmas are welcome. Alexander Richard Towell supplies the source research and direction; substantial OpenAI Codex assistance in model construction, checks and proposal preparation is disclosed. Independent AI read-backs accompany the draft items and do not substitute for human review.

Selected references

• Alexander Richard Towell, Adjacent-Domain Disclosure from Public Occupancy in GBFPlus, archival preprint v1.0.0, 20 October 2026. DOI 10.5281/zenodo.23497466.
• S. Qin, Y. Zhou, W. Dai, Y. Sun and W. Qiang, Privacy-Preserving On-Chain Attestation for Cross-Domain Data Flows via GBFPlus, Entropy 28 (2026), 947. DOI 10.3390/e28090947.