listFingerprint
plain-language theorem explainer
A base-17 polynomial hash of a finite list of natural numbers: fold left with accumulator a ↦ 17a + x, starting at 0. Gravity analysts cite it to turn the depth-two Loom reading of a Config into a single Nat amplitude. The body is a one-line foldl; no lemmas.
Claim. For a finite list $\ell = (x_0,\ldots,x_n)$ of natural numbers, the fingerprint is the natural number obtained by left-folding $a \mapsto 17a + x$ from seed $0$, i.e. $\sum_{k=0}^{n} x_k\, 17^{n-k}$.
background
The module freezes claims G2/G3 of the order-sensitive gravity proposition: an order-sensitive history on the Loom is read at depth two and seated as an antisymmetric Fin-16 edge current on the generator-(0,2) edge of the Freudenthal/Q3 patch, with no metric $H$ and no $\mu$-coordinate table.
The depth-two reading of a Loom Config is a list of natural numbers (the same second-order content isolated by pair-traces / pair-sum holonomy expansion). That list must be collapsed to a single scalar amplitude before it can be placed on an edge via the antisymmetric seating map. The fingerprint is that collapse: a polynomial evaluation of the list at base 17.
Downstream, the seated amplitude becomes the history response current, and differences of fingerprints between the two distinguished configurations cfgA and cfgB drive the response-difference theorems.
proof idea
Pure definition: one-line List.foldl with step $a \mapsto 17a + x$ and initial value 0. No tactics, no lemmas, no hypotheses.
why it matters
Supplies the scalar amplitude that turns a depth-two Loom reading into a physical edge current on the Q3 patch. Parents: historyResponse casts the fingerprint to $\mathbb{R}$ and seats it on the generator-(0,2) edge via the antisymmetric edge map; historyResponse_fwd / historyResponse_rev recover the signed amplitude on that edge and its reverse; responseDiff_fwd expresses the cfgA/cfgB response difference as the difference of the two fingerprints; fingerprint_separates_cfgAB is the decide-proof that the two depth-two readings have unequal fingerprints, which is the separation half of the frozen G2/G3 claims.
In the Recognition gravity stack this is the MODEL step that treats the depth-two commutator fingerprint as a physical current, feeding the theorem-level separation and metric-image exclusion on cfgA/cfgB without invoking a linearized flat-patch metric perturbation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.