LedgerUniquenessCert
plain-language theorem explainer
A unit certificate whose verification predicate packages three uniqueness facts for the Recognition Science ledger: the golden ratio is the unique positive root of x²=x+1, spatial dimension three is the unique dimension with nontrivial linking, and the Gray-code cycle on the 3-cube has length eight. Auditors of the certificate chain cite it to close Gap 9 (why this discrete structure). Discharge of the predicate is a one-line appeal to the complete ledger-uniqueness theorem.
Claim. A ledger-uniqueness certificate is a unit record. Its verification predicate holds precisely when (i) every real $x>0$ satisfying $x^2=x+1$ equals $\varphi$, (ii) for every integer $D\ge 2$ the linking number in dimension $D$ is nonzero if and only if $D=3$, and (iii) the Gray-code cycle length in dimension $3$ equals $8$.
background
The module packages uniqueness results for the Recognition Science ledger so that a single certificate can answer the structural objection "why this discrete ledger and not another." The three ingredients are the golden-ratio fixed point of the cost law, the spatial dimension forced by nontrivial linking, and the minimal complete cycle on the corresponding hypercube.
Upstream constants fix the notation: the fundamental time quantum is one tick ($\tau_0=1$), spatial dimension is the constant $D=3$ forced by the linking step of the forcing chain, and one octave is eight ticks. The golden ratio $\varphi$ is the unique positive root of $x^2=x+1$, equivalently the self-similar fixed point of the cost projector (T6). Linking number vanishes in $D=2$ (Jordan) and for $D\ge 4$ (Zeeman), leaving only $D=3$ with nontrivial Hopf linking (T8). A Gray-code traversal of the $D$-cube visits $2^D$ vertices; for $D=3$ that length is exactly eight (T7).
proof idea
The structure itself is an empty record (only Repr). The verification predicate is a definitional conjunction of three pure propositions: uniqueness of the positive root of $x^2=x+1$, the biconditional that linking number is nonzero precisely at $D=3$, and equality of the Gray-code cycle length at dimension three with eight.
The companion theorem that every certificate verifies is a one-line wrapper: it applies the already-proved complete ledger-uniqueness result and does no further rewriting.
why it matters
This certificate closes Gap 9 in the verification chain: the claim that the ledger parameters are not an arbitrary discrete choice. It packages the three forcing landmarks that pin the structure: T6 ($\varphi$ as unique positive cost fixed point), T8 ($D=3$ as unique linking dimension), and T7 (eight-tick octave as minimal complete cycle on the 3-cube).
Because the objection "other discrete ledgers could work" is answered by uniqueness rather than existence, downstream certificate consumers can treat the ledger skeleton as forced rather than postulated. The module doc states the three mathematical content blocks explicitly (quadratic formula for $\varphi$, Jordan/Hopf/Zeeman for linking, $2^D$ for Gray-code length), so the certificate is the audit-facing surface of those classical facts inside the RS forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.