Theorem families
Generated by
npm run familiesfrom thedeflines oflean/*.leanandlean/ledger.json. A theorem's family is the set of defined objects its statement mentions — never a taxonomy typed here, because a hardcoded list of definitions once demoted a theorem to "literal arithmetic" for being newer than the list.
83 theorems across 4 files: 59 kernel-proven, 19 closed with sorry, 5 unverifiable here. 42 defined objects give 28 families, and a theorem may belong to more than one.
| family | theorems | proven | with sorry |
|---|---|---|---|
tv | 18 | 18 | 0 |
dr | 10 | 10 | 0 |
orbit | 10 | 10 | 0 |
axis | 10 | 10 | 0 |
digits | 8 | 8 | 0 |
nonzero | 7 | 7 | 0 |
affineTable | 5 | 5 | 0 |
triples | 5 | 5 | 0 |
dbl | 4 | 4 | 0 |
swap12 | 4 | 4 | 0 |
agl | 3 | 3 | 0 |
triangleOne | 3 | 3 | 0 |
triangleTwo | 3 | 3 | 0 |
hadamard | 3 | 0 | 2 |
IsUnitary | 3 | 0 | 2 |
pauliX | 3 | 0 | 1 |
drTS | 2 | 2 | 0 |
file: DigitSpace.lean | 2 | 2 | 0 |
closedUnderDoubling | 2 | 2 | 0 |
closedUnderMirror | 2 | 2 | 0 |
pauliY | 2 | 0 | 1 |
divisorCount | 1 | 1 | 0 |
IsFaultTolerant | 1 | 0 | 1 |
file: Quantum.lean | 1 | 0 | 0 |
QuantumState | 1 | 0 | 1 |
IsNormalized | 1 | 0 | 1 |
pauliZ | 1 | 0 | 1 |
tensorProduct | 1 | 0 | 1 |
| closed arithmetic | 9 | 9 | 0 |
| statement not parsed | 17 | 0 | 16 |
Closed arithmetic
Statements about numerals rather than about this theory's constructions — c², the light year, the exact integer range of a double. They mention no defined object and are a family for that reason, not a residue. These were once withheld from deposit on a syntactic test standing in for significance; six of them are the speed-of-light group, including the theorem that justifies this package's ban on decimal literals.
generators_apart_give_twelve— provenfour_three_two_is_a_multiple_of_thirty_six_but_not_the_only_one— provenall_three_are_multiples_of_thirty_six— provenlight_year_is_c_times_a_julian_year— provenc_squared_is_exact— provenc_squared_exceeds_the_exact_range_of_a_double— proventhe_light_year_exceeds_it_as_well— proventhe_astronomical_unit_stays_inside_it— provenexceeding_the_range_is_the_hazard_not_the_error— proven
Axioms
What a proof assumes about its SUBJECT is not what it assumes about its PROOF SYSTEM, and axiom-index keeps them apart. propext and Quot.sound are facts about Lean and say nothing about digits.
- kernelProven: 59
- withMeasuredAxioms: 59
- restingOnNothingAtAll: 51
- restingOnKernelAxiomsOnly: 8
Statement not parsed
The statement reader did not match 17 declarations, so their families are UNKNOWN rather than empty. An earlier version filed these as closed arithmetic, because an unread statement contains no letters and the test for "numerals only" could not tell absence from evidence. They are listed here so the gap is visible rather than absorbed into a family that reads as an answer.
born_rule_sum— unverifiable-heregrover_amplification— sorryshor_period_finding— sorryrepetition_detects_single_error— sorrysurface_code_correctability— sorryvqe_convergence— sorrytensor_preserves_norm— sorrygrover_amplification— sorrygrover_speedup— sorryqft_unitary— sorryqft_inverse— sorryqft_correctness— sorryphase_estimation_accuracy— sorryshor_period_finding— sorryshor_factorization— sorryvqe_finds_ground_state— sorryqaoa_approximation— sorry
Every family above is recomputed on each run. To disagree with any of it:
npm run families && npm run lean:check && npm run refute