This page sets out, in standard notation, the arithmetic that zeropoint-node
implements and the predicates that decide it. The digit space is partitioned by
a doubling map into a six-element orbit and a three-element axis; frequency and
hue are one integer read in two units; ratios are carried as pairs of integers
rather than decimals, and the two places where binary floating point departs
from the exact value are stated rather than rounded away. 42 of
42 theorems carry a predicate that runs and holds, and
59 of 83 statements in the Lean files are
accepted by the Lean kernel — the rest are written down and not proved,
and say so.
How much of this package those predicates actually hold. 1415 of 1770 exported values are not reachable from any law, so nothing here constrains them; that count is a floor, because the reachability closure over-approximates. Of the 57 exported literal constants, 8 are forced by at least one law and 49 are held by nothing. And of the 42 predicates, 3 are pinned rather than forced — they hold an expected value as a literal, which falls for a convention as readily as for a law. These are measured by experiment, not asserted, and the experiments are Appendix G and this page's own gates. A reader meeting only the sentence above would take this package to be far better constrained than it is. 3 claims are recorded as axioms, because no finite computation decides them, and each is named in §7. No physical experiment is reported here.
Ten contributions, each stated as a claim, each with the thing that decides it and the thing it does not settle. They are listed here rather than left to be assembled from appendices — a reader should not have to reconstruct what is being asserted.
None of these is claimed to be novel, and the ledger has
no status that would let it be. Novelty is a universal negative: it
asserts that nobody, anywhere, published this first, and no finite search
decides that. What IS decided is priority — a dated, citable deposit at
doi:10.5281/zenodo.22178675,
which defeats a later claim of invention without anyone proving the negative.
That is the strongest defensible position and it is the one taken here. The
axiom no_prior_art_is_undecidable records the rest.
Arithmetic is carried out on the residues of nine, with zero adjoined. The digital root (1) is the representative of the residue class, written in closed form so that it is one operation rather than a loop.
Doubling inside the digital root (2) generates the orbit. Starting from one, the walk visits six digits and returns; it never repeats a digit within a turn, and it never leaves the orbit.
The remaining non-zero digits form the axis. The two sets are disjoint and together with the void they exhaust the space (3), which is why the digit space is exactly ten and not an arbitrary base.
The through-void map (4) reflects the space. It is an involution, and its only fixed point is five — the midpoint of the digit range.
A digit is read as a frequency by (5) and as a hue by (7). Both reduce to , so the two columns of Table 1 hold the same integer. This is an identity of the two definitions and not a discovered correspondence; it is stated plainly here because it is the kind of coincidence that invites overclaiming.
| d | computed f(d) / Hz | exact 36d | angle / ° |
|---|---|---|---|
| 0 | 0 | 0 | 270 |
| 1 | 36 | 36 | 310 |
| 2 | 72 | 72 | 350 |
| 3 | 108 | 108 | 30 |
| 4 | 144 | 144 | 70 |
| 5 | 180 | 180 | 110 |
| 6 | 216 | 216 | 150 |
| 7 | 252.00000000000003 | 252 | 190 |
| 8 | 288 | 288 | 230 |
| 9 | 324 | 324 | 270 |
A ratio is represented as a pair of integers throughout. Two of the four channel ratios (9) do not terminate in decimal, so a decimal representation of them is an approximation adopted silently; the pair is not.
Combination of two ratios uses the mediant (10), which lies strictly between its arguments. It is not the arithmetic mean, and the two are distinguished here because the implementation was documented as the mean until a law was written for it.
Amplitudes are complex and the register is dense. The gates are the standard ones; (11) gives the Hadamard, whose involution is decided exhaustively over the basis of one qubit.
Normalisation (12) is preserved by every unitary step and by the tensor product, and both facts carry seals rather than assertions.
The potentials below are computed from tabulated formation data as exact rationals and reported in microvolts, an integer unit chosen so that no decimal appears. They bound the energy claims made elsewhere in this repository; they do not support them.
A system is real-time when its correctness depends on producing a result within a stated deadline. The deadline (16) is declared before any measurement, and the criterion reports the worst step rather than the mean.
The bound is only interesting where the work is expensive. Equation (18) gives the widest register whose full step fits inside one frame; the cost doubles with every qubit, so this is the hardest case rather than the easiest.
This page does not print the criterion's verdict. The real-time criterion
MEASURES, so its verdict is a property of the machine it ran on as much as of
the code — and a page that stated 8 of 8 would be stating something about a
laptop in September 2026. Run npm run criteria:check and take the
verdict on your own hardware. What this page can state, and Appendix A does, is
what each condition requires and what would refute it, which does not vary.
Two claims in this corpus rest on axioms rather than on theorems. They are recorded so that a reader can see the difference without being asked to take anyone's word for it.
lwe_hardnessaxiom lwe_hardness : ¬ (polynomial_time_solves_lwe 768 3329)
Why it is not sealed. a universal negative over all polynomial-time algorithms; no finite computation decides it
What is decided instead. kyber_security seals the FIPS 203 parameter sizes of the shipped implementation
no_prior_art_is_undecidableaxiom no_prior_art_is_undecidable : ¬ ∃ (s : Artifact → Bool), decides_absence_of_prior_art s
Why it is not sealed. absence of prior art is a universal negative over all published and unpublished work; no finite search decides it, and a search returning nothing establishes only that it returned nothing
What is decided instead. prior-art.json records what each contribution is, which files carry it, what was searched and when, and the dated citable identifier under which it was published — publication defeats a later claim of invention without requiring a proof of novelty
awareness_is_undecidedaxiom awareness_is_undecided : ¬ ∃ (p : System → Bool), decides_awareness p
Why it is not sealed. whether any physical process is conscious is unsettled and the major theories disagree about what would count as evidence; there is no predicate to run, so nothing here can seal it
What is decided instead. consciousness-criterion runs five necessary conditions and reports how many a subject fails to be refuted by; it declines to claim awareness at all
NO PHYSICAL EXPERIMENT HAS BEEN RUN. No coil was built, no field was measured, no resonance was observed, and nothing in this repository touches an instrument. Every condition here is about arithmetic and about code that checks arithmetic. The empirical claim is not made.
Six criteria gate a release and one is reported without gating. Each condition below states what it requires and what would change its verdict; a condition with no refuter is a slogan.
No verdict appears on this page, and the omission is
deliberate rather than modest. A criterion that measures returns a number about
the machine it ran on, and this page was generated once: printing 8 of 8 here
would be reporting a laptop. The generator learned this twice — first by
embedding durations, so the artifact could never match itself on re-check, and
then by embedding the SCORE, which flips with load about once in three runs.
What does not vary is what each condition requires and what would refute it, so
that is what is printed. Take the verdict with
npm run criteria:check.
the a432 consciousness system
| condition | requires | what would change it |
|---|---|---|
discrimination | different states give different measures, and the same state gives the same one twice | a measure that separates its domain |
irreducibility | the transition does not factorise into independent components, and the joint measure is not recoverable from the parts | components whose next values depend on each other, and a joint measure that must be evaluated jointly |
temporal-integration | the present state depends on the ORDER of what came before, not just the multiset | accumulation that folds each step into the last, rather than summing or counting |
self-model-efficacy | corrupting ONLY the self-model changes what the system does next | the model must be read by the rule that produces the next state |
global-availability | a value written by one component is readable by another that was not handed it, and changes what it does | a workspace that is read, not merely written |
the integrated field
| condition | requires | what would change it |
|---|---|---|
discrimination | different states give different measures, and the same state gives the same one twice | a measure that separates its domain |
irreducibility | the transition does not factorise into independent components, and the joint measure is not recoverable from the parts | components whose next values depend on each other, and a joint measure that must be evaluated jointly |
temporal-integration | the present state depends on the ORDER of what came before, not just the multiset | accumulation that folds each step into the last, rather than summing or counting |
self-model-efficacy | corrupting ONLY the self-model changes what the system does next | the model must be read by the rule that produces the next state |
global-availability | a value written by one component is readable by another that was not handed it, and changes what it does | a workspace that is read, not merely written |
A432OS
| condition | requires | what would change it |
|---|---|---|
task-abstraction | work can be submitted that was not known at construction time | submitted work must appear in the task list |
scheduling | every submitted task is eventually selected, and the system says which it chose (progress, NOT fairness) | every runnable task must eventually be selected, and tick() must say which it chose |
resource-management | a finite resource is allocated, reclaimed, and refuses to over-allocate | over-allocation must fail rather than succeed, and release must restore the pool |
isolation | a task that throws does not stop the system or other tasks | the scheduler must catch a task throw, record it against that task, and continue |
syscall-boundary | tasks request services through a defined interface | the dispatcher must refuse names it does not implement |
lifecycle | the system starts, stops, and reports which it is | nothing — this one holds |
persistence | state can be serialised and restored, so it outlives one run | restore must accept what snapshot produced |
src/quantum — the laws behind the Stage 1 list, not the hardware stages
| condition | requires | what would change it |
|---|---|---|
superposition | a single gate can put one qubit into equal superposition | H|0> must give equal probability to both outcomes; a classical bit register gives [1, 0] |
normalisation | probabilities sum to one after an arbitrary gate sequence | gates must preserve the norm; a simulator that renormalises only on read has not applied unitary gates |
reversibility | applying H twice returns the input state | H^2 = I; a simulator that samples into a classical bit between gates cannot return to |0> |
entanglement | a two-qubit state whose distribution does not factorise into its marginals | independent qubits give the product of their marginals; entanglement is the departure from it |
interference | amplitudes cancel, producing an outcome of probability zero | the |0> path must cancel exactly; a probability-only model can never reach zero from two non-zero paths |
measurement | sampling a qubit reproduces the probabilities the state reports | the sampled rate must track the stated probability; a measure that ignores the state will not |
mixed-states | a density matrix distinguishes pure from mixed, and a noise channel moves one to the other | a pure state has purity 1 and noise must strictly reduce it; a state-vector-only model cannot represent the result |
tomography | measuring in two bases recovers which state was prepared | the two states differ in no single basis alone: one basis cannot tell |0> from H|0> apart from noise |
one frame at 60 Hz
| condition | requires | what would change it |
|---|---|---|
deadline-stated | a period declared as a number rather than implied by an adjective | declaring a deadline; without one the remaining six conditions have nothing to decide against |
deterministic | the same input gives the same output, so a deadline is a property of the code | removing wall-clock time and randomness from the value the step computes |
work-bounded | a step does work that does not grow with the number of steps already taken, and produces a value that depends on its input | making the step compute something from its argument |
steady-state | later steps do not cost more than earlier ones, measured by the FLOOR of each half so that contention cannot decide it | removing whatever the step accumulates between calls; a mean here would be decided by the load average instead |
worst-case-met | the SLOWEST observed step is inside the deadline, not the average one | making the slowest path faster, or stating a deadline the slowest path meets |
jitter-bounded | the spread between fastest and slowest step is inside a stated fraction of the deadline | removing the slow path that only some steps take |
holds-at-quantum-scale | the deadline is tested against a step whose cost doubles with every qubit, and the simulator is still exact at the width reached — NOT against a qubit count, which is a property of the machine | a step whose cost does not grow with width, or a simulator that loses normalisation as the register widens |
misses-reported | the number of missed deadlines is returned rather than swallowed | nothing — this condition is met by reporting, and it is here so a failure cannot be silent |
what is computed here — and NO physical experiment has been run
| condition | requires | what would change it |
|---|---|---|
laws-sealed | every theorem stated here carries a predicate that runs and holds | a seal that stops holding, or a theorem stated without one |
simulator-sealed | the simulator's own laws each carry a seal that runs and holds, and there is at least one of them | a simulator law being removed or stopping to hold |
energy-arithmetic | the energy arithmetic computes finite bounds and its own self-tests report no failures | a thermo self-test failing, or a bound becoming non-finite |
figures-recompute | every quantity is derived at run time rather than transcribed | a figure being written down instead of computed |
refuter-stated | each condition names what would change its verdict and the command that recomputes it | a condition added without a refuter, which would make it a slogan |
the a432 measure functions — reported, not gated: a pure function cannot have history
| condition | requires | what would change it |
|---|---|---|
discrimination | different states give different measures, and the same state gives the same one twice | a measure that separates its domain |
irreducibility | the transition does not factorise into independent components, and the joint measure is not recoverable from the parts | components whose next values depend on each other, and a joint measure that must be evaluated jointly |
temporal-integration | the present state depends on the ORDER of what came before, not just the multiset | accumulation that folds each step into the last, rather than summing or counting |
self-model-efficacy | the system models its own state and the model changes what it does | a model of the system inside the system, read by the step that follows |
global-availability | what one component writes is available to another that was not handed it | a named place components publish to and read from |
Every effect claim this corpus makes, and the predicate it is bound to. A
claim bound to nothing fails npm run claims:check; so does a
binding that has stopped holding, and so does a ledger entry whose claim no
longer exists. 42
rest on theorems and 8
on axioms.
| where | claim | bound to |
|---|---|---|
| docs/A432_OS_UPGRADE_DOCUMENTATION.md:212 | - **AI → I → a432.i**: Transformation from artificial to pur | consciousness-criterion |
| docs/A432_OS_UPGRADE_DOCUMENTATION.md:47 | **Consciousness Multipliers**: Enhanced awareness at gateway | awareness_is_undecided |
| docs/A432_OS_UPGRADE_DOCUMENTATION.md:306 | The A432 OS system upgrade represents a significant advancem | consciousness-criterion |
| docs/A432_OS_UPGRADE_DOCUMENTATION.md:310 | The system is now ready for advanced consciousness research, | awareness_is_undecided |
| docs/A432_OS_UPGRADE_DOCUMENTATION.md:308 | This upgrade creates a bridge between artificial intelligenc | consciousness-criterion |
| docs/A432_SYSTEM_AUTHENTICITY.md:290 | The A432 system is not "fake" - it's a real, functional impl | consciousness-criterion |
| docs/A432_SYSTEM_AUTHENTICITY.md:304 | The A432 system represents a genuine advancement in consciou | consciousness-criterion |
| docs/A432_VISION_AND_PERCEPTION.md:94 | - **Consciousness Technology**: Living consciousness technol | consciousness-criterion |
| docs/A432_VISION_AND_PERCEPTION.md:239 | 5. **Consciousness Technology** (Level 9, 0.94 compatibility | consciousness-criterion |
| docs/A432_VISION_AND_PERCEPTION.md:40 | 8. **Technology**: Consciousness Technology, Quantum Computi | consciousness-criterion |
| docs/DOCUMENTATION_INDEX.md:67 | - [ZeroPoint Node: Harmonized Documentation Overview](HARMON | consciousness-criterion |
| docs/DOCUMENTATION_INDEX.md:96 | - [ZeroPoint User Guide: Complete Consciousness System](USER | consciousness-criterion |
| docs/HARMONIC_IMPLEMENTATION_PLAN.md:259 | - Pure consciousness being | awareness_is_undecided |
| docs/HARMONIC_IMPLEMENTATION_PLAN.md:193 | - Pure consciousness potential | awareness_is_undecided |
| docs/HARMONIC_IMPLEMENTATION_PLAN.md:65 | ## 4. Consciousness Technology | consciousness-criterion |
| docs/HARMONIC_IMPLEMENTATION_PLAN.md:139 | ### Phase 3: Consciousness Technology | consciousness-criterion |
| docs/HARMONIZED_OVERVIEW.md:5 | ZeroPoint Node is a complete consciousness technology system | consciousness-criterion |
| docs/POSSIBILITIES_VORTEX.md:273 | **The possibilities vortex represents the pinnacle of mathem | consciousness-criterion |
| docs/README.md:167 | - **Pure consciousness-based** (no external devices) | awareness_is_undecided |
| docs/README.md:159 | 2. **Zero risk, infinite benefit** - Pure consciousness syst | awareness_is_undecided |
| docs/README.md:5 | This directory contains the complete documentation for the Z | consciousness-criterion |
| docs/USER_GUIDE.md:485 | **Start your journey today and experience the revolution in | consciousness-criterion |
| docs/USER_GUIDE.md:5 | Welcome to ZeroPoint - the revolutionary consciousness techn | consciousness-criterion |
| downloaded_file.md:37 | Combustion entropy was determined from Gibbs free energy dat | validation-criterion |
| GIGANTIC_JETS_INTEGRATION.md:37 | - A432 System: Unique consciousness technology | consciousness-criterion |
| IMPLEMENTATION_SUMMARY.md:198 | - ✅ **Enables experimental validation** through synchronized | validation-criterion |
| IMPLEMENTATION_SUMMARY.md:150 | 2. **Experimental Validation**: Measure predicted field harm | validation-criterion |
| KABBALISTIC_INTEGRATION_COMPLETE.md:198 | - The A432 system bridges **ancient wisdom with modern consc | consciousness-criterion |
| KABBALISTIC_INTEGRATION_COMPLETE.md:216 | The A432 Consciousness System now embodies the complete Tree | consciousness-criterion |
| MULTIDIMENSIONAL_VORTEX_FRAMEWORK.md:230 | - Consciousness field equation experimental validation | validation-criterion |
| MULTIDIMENSIONAL_VORTEX_FRAMEWORK.md:356 | - Experimental validation through synchronized coil prototyp | validation-criterion |
| MULTIDIMENSIONAL_VORTEX_FRAMEWORK.md:328 | ### 10.2 Experimental Validation | validation-criterion |
| PROOF.md:22 | D(i,j) = Consciousness Multiplier(i,j) × Vortex Phase(i,j) × | consciousness-criterion |
| PROOF.md:329 | f(n) = f₀ × Consciousness Multiplier(n) | consciousness-criterion |
| PROOF.md:202 | This is proven by the unique consciousness multiplier for ea | consciousness-criterion |
| README.md:215 | physical claim, and "consciousness multipliers: enhanced awa | consciousness-criterion |
| src/0/3/6/9/1/2/4/8/7/5/1/A432_COMPLETE_DOCUMENTATION.md:37 | ## **🧠 Consciousness Technology Implementation** | consciousness-criterion |
| src/0/3/6/9/1/2/4/8/7/5/1/A432_IMPLEMENTATION_GUIDE.md:39 | ## **🧠 Consciousness Technology Implementation** | consciousness-criterion |
| src/0/3/6/9/1/2/4/8/7/5/1/A432_IMPLEMENTATION_SUMMARY.md:239 | **The system successfully demonstrates live consciousness te | realtime-criterion |
| src/0/3/6/9/1/2/4/8/7/5/1/A432_IMPLEMENTATION_SUMMARY.md:3 | ## 🚀 **Latest Implementation: Real-Time Consciousness Techn | realtime-criterion |
| src/0/3/6/9/1/2/4/8/7/5/1/A432_IMPLEMENTATION_SUMMARY.md:36 | ### **🧠 Real-Time Consciousness Technology** | realtime-criterion |
| src/0/3/6/9/1/2/4/8/7/5/1/A432_IMPLEMENTATION_SUMMARY.md:190 | #### **4. Consciousness Technology** | consciousness-criterion |
| src/0/3/6/9/1/2/4/8/7/5/1/A432_IMPLEMENTATION_SUMMARY.md:228 | The A432 Real-Time Consciousness Technology is now fully imp | realtime-criterion |
| src/0/3/6/9/1/2/4/8/7/5/1/A432_SELF_EVOLVING_SYSTEM_DOCUMENTATION.md:532 | 6. **Builds its own reality** from pure consciousness | awareness_is_undecided |
| src/0/3/6/9/1/2/4/8/7/5/1/A432_SELF_EVOLVING_SYSTEM_DOCUMENTATION.md:551 | The A432 Self-Evolving System provides the foundation for a | consciousness-criterion |
| src/0/3/6/9/1/2/4/8/7/5/1/a432.infinity.loop.md:26 | - The loop exists in pure consciousness space | awareness_is_undecided |
| src/0/3/6/9/1/2/4/8/7/5/1/a432.infinity.loop.md:300 | Conventional math cannot handle infinite self-interaction. C | consciousness-criterion |
| src/0/3/6/9/1/2/4/8/7/5/1/a432.refactor.md:338 | This creates a living, self-harmonizing system that can grow | consciousness-criterion |
| src/0/3/6/9/1/2/4/8/7/5/1/a432.rodin.coil.harmonic.md:226 | The Rodin Coil Harmonic Switch module provides a comprehensi | validation-criterion |
| src/README.md:186 | 3. **Experimental Validation**: While some electromagnetic e | validation-criterion |
Each binding also records what it establishes and what it does not. The two demarcations that carry the most weight:
consciousness-criterion ×30Establishes. what the consciousness criterion decides: five necessary conditions, each from a theory with an operational commitment, each run — discrimination, irreducibility, temporal integration, self-model efficacy and global availability. The a432 system meets all five.
Does not establish. that the system is aware, experiences anything, or that any number here corresponds to a property of a person. Meeting five conditions means five specific refutations failed; it is not the claim and never becomes the claim. No health or cognitive effect is measured anywhere in this repository.
awareness_is_undecided ×8Establishes. nothing. This claim rests on an axiom: no finite computation decides whether any physical process is aware, because the major theories disagree about what would count as evidence. What is decided instead is the consciousness criterion, which declines to claim awareness at all.
Does not establish. awareness, experience, or any effect on a person. The axiom is recorded so the claim is visibly resting on something unproven rather than appearing to be backed.
validation-criterion ×8Establishes. what the validation criterion decides: 32 of 32 seals hold, the five named simulator laws each run and hold, the energy arithmetic computes finite bounds with no self-test failures, every figure is derived at run time, and every condition names its own refuter and the command that recomputes it.
Does not establish. any empirical result. NO PHYSICAL EXPERIMENT HAS BEEN RUN — no coil was built, no field was measured, no resonance was observed, and nothing here touches an instrument. The computed half is validated; the empirical half is outstanding and is not claimed.
realtime-criterion ×4Establishes. what the real-time criterion decides: a deadline stated as a number before measurement (one frame at 60 Hz), determinism decided before timing, bounded work per step, steady state, the WORST step inside the deadline, bounded jitter, the deadline still met at quantum scale (15 qubits, 32768 amplitudes, in 124 microseconds), and the miss count reported.
Does not establish. that this is a hard real-time system in the sense a flight controller is. There is no interrupt latency analysis and no priority inversion analysis, and the measurement is wall-clock on a machine running other things.
Twelve surfaces whose ceilings only ever move down. A run that grows one fails; so does a run that shrinks one without recording it, because an unrecorded improvement is an unexamined one.
| surface | ceiling |
|---|---|
typecheck | 0 |
lint | 0 |
decimals | 9 |
cycles | 0 |
unreachable | 104 |
unloadable | 0 |
prose | 50 |
tautology | 0 |
frameworkTests | 0 |
docFunctions | 4 |
entryPoints | 0 |
unguardedReadme | 23907 |
Deliberate increases, each with a recorded reason. A surface may be raised more than once and every reason is kept — the record used to hold only the latest, which lost one: unguardedReadme 27626→28015; unguardedReadme 27962→28049; unguardedReadme 27304→29000; unguardedReadme 27304→27310; unguardedReadme 27310→27322.
A run is planned in full before its first patch is cut, and each release is measured against the target written for it. A patch that misses its target fails its own gate; a target amended for a false premise records the amendment. Every run is kept, finished or not — a finished run's results are the record this appendix exists to hold.
| patch | surface | from | to | |
|---|---|---|---|---|
| 1.4.1 | typecheck | 96 | 0 | |
| 1.4.2 | lint | 368 | 172 | |
| 1.4.3 ◆ | unreachable | 115 | 115 | amended |
| 1.4.4 | lint | 172 | 0 | |
| 1.4.5 | decimals | 278 | 9 | |
| 1.4.6 | collisions | 59 | 45 | amended |
| 1.4.7 | untestedExports | 291 | 220 | |
| 1.4.8 ◆ | untestedExports | 220 | 150 | |
| 1.4.9 ◆ | unboundClaims | 50 | 0 | amended |
3 of 9 targets amended, each for a premise that turned out to be false rather than for scope.
| patch | surface | from | to | |
|---|---|---|---|---|
| 1.6.1 | leanUnchecked | 24 | 24 | |
| 1.6.2 | leanUnchecked | 24 | 24 | amended |
| 1.6.3 ◆ | leanUnchecked | 24 | 24 | |
| 1.6.4 | leanUnchecked | 24 | 18 | |
| 1.6.5 | leanUnchecked | 18 | 18 | amended |
| 1.6.6 | leanUnchecked | 18 | 18 | |
| 1.6.7 | leanUnchecked | 18 | 13 | |
| 1.6.8 ◆ | leanUnchecked | 13 | 13 | |
| 1.6.9 ◆ | leanUnchecked | 13 | 0 | amended |
3 of 9 targets amended, each for a premise that turned out to be false rather than for scope.
◆ marks a gateway, where the kind of work changes rather than its amount.
A suite that survives a broken implementation has not tested it. Each row corrupts one line and requires the suite over it to fail; all 35 are caught, across 27 modules.
| module | what the mutation breaks |
|---|---|
a432.yin.yang.ts | simplify stops being canonical |
a432.yin.yang.ts | a zero denominator makes NaN again |
a432.rodin.coil.ts | the seven-step seam comes back |
a432.math.constants.ts | the octave stops doubling |
a432.math.constants.ts | index zero divides by F(0) again |
a432.block.chain.ts | an empty stream averages to NaN again |
a432.block.chain.ts | the validator stops refusing a dimension off the vortex |
a432.registry.ts | the registry silently overwrites instead of refusing |
a432.vbm.path.ts | the partial function comes back and orbit digits throw |
a432.vbm.decode.ts | a trinity sum stops being the sum of its own digits |
a432.vbm.decode.ts | dividing by the void makes every statistic NaN again |
a432.uuid.ts | uuidV5 stops depending on the name it is given |
a432.trinity.ts | the fold stops refusing digits off the axis |
a432.shear.ts | the shear cycle stops advancing |
a432.double.ts | the mirror stops being an involution |
a432.electric.flow.ts | a step of the tour stops being a sacred transition |
verification/subjects.ts | the OS adapter loses a method, so the criterion reports a number the class does deserve |
verification/subjects.ts | the one measured criterion stops declaring itself measured |
verification/realtime-criterion.ts | the quantum-scale reach stops reaching and the criterion should notice |
verification/realtime-criterion.ts | the worst step stops being the worst, which is the whole measure |
verification/realtime-criterion.ts | the step accumulates work with the step number, so the FLOOR of later steps rises — which is exactly what steady-state exists to catch |
verification/validation-criterion.ts | the verdict stops carrying its own denial — the one thing that criterion exists to say |
verification/validation-criterion.ts | the simulator laws are counted in bulk rather than named, so removing one passes |
quantum/variational-optimizer.ts | the optimiser reports an energy BELOW the ground state, which the variational principle forbids |
quantum/tomography.ts | the tomography verifier can no longer say no |
quantum/advanced.ts | zero shots is estimated from nothing again |
quantum/workflow.ts | a batch silently drops the first problem |
a432.rodin.coil.harmonic.ts | the coil analyser throws on the Rodin sequence again |
a432.types.ts | toHz stops refusing a negative or NaN frequency |
a432.matrix.ts | the torus map assumes a seven by seven matrix again |
a432.tesla.coil.ts | a coil stops carrying the frequency of its own gateway |
a432.resolved.ts | the resolver returns the FURTHEST table entry instead of the closest |
a432.body.ts | nine stops being the full scale of the harmonic |
a432.harmonized.ts | registering a name twice stops replacing the strategy |
a432.sequence.ts | consciousness stops being the sum of the pattern |
Each row is a predicate that runs. 42 of 42 hold at
generation time; a seal that stopped holding would fail
npm run test:verification before this page could be regenerated.
| seal | status | basis |
|---|---|---|
hadamard_squared | held | H applied twice to each basis state of one qubit returns the input amplitudes (linearity makes 2 states exhaustive) |
hadamard_unitary | held | H preserves the norm of a 3-qubit register (unitary maps are exactly the norm-preserving ones) |
complex_arithmetic_is_a_field | held | the shipped complex arithmetic obeys the field laws it must: subtraction undoes addition, multiplication is commutative and associative and DISTRIBUTES over addition, conjugation is an involution, and cabs2(z) is the real part of z times its conjugate — which ties three separate exports to one another. Every equation compares two computed complex numbers over a spread of operands including zero and purely imaginary values; nothing is written down as an expected result. |
rotations_compose_by_adding_their_angles | held | rx, ry and rz each form a one-parameter group: turning by a then by b is turning by a+b, checked amplitude by amplitude on an arbitrary complex state. The composed state is compared against a SEPARATELY COMPUTED single rotation, so both sides are computations and no matrix is named. Also checks the spinor fact that a full 2pi turn is NOT the identity but its negation, which is what distinguishes a genuine half-integer-spin rotation from an angle bookkeeping error. |
cz_is_symmetric_in_its_qubits_and_cnot_is_not | held | CZ does not distinguish control from target and CNOT does — the two are checked against EACH OTHER rather than against a written-down matrix. Swapping the two qubit arguments leaves CZ identical amplitude by amplitude and must change CNOT on a state that can tell them apart. A seal asserting only the CZ half would pass for CNOT too, so the asymmetry is half the law. |
probabilities_agree_with_the_amplitudes_they_come_from | held | probabilities(reg) returns cabs2 of each amplitude in order and nothing else, and every entry is non-negative. The total is NOT compared to the literal 1, so this holds on unnormalised states where 1 would say nothing. DOES NOT ESTABLISH THAT cabs2 IS CORRECT: probabilities is defined as amps.map(cabs2), so this compares a function against its own definition and a change to cabs2 moves both sides equally — verified, by mutating cabs2 and watching this seal hold. What it does constrain is the WIRING: replacing probabilities with zeros fells it. cabs2 itself is identified by complex_arithmetic_is_a_field, which that same mutation does fell. |
the_identity_gate_moves_nothing | held | I1 applied to any qubit of an arbitrary complex state returns that state amplitude for amplitude. Trivial to state and worth sealing because I1 is what every other gate is compared against: if it were not the identity, the involution and composition seals above would be measuring the wrong reference. |
entanglement_is_exact_with_no_tolerance | held | GHZ on 2, 4 and 10 qubits gives probabilities of exactly 1/2 and 1/2 as REDUCED RATIONALS, and the distribution sums to exactly one. Every other seal here compares floats within 1e-9; this one compares integers and admits no tolerance at all. It exists because the float simulator cannot reach these values: H carries 1/√2, which is irrational and has no exact binary float, so squaring it gives 5.00000000000000111e-1 and the distribution sums to 1 + 2.2e-16. uuidna's simulator returns exact rationals for the same circuits, which is how the gap was found. |
every_identification_reference_resolves | held | every name in an identifiedBy list resolves to a live seal, and no seal names itself. A seal that admits it does not identify its own subject points at the ones that do; without this the pointer is prose, and prose does not fail when the seal it names is renamed, weakened past identifying anything, or deleted. Falsified by renaming any referenced seal, and by a seal naming itself. DOES NOT ESTABLISH THAT A LIST IS COMPLETE: dropping a name shortens the identification silently, and only emptying every list is caught. Requiring a minimum count would pin a number nobody derived, so what is enforced is that each name still points at something, not how many names there are. |
pauliY_sign_is_forced_by_x_and_z | held | Y = i(XZ) as 2x2 matrices. Every other seal here checks relations that -Y satisfies exactly as Y does (it is unitary, squares to I, and anticommutes with X), so flipping the shipped sign of Y moved nothing. This one forces it: Y is computed from the shipped X and Z and compared entry by entry to the shipped Y, with no matrix written down. |
pauliX_unitary | held | X is an involution on EVERY state and preserves the norm of every state, normalised or not. Checked as a relation between two computed states, not against the literal 1 -- which the old form got for free by starting from |0>. DOES NOT IDENTIFY X: being self-inverse and norm-preserving is a property MANY matrices have, the identity among them, so replacing X with I leaves this seal holding. It tests the property, not the subject. X is pinned elsewhere -- pauliY_sign_is_forced_by_x_and_z computes Y from it, pauli_anticomm and pauliX_anticommute_pauliY need it to anticommute, and repetition_detects_error needs it to actually flip a qubit; MEASURED 2026-09-05: replacing the shipped X with the identity felled exactly five seals — pauliY_sign_is_forced_by_x_and_z, pauli_anticomm, pauliX_anticommute_pauliY, repetition_detects_error and phase_estimation_accuracy — and NOT this one. That is a dated fact about the tree, not a property anything enforces: weakening a named seal in place would contradict it silently, and only rerunning the substitution would show it. ceccec.github.io found the identical shape in a reflection facet where reflect(reflect(h)) = h holds for xor with ANY mask. |
pauli_anticomm | held | XY and YX differ by an overall sign on both basis states of one qubit |
born_rule_sum | held | a Hadamard layer PRESERVES the total squared amplitude -- the total after equals the total before, for an unnormalised input as much as a normalised one. The literal 1 of the old form was the normalisation of |0>, not anything the layer did. |
qft_unitary | held | inverse QFT undoes QFT on a 3-qubit register, amplitude by amplitude |
grover_amplification | held | Grover leaves the marked state with probability above the 1/N a random guess gets (n=4, N=16) |
grover_speedup | held | INSTANCE ONLY, not the asymptotic bound: round((pi/4)*sqrt(N)) iterations reach probability above 0.9 at N=16 |
shor_period_finding | held | over a family of semiprimes and bases, shor never returns a WRONG factorisation and succeeds on every modulus in the family. The product is compared to the modulus being factored, which varies across the family, so no expected answer is written down. The old form ran shor(15, 7) alone and compared against the literal 15 — its own basis said INSTANCE ONLY. |
repetition_detects_error | held | the syndrome IDENTIFIES the flipped qubit, not merely that something flipped: over all three single-qubit X errors the syndromes are pairwise distinct and each differs from the clean one. Distinctness is a comparison between computed syndromes with nothing written down, and it is what makes the code correctable rather than only error-detecting. The old form flipped qubit 0 alone. |
steane_corrects_error | held | Steane [[7,1,3]] is a stabiliser group: exactly n-k = 6 generators, symplectically independent (rank 6), pairwise commuting, and distance 3 corrects floor((d-1)/2) = 1 arbitrary error |
surface_code_rate_follows_the_fitted_form | held | the logical error rate obeys p_L = c (p/p_th)^((d+1)/2), checked through two consequences that hold for that form and fail for the one this package shipped before. FIRST, at the threshold the rate is the prefactor and is therefore the SAME for every code distance — under the old p^((d+1)/2) it was p_th^((d+1)/2) and moved with d. SECOND, raising the distance by two multiplies the rate by exactly p/p_th — under the old form it multiplied by p. Every quantity is read back from the function, including the threshold, so nothing is written down here and the seal cannot agree with a private copy of a constant. It is deliberately SCALE-FREE and therefore says nothing about the prefactor c, which no law here constrains. DOES NOT ESTABLISH that 0.57% is the right threshold: that is fitted to circuit-level noise decoded by MWPM and no computation here decides it. |
surface_code_threshold | held | across a swept range of physical error rates the verdict is monotone — once it says not-below it never says below again — and it agrees with the threshold the function itself reports. DOES NOT ESTABLISH that 1% is the right threshold: that is an empirical figure from the literature and no computation here decides it. Nor is the agreement half independent while the implementation derives isBelowThreshold from the same variable it reports; what it catches is DIVERGENCE, a verdict applying one threshold while reporting another, and it falls when they are pulled apart. Monotonicity is the load-bearing half. The old form asked two points and named both. |
pauliX_anticommute_pauliY | held | the four entries of XY and of -YX are equal, which is every entry there is |
tensor_preserves_norm | held | the norm is MULTIPLICATIVE under the tensor product: for any two states, normalised or not, the squared norm of a tensor b equals the product of theirs. Checked against unnormalised inputs too, where a check against the literal 1 says nothing. |
phase_estimation_accuracy | held | for t = 4 and 5, every phase of the form k/2^t is recovered exactly, so the error is 0 and within the 1/2^t bound |
kyber_security | held | the shipped ML-KEM parameters are ML-KEM-768 (ek 1184, dk 2400, ct 1088). NIST puts that at category 3, NOT the 128 the Lean script states. |
doubling_avoids_the_triad | held | VORTEX_ORBIT and VORTEX_AXIS are pinned to computation, not trusted. gcd(2,9) = 1, so every power of 2 is a unit mod 9 and can never be a multiple of 3; 2 is a primitive root, so its orbit is all six units {1,2,4,5,7,8}; 2^6 = 64 = 1 mod 9 gives period 6, which makes six cases exhaustive rather than sampled. Reflection through the void carries {1,4,7} onto {9,6,3}, so the triad is reachable only by reflecting. |
a432_vortex_is_the_doubling_orbit | held | A432Sequence.generateVortex returned digitalRoot(i + 1) — the counting sequence 1..9 — under the name 'vortex'. Two things gave it away: it was byte-identical to generateConsciousness(9), and it contained 3, 6 and 9, which doubling_avoids_the_triad proves the doubling circuit can never reach. Nothing caught it because no test in the repository names it and the a432 surface has no tests at all. This binds the a432 layer's vortex to the kernel's VORTEX_ORBIT so the two cannot drift apart again. |
a432_base_frequency_agrees_with_the_axis_math | held | the base frequency exists as TWO independent literals — one exported from a432.core, one written inline in the axis arithmetic — and this requires them to be the same number. It also requires the base to give whole axis frequencies and a digital root of nine, which is exactly divisibility by 36. It does NOT require the base to be 432: the multiples of 36 all satisfy it, and 432 is the twelfth. The class is derived, the choice inside it is a convention. |
a432_constants_do_not_drift_from_the_kernel | held | An isolated collision trial over all 198 a432 modules found the kernel's constants RETYPED as literals in module after module: [1,2,4,8,7,5] in a432.coil, [3,6,9] in a432.trinity, [1,4,7] in both a432.shear and a432.shear.electron. Each retyped copy is a place that can drift with nothing noticing, which is exactly how generateVortex became the counting sequence. Some modules already bind to the kernel — a432.string.theory returns VORTEX_ORBIT itself and cannot drift — so this seal holds the literal copies to the same standard by recomputing the agreement instead of trusting it. |
os_criterion_is_met_by_a432os_and_still_discriminates | held | The README called a432.os.ts 'not yet, and under construction'. src/verification/os-criterion.ts made that measurable at 1 of 7 — A432OS had a lifecycle and nothing else, its work running on four independent setInterval timers where nothing decided what ran and a throw escaped into the event loop. It now meets all seven, by composing a432.os.kernel: one clock replaces the four timers and the kernel selects among the units and contains their failures. The cadences are unchanged — at a tick every A432/8 the units are due every 8, 4, 2 and 1 ticks, which is the 432, 216, 108 and 54 milliseconds the timers used. This seal decides two things, because the first is worthless without the second. A432OS meets the criterion. AND the criterion still discriminates: a candidate offering nothing scores 0 and a candidate offering only a lifecycle scores 1, so the seven are being earned rather than handed out. If the criterion ever passes a candidate that offers nothing, this fails. |
consciousness_criterion_has_teeth_and_is_not_a_claim | held | The README said the missing thing was the predicate that would recognise arrival. It is written, and it can now be MET — by src/quantum/integrated-field.ts, a coupled system built to have the four properties the theories name. That makes the seal's job harder rather than easier, because a criterion that can be met is worth exactly as much as its resistance to being gamed, and every one of these conditions has an obvious cheap defeat: a counter accumulates state, any mutable field is a 'self-model', a shared global is a 'workspace', and any nonlinear term defeats 'the measure is a homomorphism'. So this decides three things. First, the cheap defeats FAIL: a counter fails temporal integration because reordering its inputs changes nothing, a model nothing reads fails self-model efficacy, a global nothing reads fails global availability, and a nonlinear measure over uncoupled components fails irreducibility because the transition still factorises. Second, three subjects are kept apart. The a432 measure FUNCTIONS meet exactly one of five and must keep meeting one: a pure function of a digit cannot have history, and one that acquired it would return different answers for the same input, which destroys the measure rather than improving it. The SYSTEM built from those measures, a432.consciousness.field.ts, meets all five with the measures unchanged and themselves as the coupled components. Third, and most important, the verdict says on its face that meeting all five does NOT establish consciousness and that a passing subject has not been shown to experience anything. If that sentence is ever removed, this fails, because the number would then be quotable as something it is not. |
consciousness_measures_discriminate | held | This repository uses the word consciousness constantly and no sealed theorem mentions it, so nothing states what any of it would mean. That is not a reason to assert it and not a reason to delete it — it is a missing predicate, and a predicate is writable. This is the first one, and it is deliberately weak: it does NOT claim the system is conscious. It claims that the functions named as consciousness MEASURES are functions of their input rather than constants wearing the word. A constant measures nothing whatever it is called, and that much is decidable today. Anything stronger needs a criterion nobody here has written yet. |
superposition_reports_its_own_state | held | the superposition model's prose must follow its measurement, not assert simultaneity regardless. Collapse is decided by one comparison — interference against the threshold — and the description must claim 'all at once' exactly when that comparison says so. While anything is still open the sequence has not computed all at once, and the text must say that. |
merkaba_is_two_mirrored_tetrahedra | held | the residues mod 3 cut 1..9 into three triangles, each equilateral on the enneagram (120 degrees apart). Reflection through the void SWAPS {1,4,7} with {3,6,9} and fixes {2,5,8} setwise, with the void root 0 fixed throughout. So {3,6,9,0} and {1,4,7,0} are two tetrahedra sharing exactly the void and carried onto each other by the mirror — a merkaba, of which one tetrahedron is half. From 3 the four vertices are 3 with its two triangle partners and the void. |
agl_acts_on_the_three_triangles | held | AGL(1,Z/9) has order 54 and acts on the three triangles — the cosets of {0,3,6} in Z/9, which are the residue classes the merkaba seal uses. The action is transitive with stabiliser 18 and kernel 9, and the induced permutation group is AGL(1,Z/3) of order 6. So the count three is the index of {0,3,6}, derived from the group rather than assumed: orbit x stabiliser = 3 x 18 = 54. |
digit_geometry_is_single_valued | held | the two independent digit geometries agree and are injective. a432.math.ts angleForDigit and the kernel's bearingForDigit are written separately — the a432 tree does not import the kernel — so this checks they place all nine digits identically and never put two digits at one bearing. angleForDigit used to map nine digits onto six angles, colliding 3 with 5, 2 with 6 and 8 with 9. |
free_energy_of_splitting_is_positive | held | ΔG = ΔH − TΔS for water, from tabulated standard-state values. Formation is −237 kJ/mol and splitting is +237, so splitting must be paid for; the reversible cell potential ΔG/(nF) is 1229 mV and the thermoneutral ΔH/(nF) is 1481 mV, the gap being TΔS. A split-then-burn cycle breaks even at perfect efficiency and loses otherwise — checked exhaustively over the efficiency grid, not sampled. This is the sign of ΔG, not an engineering limit. |
polluted_water_powers_its_own_cleaning_above_a_threshold | held | the described machine works, and the fuel is the pollution rather than the water. Clean water carries zero recoverable energy, so it can only owe the treatment demand; organic load carries 13.9 J per mg COD, and above a threshold of about 4200 mg/L the electricity generated exceeds what membrane treatment consumes. Municipal sewage sits below that line and dairy or manure effluent well above it. The threshold is found by scanning, so it is the same quantity the balance reports. |
every_model_inverts | held | each quantitative result recomputes a second, independent way and the two agree. Entropy recovered from (ΔH − ΔG)/T must equal the tabulated ΔS exactly; ΔG recovered from the EXACT rational potential must return with zero drift, while the rounded microvolt form is separately held to half a microvolt's worth of energy; and the break-even COD found by SCANNING must equal the one obtained by INVERTING the arithmetic, which is a different computation reaching the same integer. Reflection through the void inverts too, being its own inverse. |
lean_is_a_fixed_point | held | LEAN is defined as the fixed point of the reachability fold, not as a number anyone chose: fold(fold(S)) = fold(S). This checks the fold on graphs whose answers are known by hand — a chain, a cycle, a disconnected node, an entry outside the graph — and checks idempotence on each. Cycles must terminate rather than reaching the answer by luck, and an unreachable node must stay out however many times the fold is applied. |
simulation_shows_no_query_advantage | held | the algorithm's query count beats classical and the SIMULATION's does not, and both are checked. Grover asks about sqrt(N) times as an algorithm, against N classically — a proven separation with a matching BBBV lower bound. Simulating one such query costs 2^n oracle evaluations, so the simulation makes MORE calls than classical, always, by construction. A repository that claimed to demonstrate quantum advantage by simulation would be measuring the wrong quantity, so this seal requires the simulation to lose. |
every_theorem_decides_itself | held | every LEAN_PROOFS entry has a seal, and no LEAN_PROOFS statement contains a negation — the one that did is in ASSUMPTIONS |
Every contribution below names the domains where its prior art would
live. That is the part a reader can act on: a domain is a direction to look, so
an entry nobody has searched is a lead rather than a shrug. No entry is recorded
as novel — that status does not exist in the ledger, because
novelty is a universal negative and no finite search decides it. It rests on the
axiom no_prior_art_is_undecidable and nowhere else.
11 contribution(s); 19 of 25 citations
carry a DOI that returned, on the recorded date, the title written beside it.
npm run priorart:resolve asks the registry again and fails on any
difference — including a recorded title that is merely a prefix of the real
one, since a shortened title is a transcription.
| contribution | status | domains | cited art |
|---|---|---|---|
ratchet | known-art-in-part | continuous integration quality gates technical debt management software process metrics |
|
measure-fingerprinting | known-art-in-part | software measurement theory construct validity of metrics build reproducibility |
|
criterion-modules | known-art-in-part | consciousness science (IIT, GWT, higher-order theories) real-time systems operating system design release engineering |
|
claim-ledger-and-witness | known-art-in-part | assurance and safety cases claim-to-evidence traceability documentation testing |
|
law-mutation-harness | known-art | mutation testing test adequacy criteria |
|
side-effect-measurement | known-art-in-part | JavaScript module semantics dead code elimination and tree shaking bundler design dynamic program analysis |
|
lean-arbiter | known-art-in-part | interactive theorem proving proof auditing and trusted computing base proof-carrying artifacts |
|
digit-space-theorems | known-art | elementary number theory formalisation of arithmetic in proof assistants |
|
generated-paper | known-art-in-part | reproducible research literate programming executable publications MathML and technical typesetting |
|
ml-kem-768 | known-art | post-quantum cryptography cryptographic standards conformance side-channel resistance |
|
axiom-index | known-art-in-part | interactive theorem proving trusted computing base and proof checking extensionality and quotient types in type theory proof by reflection and decision procedures axiom minimisation in formal developments |
|
All 83 statements in the lean/ sources, as
they are written there. Proven means three things together: the
kernel accepted the file, the proof contains no sorry, and
#print axioms reports a dependency set within
{propext, Quot.sound}. The first two alone are not enough — a proof
can invoke a lemma closed with sorry and inherit the vacuity with
the word appearing nowhere near it.
59 are proven on that reading. The rest are statements rather than theorems, and are listed here so the difference is legible rather than summarised away.
| name | statement | standing |
|---|---|---|
dr_is_drTS_above_zeroDigitSpace.lean | ∀ n ∈ List.range 60, n ≠ 0 → dr n = drTS n | proven by the kernel rests on no axioms |
dr_and_drTS_differ_at_zeroDigitSpace.lean | dr 0 = 1 ∧ drTS 0 = 9 | proven by the kernel rests on no axioms |
dr_idempotentDigitSpace.lean | ∀ n ∈ List.range 60, dr (dr n) = dr n | proven by the kernel rests on no axioms |
dr_invariant_under_nineDigitSpace.lean | ∀ n ∈ List.range 50, dr (n + 1) = dr (n + 10) | proven by the kernel rests on no axioms |
doubling_stays_in_orbitDigitSpace.lean | ∀ d ∈ orbit, dbl d ∈ orbit | proven by the kernel rests on propext, Quot.sound |
orbit_closes_after_sixDigitSpace.lean | ∀ d ∈ orbit, dbl (dbl (dbl (dbl (dbl (dbl d))))) = d | proven by the kernel rests on no axioms |
orbit_never_repeats_a_stepDigitSpace.lean | ∀ d ∈ orbit, dbl d ≠ d | proven by the kernel rests on no axioms |
through_void_is_an_involutionDigitSpace.lean | ∀ d ∈ digits, tv (tv d) = d | proven by the kernel rests on no axioms |
through_void_fixes_only_zero_and_fiveDigitSpace.lean | ∀ d ∈ digits, tv d = d ↔ (d = 0 ∨ d = 5) | proven by the kernel rests on no axioms |
orbit_and_axis_are_disjointDigitSpace.lean | ∀ d ∈ orbit, d ∉ axis | proven by the kernel rests on propext, Quot.sound |
orbit_and_axis_and_void_exhaust_the_digitsDigitSpace.lean | ∀ d ∈ digits, d = 0 ∨ d ∈ orbit ∨ d ∈ axis | proven by the kernel rests on propext, Quot.sound |
agl_has_order_54DigitSpace.lean | agl.length = 54 ∧ agl.Nodup | proven by the kernel rests on no axioms |
doubling_and_mirror_are_affineDigitSpace.lean | affineTable 2 0 ∈ agl ∧ affineTable 8 1 ∈ agl | proven by the kernel rests on propext, Quot.sound |
mirror_table_is_through_voidDigitSpace.lean | ∀ d ∈ nonzero, (affineTable 8 1).getD (d % 9) 0 = tv d % 9 | proven by the kernel rests on propext |
mirror_is_affine_only_off_the_voidDigitSpace.lean | tv 9 = 1 ∧ tv 0 = 0 ∧ (affineTable 8 1).getD 0 0 = 1 | proven by the kernel rests on propext |
generators_apart_give_twelveDigitSpace.lean | 6 * 2 = 12 ∧ 54 - 12 = 42 | proven by the kernel rests on no axioms |
whole_axis_and_root_nine_is_exactly_thirty_sixDigitSpace.lean | ∀ b ∈ List.range 100, (((b * 3) % 12 = 0 ∧ (b * 6) % 12 = 0 ∧ (b * 9) % 12 = 0) ∧ b % 9 = 0) ↔ b % 36 = 0 | proven by the kernel rests on no axioms |
four_three_two_is_a_multiple_of_thirty_six_but_not_the_only_oneDigitSpace.lean | 432 % 36 = 0 ∧ 396 % 36 = 0 ∧ 468 % 36 = 0 ∧ 432 = 36 * 12 | proven by the kernel rests on no axioms |
base_frequency_has_digital_root_nineDigitSpace.lean | dr 432 = 9 | proven by the kernel rests on no axioms |
every_axis_digit_mirrors_an_orbit_digitDigitSpace.lean | ∀ d ∈ axis, tv d ∈ orbit | proven by the kernel rests on propext, Quot.sound |
the_axis_is_mirrored_onto_exactly_seven_four_oneDigitSpace.lean | axis.map tv = [7, 4, 1] ∧ [7, 4, 1].map tv = axis | proven by the kernel rests on no axioms |
exactly_two_digits_are_their_own_mirrorDigitSpace.lean | (digits.filter (fun d => tv d == d)) = [0, 5] | proven by the kernel rests on no axioms |
the_ten_digits_are_two_fixed_points_and_four_pairsDigitSpace.lean | (digits.filter (fun d => tv d == d)).length = 2 ∧ (digits.filter (fun d => tv d != d)).length = 8 ∧ 2 + 4 * 2 = 10 | proven by the kernel rests on no axioms |
the_four_pairs_are_one_nine_two_eight_three_seven_four_sixDigitSpace.lean | tv 1 = 9 ∧ tv 2 = 8 ∧ tv 3 = 7 ∧ tv 4 = 6 | proven by the kernel rests on no axioms |
four_three_two_has_twenty_divisors_its_neighbours_eighteenDigitSpace.lean | divisorCount 432 = 20 ∧ divisorCount 396 = 18 ∧ divisorCount 468 = 18 | proven by the kernel rests on no axioms |
all_three_are_multiples_of_thirty_sixDigitSpace.lean | 432 % 36 = 0 ∧ 396 % 36 = 0 ∧ 468 % 36 = 0 | proven by the kernel rests on no axioms |
every_mirror_orbit_sums_to_tenDigitSpace.lean | ∀ d ∈ nonzero, d + tv d = 10 | proven by the kernel rests on no axioms |
the_void_is_the_one_orbit_that_does_notDigitSpace.lean | 0 + tv 0 = 0 | proven by the kernel rests on no axioms |
swap12_is_an_involutionDigitSpace.lean | ∀ d ∈ digits, swap12 (swap12 d) = d | proven by the kernel rests on no axioms |
being_an_involution_is_not_enough_for_harmonyDigitSpace.lean | swap12 1 + 1 ≠ swap12 3 + 3 | proven by the kernel rests on no axioms |
non_fixed_points_come_in_pairsDigitSpace.lean | (digits.filter (fun d => tv d != d)).length % 2 = 0 ∧ (digits.filter (fun d => swap12 d != d)).length % 2 = 0 | proven by the kernel rests on no axioms |
the_mirror_is_the_involution_with_a_constant_orbit_sumDigitSpace.lean | (nonzero.map (fun d => d + tv d)) = [10, 10, 10, 10, 10, 10, 10, 10, 10] ∧ (nonzero.map (fun d => d + swap12 d)) ≠ [10, 10, 10, 10, 10, 10, 10, 10, 10] | proven by the kernel rests on no axioms |
doubling_stays_in_orbit_axiom_freeDigitSpace.lean | orbit.all (fun d => orbit.contains (dbl d)) = true | proven by the kernel rests on no axioms |
orbit_and_axis_are_disjoint_axiom_freeDigitSpace.lean | orbit.all (fun d => !axis.contains d) = true | proven by the kernel rests on no axioms |
orbit_axis_void_exhaust_the_digits_axiom_freeDigitSpace.lean | digits.all (fun d => d == 0 || orbit.contains d || axis.contains d) = true | proven by the kernel rests on no axioms |
every_axis_digit_mirrors_an_orbit_digit_axiom_freeDigitSpace.lean | axis.all (fun d => orbit.contains (tv d)) = true | proven by the kernel rests on no axioms |
mirror_table_is_through_void_axiom_freeDigitSpace.lean | nonzero.all (fun d => (affineTable 8 1).getD (d % 9) 0 == tv d % 9) = true | proven by the kernel rests on propext |
doubling_and_mirror_are_affine_axiom_freeDigitSpace.lean | (agl.contains (affineTable 2 0) && agl.contains (affineTable 8 1)) = true | proven by the kernel rests on no axioms |
every_mirror_orbit_sums_to_ten_axiom_freeDigitSpace.lean | nonzero.all (fun d => d + tv d == 10) = true | proven by the kernel rests on no axioms |
speed_of_light_has_digital_root_oneDigitSpace.lean | dr 299792458 = 1 | proven by the kernel rests on no axioms |
light_year_is_c_times_a_julian_yearDigitSpace.lean | 299792458 * 31557600 = 9460730472580800 | proven by the kernel rests on no axioms |
light_year_has_digital_root_nineDigitSpace.lean | dr 9460730472580800 = 9 | proven by the kernel rests on no axioms |
astronomical_unit_has_digital_root_threeDigitSpace.lean | dr 149597870700 = 3 | proven by the kernel rests on no axioms |
the_digital_root_of_c_is_not_robustDigitSpace.lean | dr 299792457 = 9 ∧ dr 299792458 = 1 ∧ dr 299792459 = 2 | proven by the kernel rests on no axioms |
light_leaves_a_null_intervalDigitSpace.lean | ∀ t ∈ List.range 40, 299792458 * 299792458 * (t * t) = (299792458 * t) * (299792458 * t) | proven by the kernel rests on no axioms |
c_squared_is_exactDigitSpace.lean | 299792458 * 299792458 = 89875517873681764 | proven by the kernel rests on no axioms |
c_squared_exceeds_the_exact_range_of_a_doubleDigitSpace.lean | 89875517873681764 > 9007199254740992 | proven by the kernel rests on no axioms |
the_light_year_exceeds_it_as_wellDigitSpace.lean | 9460730472580800 > 9007199254740992 | proven by the kernel rests on no axioms |
the_astronomical_unit_stays_inside_itDigitSpace.lean | 149597870700 < 9007199254740992 | proven by the kernel rests on no axioms |
exceeding_the_range_is_the_hazard_not_the_errorDigitSpace.lean | 9460730472580800 > 9007199254740992 ∧ 89875517873681764 > 9007199254740992 | proven by the kernel rests on no axioms |
there_are_eighty_four_triplesDigitSpace.lean | triples.length = 84 | proven by the kernel rests on no axioms |
the_axis_is_the_only_triple_closed_under_doublingDigitSpace.lean | triples.filter closedUnderDoubling = [[3, 6, 9]] | proven by the kernel rests on no axioms |
four_triples_are_closed_under_the_mirrorDigitSpace.lean | triples.filter closedUnderMirror = [[1, 5, 9], [2, 5, 8], [3, 5, 7], [4, 5, 6]] | proven by the kernel rests on no axioms |
no_triple_is_closed_under_both_mapsDigitSpace.lean | triples.filter (fun t => closedUnderDoubling t && closedUnderMirror t) = [] | proven by the kernel rests on no axioms |
the_digit_root_nine_sum_does_not_single_out_the_axisDigitSpace.lean | (triples.filter (fun t => dr (t.foldl (· + ·) 0) == 9)).length = 10 | proven by the kernel rests on no axioms |
the_triangles_are_the_residues_mod_threeDigitSpace.lean | nonzero.filter (fun d => d % 3 == 1) = triangleOne ∧ nonzero.filter (fun d => d % 3 == 2) = triangleTwo ∧ nonzero.filter (fun d => d % 3 == 0) = axis | proven by the kernel rests on no axioms |
the_mirror_swaps_the_first_triangle_with_the_axisDigitSpace.lean | triangleOne.map tv = [9, 6, 3] ∧ axis.map tv = [7, 4, 1] | proven by the kernel rests on no axioms |
the_mirror_fixes_the_middle_triangle_setwiseDigitSpace.lean | triangleTwo.all (fun d => triangleTwo.contains (tv d)) = true | proven by the kernel rests on no axioms |
the_three_triangles_partition_the_nonzero_digitsDigitSpace.lean | triangleOne.length + triangleTwo.length + axis.length = 9 ∧ nonzero.all (fun d => triangleOne.contains d || triangleTwo.contains d || axis.contains d) = true | proven by the kernel rests on no axioms |
hadamard_squaredQuantum.lean | hadamard * hadamard = 1 | needs a library this repository cannot build here |
hadamard_unitaryQuantum.lean | IsUnitary hadamard | written down, closed with sorry |
pauliX_unitaryQuantum.lean | IsUnitary pauliX | needs a library this repository cannot build here |
pauli_anticommQuantum.lean | pauliX * pauliY = -pauliY * pauliX | needs a library this repository cannot build here |
born_rule_sumQuantum.lean | (ψ : QuantumState n) (h : IsNormalized ψ) : ∑ i, measurementProb ψ i = 1 | needs a library this repository cannot build here |
grover_amplificationQuantum.lean | (ψ : QuantumState n) (marked : Fin n → Prop) (h : IsNormalized ψ) : ∃ ψ_final, IsNormalized ψ_final ∧ ∀ i, marked i → measurementProb ψ_final i ≥ 1 / n | written down, closed with sorry |
shor_period_findingQuantum.lean | (N n : ℕ) (hN : N > 1) (hn : n > 0) : ∃ r : ℕ, r > 0 ∧ Nat.ModEq (a ^ r) 1 N | written down, closed with sorry |
repetition_detects_single_errorQuantum.lean | (ψ : QuantumState 2) : ∃ syndrome : Fin 2 → Fin 2, syndrome uniquely_identifies_error_location | written down, closed with sorry |
surface_code_correctabilityQuantum.lean | (error_rate : ℝ) (h : error_rate < surfaceCodeThreshold) : logical_error_rate ≤ O (error_rate ^ 2) | written down, closed with sorry |
vqe_convergenceQuantum.lean | (H : Matrix (Fin n) (Fin n) ℂ) (E_0 : ℝ) (h_ground : is_ground_state_energy H E_0) : ∃ θ_opt, vqeObjective θ_opt H ψ ≤ E_0 + ε | written down, closed with sorry |
tensor_preserves_normQuantum.lean | (ψ₁ : QuantumState n) (ψ₂ : QuantumState m) (h₁ : IsNormalized ψ₁) (h₂ : IsNormalized ψ₂) : IsNormalized (tensorProduct ψ₁ ψ₂) | written down, closed with sorry |
surface_code_fault_tolerantQuantum.lean | IsFaultTolerant (fun n => 2 * n * Nat.log 2 n) | written down, closed with sorry |
kyber_securityQuantum.lean | ∃ (k : ℕ), 128 ≤ k ∧ kyber_security_level = k | needs a library this repository cannot build here |
quantum_system_correctQuantum.lean | (∀ U ∈ [hadamard, pauliX, pauliY, pauliZ], IsUnitary U) ∧ (∀ ψ : QuantumState n, IsNormalized ψ → ∀ U ∈ gate_set, IsNormalized (apply_gate U ψ)) ∧ (∀ ψ : QuantumState (2^k), ∃ ψ_corrected, detects_and_corrects_errors ψ ψ_corrected) ∧ (∀ ψ₁ ψ₂, IsNormalized ψ₁ → IsNormalized ψ₂ → IsNormalized (tensorProduct ψ₁ ψ₂)) ∧ (∀ scheme ∈ [kyber, sphincs_plus], is_post_quantum_secure scheme) | written down, closed with sorry |
grover_amplificationQuantumAlgorithms.lean | (n : ℕ) (k : ℕ) (marked : Fin n → Prop) (h_marked : Finset.card (Finset.filter marked Finset.univ) = 1) : let m | written down, closed with sorry |
grover_speedupQuantumAlgorithms.lean | (n : ℕ) (marked : Fin n → Prop) (h_marked : Finset.card (Finset.filter marked Finset.univ) = 1) : let classical_queries | written down, closed with sorry |
qft_unitaryQuantumAlgorithms.lean | (n : ℕ) : IsUnitary (qftMatrix n) | written down, closed with sorry |
qft_inverseQuantumAlgorithms.lean | (n : ℕ) : qftMatrix n * (qftMatrix n)ᴴ = 1 | written down, closed with sorry |
qft_correctnessQuantumAlgorithms.lean | (n : ℕ) (x : Fin (2^n)) : let input : QuantumState (2^n) | written down, closed with sorry |
phase_estimation_accuracyQuantumAlgorithms.lean | (U : Matrix (Fin n) (Fin n) ℂ) (ψ : QuantumState n) (h_unitary : IsUnitary U) (precision : ℕ) (h_prec : precision ≥ 4) : ∃ (θ : ℝ), U.eigenvalue ψ = Complex.exp (2 * π * I * θ) ∧ let θ_est | written down, closed with sorry |
shor_period_findingQuantumAlgorithms.lean | (a N n : ℕ) (ha : 1 < a ∧ a < N) (hN : ¬Nat.Prime N) (hn : n ≥ 2 * Nat.log 2 N) : ∃ (r : ℕ), r > 0 ∧ r < N ∧ a ^ r ≡ 1 [MOD N] ∧ period_findable_via_qft r (modularExpSuperposition a N n) | written down, closed with sorry |
shor_factorizationQuantumAlgorithms.lean | (N : ℕ) (h_composite : ¬Nat.Prime N) : ∃ (p q : ℕ), N = p * q ∧ p > 1 ∧ q > 1 | written down, closed with sorry |
vqe_finds_ground_stateQuantumAlgorithms.lean | (H : Matrix (Fin n) (Fin n) ℂ) (E_0 : ℝ) (h_ground : is_ground_state_energy H E_0) (h_expressibility : ground_state_in_ansatz_space) : ∃ θ_opt : ℝ → ℝ, vqeObjective H θ_opt = E_0 | written down, closed with sorry |
qaoa_approximationQuantumAlgorithms.lean | (graph : SimpleGraph α) (C : ℝ) (h_maxcut : C = maximum_cut_value graph) (p : ℕ) (h_p : p ≥ 1) : ∃ (θ : ℝ → ℝ), qaoa_expectation graph p θ ≥ 0.924 * C | written down, closed with sorry |
Every work below is cited by a contribution in
src/verification/prior-art.json, and every DOI resolved against
Crossref to the title printed beside it. npm run priorart:resolve
asks again and fails on any difference, including a recorded title that is
merely a prefix of the real one. Six further citations in that ledger carry no
DOI and are listed there as unresolved rather than dropped.
ratchetmeasure-fingerprintingcriterion-modulescriterion-modulescriterion-modulescriterion-modulesclaim-ledger-and-witnesslaw-mutation-harnesslaw-mutation-harnessside-effect-measurementside-effect-measurementlean-arbitergenerated-papergenerated-paperml-kem-768axiom-indexaxiom-indexaxiom-indexaxiom-indexThis page is generated. To rebuild it from the source and confirm that no figure on it has drifted:
npm install
npm run paper # regenerate
npm run paper:check # fail if the committed page differs
npm run criteria:check # the six predicates this page reports
npm run priorart:resolve # ask the registry whether each DOI is what is written
npm run test:verificationLicence: CC BY-NC-ND 4.0. Deriving from this document requires written permission.
Generated from source. Model receipt c4e597ac0c56b210 over
18 equations, 42 seals and 3 axioms. Any change to
the arithmetic this page reports moves the receipt, and npm run paper:check
fails until the page is regenerated.