| # | Description | Status | Sources |
|---|---|---|---|
| A. Inputs: imported, not derived here | |||
| A1p26001 | $\NPC$-completeness and self-reducibility: satisfiability is $\NPC$-complete (Cook, Levin), the reductions reach combinatorial mathematics (Karp), and polynomial time is invariant across the standard machines (Church–Turing). | I | [Cook 1971; Levin 1973; Karp 1972; Hartmanis & Stearns 1965] |
| A2p26002 | Proof complexity, used as proved: $\NPC=\coNP$ iff some propositional proof system is polynomially bounded (Cook–Reckhow); Extended Frege is not automatizable unless RSA breaks, bounded-depth Frege unless factoring and Diffie–Hellman are feasible, and resolution is $\NPC$-hard to automate. | I | [Cook & Reckhow 1979; Kraj'ivcek 1995; Kraj'ivcek & Pudl'ak 1998; Bonet et al. 2000; Atserias & M"uller 2020] |
| A3p26003 | One-way functions and the average case: the discrete logarithm and factoring as the canonical instances (Diffie–Hellman), Impagliazzo’s worlds; Shor’s order finding, which inverts both for a quantum observer. | I | [Diffie & Hellman 1976; Impagliazzo 1995; Shor 1997] |
| A4p26004 | The three barriers: relativization (Baker–Gill–Solovay), natural proofs (Razborov–Rudich), algebrization (Aaronson–Wigderson); Wigderson’s survey of what a separation must use. | I | [Baker et al. 1975; Razborov & Rudich 1997; Aaronson & Wigderson 2009; Wigderson 2019] |
| A5p26005 | Eckmann and Tlusty: under uniform angle scaling a single walk in $\mathrm{SO}(3)$ reaches the identity only on a measure-zero set, while the doubled walk returns for some exponentially large scaling, delivered non-constructively. | I | [Eckmann & Tlusty 2025] |
| A6p26006 | The corpus: the horizon clause and its complexity face (00:Z1–Z4; 25:G3, 25:G7), the shell theorem (00:Z10; 20:E1, 20:E12), the scale import $\Om=4S+1$ (00:A5), the window ladder $P^{2}<\Om$ (00:B8), the four generative levels (00:B6), the drive of every prime shell (00:A10). | I | |
| B. Computation as counting along a representation | |||
| B1p26007 | A representation $R=(E_R,O_R,c_R)$: an encoding, a finite set of elementary operations, and the cost, the graph distance in $G_R$. $R$ is admissible when it and a standard machine simulate each other with polynomial overhead. Cost is counted in bit operations, $\ell=\log_2P$ for a carrier element and $n$ for a stored length-$n$ object. | D | Def. 2.1 |
| B2p26008 | Cost is a function of the pair (target, representation), not of the target alone: a target far in one chart can be near in another, and the transform between charts is itself a path. “Within the horizon” is a predicate on pairs. | D | Claim 2.2 |
| B3p26009 | The longitudinal turn on the shell: the multiplicative characters $\chi_\nu(g^t)=g^{\nu t}$ are eigenvectors of the scale shift $x\mapsto gx$, with the $(P-1)$-th roots of unity $g^{\nu}$ as distinct eigenvalues; the shift $x\mapsto g^{r}x$ fixes every unit when $(P-1)\mid r$ and none otherwise. | T |   Prop. 2.3; A6 master: 00:Z10 |
| B4p26010 | The continuum reading [chart]: the dilation generator $\HH=-\mathrm i(x\partial_x+\tfrac12)$ has $x^{-1/2+\mathrm i\nu}$ as eigenfunction of eigenvalue $\nu$ on $x>0$, so the frequency index is the spectrum of $\HH$ in the chart of the scale shift (20:E1). | T |  Prop. 2.3; B3 |
| B5p26011 | The Gauss sum couples the two turns: multiplication by a unit permutes the units; $\sum_{t\neq0}\psi(tc)$ is $-1$ for $c\neq0$ and $P-1$ for $c=0$; $\sum_u\chi(u)=0$ for $\chi\neq1$; hence $\lvert g(\chi)\rvert^{2}=P$ for every nontrivial $\chi$ on the shell ($\Om$ on the Carrier). | T | Rem. 2.4; B3 |
| C. The comprehension horizon | |||
| C1p26012 | Two horizons, nested: the per-instance feasible horizon $H(\ell)$, polynomial in the feasible regime, and the absolute horizon $\Om^{1/4}$, the observer’s total budget in the totality. The totality holds the inverse of every ascent whole, the table of $P-1$ index pairs, below its own count: the endpoint-given oracle. | D | Def. 3.1; A6 |
| C2p26013 | The family’s size and the table beyond the horizon [chart]: at the anchor $2^{204}<\sqrt\Om<2^{205}$, so the shells of the family $P^{2}<\Om$ have at most $205$ bits; $2^{102}<\Om^{1/4}<2^{103}$, so a decision table with one entry per $204$-bit input exceeds the absolute horizon and lies below $\sqrt\Om$. | T | Rem. 4.4; A6 master: 00:B8 |
| D. Proof as a bounded path; certificate as a near-representation | |||
| D1p26014 | The classes in a representation: $L\in\PC_R$ when a $\mathrm{poly}(\ell)$ uniform rule selects each next operation and the deterministic forward path reaches the decision bit within $H(\ell)$; $L\in\NPC_R$ when a certificate of polynomial length places “accept” within $H(\ell)$ of $(E_R(x),w)$. The axis is find versus exist. | D | Def. 4.1 |
| D2p26015 | Faithfulness: for every admissible $R$, $\PC_R=\PC$ and $\NPC_R=\NPC$. The forward direction simulates each operation in polynomial time and guesses the operation sequence with the certificate; the reverse rewrites a standard computation as an $R$-derivation of polynomial length. | T | |
| D3p26016 | The classes are representation-invariant; what varies with $R$ is the cost of a specific target within a fixed budget. A certificate is a representation in which the far target is near: supplied ($\NPC$) rather than forward-constructed ($\PC$). | D | |
| D4p26017 | Faithfulness is to the class structure on the carrier family: the carrier classes are $\PC$ and $\NPC$, the textbook asymptotic classes their degenerate idealisation. No tower of carriers is admitted; a fixed length admits a decision table, decided by the totality, unreachable below the horizon (C2). | D | |
| E. P versus NP: finding versus checking | |||
| E1p26018 | The search problem $\mathrm{Search}_V$ of $L\in\NPC$ with verifier $V$ and witness bound $p$ maps an instance to a witness or to $\bot$. The near-representation is forward-constructible iff $\mathrm{Search}_V\in\mathrm{FP}$. | D | Def. 5.1 |
| E2p26019 | The crisp form: $\PC=\NPC$ iff $\mathrm{Search}_V\in\mathrm{FP}$ for every $L\in\NPC$, equivalently for $\mathrm{SAT}$; by self-reduction on the variables and the witness-preserving Cook–Levin reduction. | T | |
| E3p26020 | A propositional proof system is a polynomial-time onto map $\Pi$ to $\mathrm{TAUT}$; $p$-bounded when every tautology has a polynomial-size proof; automatizable when some algorithm finds a proof in time polynomial in the tautology and its least proof size. | D | Def. 5.3 |
| E4p26021 | The witness–automatization dictionary: for $L\in\NPC$ with verifier $V$, $\mathrm{Search}_V\in\mathrm{FP}$ iff the certificate system $\Pi_V$ (a witness system, not a system for $\mathrm{TAUT}$) is automatizable; so $\PC=\NPC$ iff every witness system is automatizable. | T | |
| E5p26022 | Finding collapses to checking: if $\PC=\NPC$ then every propositional proof system is automatizable, the proof built bit by bit by self-reduction on the predicate “$\tau$ has a $\Pi$-proof of size at most $s$”. | T | |
| E6p26023 | The gap is finding versus existing: the truth-table system is automatizable but not $p$-bounded, so existence ($\NPC=\coNP$) and discovery are distinct; the known separations condition the gap on the hardness of factoring and the discrete logarithm, the substrate’s descent. | D | |
| E7p26024 | A localizing chart for $x\in L$: an admissible chart in which some witness lies within the polynomial horizon of $\mathbf0$. A constructive localising selector emits, in $\mathrm{FP}$, such a chart with a canonical forward rule whose orbit reaches the witness in $\mathrm{poly}(\ell)$ steps. Proximity alone is insufficient. | D | Def. 5.7 |
| E8p26025 | Existence is free: for every witness index $m$ of the scale chart the translation $j\mapsto j+(n-m)+1$ of the index cycle is a chart (a bijection of the cycle) that places $g^{m}$ one counting step from the origin, $g=g^{0}\cdot g$. The witness enters only to name the chart. | T | Prop. 5.8; E7 |
| E9p26026 | The selector is the content: a constructive localising selector for every $L\in\NPC$, equivalently for $\mathrm{SAT}$, exists iff $\PC=\NPC$; a selector for a single easy $L$ does not suffice. | T | |
| E10p26027 | The counting distance of a unit along the orbit of $g$ is its index: $m\mapsto g^{m}$ is a bijection of the index cycle onto the units, the distances $1,\dots,P-1$ have mean $P/2$ and maximum $P-1$, between $2^{\ell-1}$ and $2^{\ell}$ for $\ell$ the bit length. | T | Rem. 5.9; A6 master: 00:A12 |
| E11p26028 | Three quantities differ: the naive orbit length (up to $2^{\ell}$ steps), the cost of a specified algorithm (baby-step–giant-step, F3), and the minimum complexity of the descent, the open lower bound. The bijection of E10 bounds none of them. Short to name is not short to find. | D | |
| F. The directional asymmetry is a one-way function | |||
| F1p26029 | Charts and the family: on $\F_P$ the additive chart and the scale chart $(\F_P^{\times},\cdot)\simeq C_{P-1}$; with a fixed generator $g$ the ascent $a_P(j)=g^{j}$ and the descent $d_P=\mathrm{dlog}_g$. The carrier family is $\{\F_P:P^{2}<\Om\}$ (00:B8), input size $\ell$, feasibility $\mathrm{poly}(\ell)$. | D | |
| F2p26030 | Ascent is feasible: square-and-multiply computes $g^{j}$ in at most $2\,\mathrm{bits}(j)$ modular multiplications, hence at most $2\ell$ for $j<P$; on the three carriers $17$, $26$, $38$ multiplications at $j=P/3$, right to left with the last squaring skipped [data]. | T | Thm. 6.2; F1 |
| F3p26031 | The descent’s count: with $m^{2}\ge P-1$ baby steps $1,g,\dots,g^{m-1}$ ($m$ entries, one multiplication per step) and at most $m$ giant steps, baby-step–giant-step recovers from $g^{x}$ an index $y$ with $g^{y}=g^{x}$; at most $2m$ operations, $m=\lfloor\sqrt{P-1}\rfloor+1$; $134$, $1334$, $13334$ on the three carriers [data]. | T | § 6; F1 |
| F4p26032 | Three scales: the feasibility budget $\mathrm{poly}(\ell)$, exceeded by the descent; the per-instance descent $2\sqrt P$, at most $\Om^{1/4}$ on the family, superpolynomial yet far below carrier scale; the uniform statement that no $\mathrm{poly}(\ell)$ inverse exists across the family, with no per-instance witness. | D | |
| F5p26033 | A one-way family: each $f_\ell$ computable in $\mathrm{poly}(\ell)$ while every $\mathrm{poly}(\ell)$-time inverter succeeds on at most a sub-horizon fraction of the carrier, the finite-totality reading of negligibility. | D | Def. 6.3 |
| F6p26034 | One-way implies separation: if a one-way family exists then $\PC\neq\NPC$, since inverting $f$ is the search problem of the verifier $[f(x)=y]$, which $\PC=\NPC$ would place in $\mathrm{FP}$. | T | |
| F7p26035 | The scale-descent residue: the ascent family $\{a_P\}$ on the carrier family is one-way, $\mathrm{poly}(\ell)$ forward and inverted by no $\mathrm{poly}(\ell)$ forward computation. Decided by the totality, beyond the bounded observer; the complexity literature posits the same statement as the discrete-logarithm hardness assumption (00:Z4). | Ω | master: 00:Z4 |
| F8p26036 | If the scale descent is one-way (F7) then $\PC\neq\NPC$. | T | |
| F9p26037 | The native locus: ascent is a horizon-bounded forward count, descent its inverse below the horizon; $\PC\neq\NPC$ follows from F7 one way, the converse not known. The single arrow of the drive is the structural reason for the residue, the descent the time-reversed branch a composed observer cannot freely take. | D | |
| F10p26038 | The descent is the inverse coordinate map: $a_P:j\mapsto g^{j}$ is the bijection of $C_{P-1}$ onto $\F_P^{\times}$ carrying the time index to its position, and $d_P=\mathrm{dlog}$ its inverse, a cyclic-group coordinate, not the inverse of the multiplicative Fourier transform (B3). | T | master: 00:A12 |
| F11p26039 | The scaling flow returns the doubled walk: Eckmann and Tlusty’s two facts (A5) read on the shell as the find–exist split, a designated point unreachable by the single scaling, the relaxed target met non-constructively at an exponential scaling. A geometric parallel, not a lower bound. | I | |
| G. The arithmetic-hierarchy closure | |||
| G1p26040 | The four primitive roles on $\F_P$ with the generator $g$: succession $x+1$, addition $x+a$, multiplication $mx$, fixed-base exponentiation $a_P(j)=g^{j}$, each the previous iterated with a fixed operand; the fourth is the top, its inverse the discrete logarithm. | D | Def. 7.1 |
| G2p26041 | Ladder closure: the four roles generate the two cyclic structures, $C_P$ additive and $C_{P-1}$ multiplicative, with the bridge $a_P$. A tower exponent $g^{j}$ is read modulo $P-1$, so tetration is exponentiation of a reduced index, and the power map acts on the index as multiplication; no third cyclic structure hosts a fifth role (00:B6). | T | master: 00:B6 |
| G3p26042 | Phase-index dynamics: in the scale chart $x=g^{m}$ the power map acts by $P_k(g^{m})=g^{km}$ and its iterates by $P_k^{\,r}(g^{m})=g^{k^{r}m}$, the exponents read modulo $P-1$; the ascent is the orbit traversal $g^{j+1}=g\cdot g^{j}$, one multiplication per counted step. | T | Thm. 7.3; G1 |
| G4p26043 | The one-way function is the inverse of the last role: each forward role costs one modular operation, the ascent at most $2\ell$ multiplications; the descent recovers the index, the position in the counted orbit of the fourth role. The descent/ascent operation ratio at the three carriers is $134/17$, $1334/26$, $13334/38$ [data]. | T | |
| G5p26044 | The power map $P_k$ is a bijection of $\F_P^{\times}$ iff $k$ is invertible modulo $P-1$, inverted by $x\mapsto x^{a}$ with $ak\equiv1$; otherwise its image is the cycle of $g^{d}$, $d=\gcd(k,P-1)$, of exactly $(P-1)/d$ elements. | T | Rem. 7.5; G3 |
| G6p26045 | The index cycle $C_{P-1}$ is the abelian hidden-subgroup datum on which Shor’s transform acts, the chart H5 marks as the hard classical case. The one-way map is the exponential $a_P$, whose inverse is the discrete logarithm, not the power map, which is efficiently inverted when bijective (G5). | D | |
| H. The transform map | |||
| H1p26046 | The two quarter turns as a structured correspondence: the transverse turn (the additive transform) is forward-computable classically on a stored vector; the longitudinal turn’s period is reached by a $\BQP$ observer through order finding, not by reading a transform vector. A correspondence between charts and the observers that reach them, not a complexity theorem. | D | |
| H2p26047 | A chart change $T$ is forward-computable when $T$ and $T^{-1}$ lie in $\PC$; a problem is transform-diagonalisable by $T$ when its instances become pointwise in the $T$-chart. Well defined for abelian and hidden-subgroup problems, not a feature of $\NPC$ at large. | D | Def. 8.2 |
| H3p26048 | Fourier-diagonalisable implies $\PC$: the additive transform on the shell is exact and self-inverse, $T^{-1}T=1$ on the full cycle $n=P-1$ (the round trips on the sub-cycles $n=8$, $256$, $2^{16}$ over $\F_{17}$, $\F_{257}$, $\F_{65537}$ [data]); the cyclic convolution costs $n^{2}$ multiplications in the position chart and $\tfrac32n\log_2n+n$ through the transform ($1\,048\,576$ against $16\,384$ at $n=2^{10}$) [data]. | T | |
| H4p26049 | Structured witness sets are forward-localizable: when the witnesses of $x$ are the solutions of an affine $\F_2$-system readable from $x$, Gaussian elimination returns a particular solution $w_0$ and a basis; the chart $w\mapsto w-w_0$ places $w_0$ at $\mathbf0$ and every solution within the basis’s size in counting steps. | T | |
| H5p26050 | The scale chart is the hard case: the discrete logarithm is the carrier’s native order-finding instance, reached by a $\BQP$ observer and, under F7, by no classical forward computation; factoring is a distinct instance not covered by F7. A correspondence on structured instances, not a boundary theorem. | D | |
| J. The scope and the barriers | |||
| J1p26051 | A universal constructive selector would invert the one-way family: applied to the inversion family of a one-way $f$ it inverts $f$ in $\mathrm{poly}(\ell)$; under F7 none exists, and its non-existence is equivalent to $\PC\neq\NPC$ (E9). The natural-proofs reading is an analogy, the density not established. | T | |
| J2p26052 | The barriers as obstructions: relativization treats the shell as a featureless sphere, natural proofs forbid a large generic marking where the hardness is the non-generic alignment with the arrow, algebrization adds an algebraic oracle the carrier’s scale arithmetic replaces. The reading is a locus, not a technique the barriers exclude. | D | |
| K. The horizon clause and the residue | |||
| K1p26053 | $\Om$-hard: a statement the totality decides and whose instance witnesses are checkable at sub-carrier scale, while its uniform forward-findable certificate is carrier-scale, below the bounded observer’s horizon. Decidable, not undecidable: settled at the scale of the whole (00:Z3). | D | § 10; A6 master: 00:Z3 |
| K2p26054 | The three faces: the shell theorem’s classical screen value in 20-rh (every mode on the self-dual line; classical RH as the count equality, $\Om$-hard in its uniform form), the uniform per-$n$ Goldbach bound, and the forward-invertibility of the scale descent are one horizon clause, decided by the totality beyond the bounded observer (00:Z2). | D | master: 00:Z2 |
| K3p26055 | Frequency and the spectrum [chart]: the frequency chart is the spectrum of the scale shift on the shell (B3), the dilation generator its continuum reading (B4, 20:E1). The Hilbert–Pólya correspondence is a target of 20-rh, not a result; the spectral and the computational faces meet on the one $\HH$-axis as a reading. | D | |
| K4p26056 | An arrow-forward computation: a $\mathrm{poly}(\ell)$-length path applying only the drive-forward operations of the carrier. | D | |
| K5p26057 | Why the single arrow stops short of a proof: forbidding the inverse outright is circular; admitting every $\mathrm{poly}(\ell)$ operation makes the exclusion $\mathrm{dlog}\notin\mathrm{FP}$, which implies $\PC\neq\NPC$ one way; the closure removes the circularity (G4) and leaves the lower bound as the residue. | D | |
| K6p26058 | The irreducible residue: the uniform certificate that the inverse of the last role has no $\mathrm{poly}(\ell)$ forward algorithm across the carrier family, the computational face of the horizon clause, decided by the totality and below the bounded observer’s horizon (00:Z4). | Ω | master: 00:Z4 |
Nothing matches that filter.
Status
- I
- Import. A standard result used as proved, or a result of the corpus.
- D
- Definition. A naming or set-up move, or a reading of the construction, carrying no claim of its own.
- T
- Theorem. Derived within this paper from the rows above it; where a py token is named, its content is reproduced by the framework’s ledger file; where a lean token is named, proved in Lean. A continuum reading of a finite object is marked [chart]; its witness is a certified bracket or a Mathlib theorem on the reals. A table of computed values is marked [data].
- Ω
- $\Om$-hard. Decided by the totality; its uniform certificate below the bounded observer’s horizon.
Sources
- Gold: the python check that decides the predicate, at its line in the script (the source, rendered on this site); on hover the deciding family and the families that corroborate it, and the verdict of the last run (red when it fails). The script page's bar runs the predicate's cell of the package's notebook on Google Colab (one cell per predicate; the whole notebook from the header badge).
- The predicate as one Lean declaration, named by its accession key (
p26009) — the conjunction of the theorems that prove it — at its line in the rendered module, one mark per library that proves it, the core's first. Green: the core (lean/FrcCore) — the statement on the shell ring, by computation and induction, no Mathlib, no axioms: the finitist witness. Violet: Mathlib (lean/FrcLedger) — the classical statement for every shell on Mathlib's hierarchy (its axioms,propext,Classical.choice,Quot.sound, on hover). Red: a proof the gate rejects (an unfinished proof,native_decide) — not a witness. A predicate proved in both libraries shows both marks; one mark, one proof. The module page's bar opens the module as one executable file in Lean Live (the core on plain Lean, no Mathlib; the file elaborates in the browser and prints every predicate's axioms at its end); the header's two Lean badges count the marks of each colour and open the two executables. - section
- The statement in the paper's body that carries the predicate: a proposition, a remark or a section.
- rests on
- The predicates it rests on, by label: realisations, definitions and imports of this ledger, predicates of other ledgers (
32:B3) and of the master (00:D15).