Plectis

The universe map

1,292 objects and 3,246 connections, generated from the public Lean repository. The first screen shows the 192 navigational objects; load the complete universe to add every Lean module and argument step.

Papers explain, Comparator replays selected exact interfaces, and Palomar may review a prepared unit. None widens Lean's proposition or records peer review or an accepted outcome unless its own source says so.

Show

The interactive map needs JavaScript. Every object it shows is in the lists below, and the complete graph is published as graph.json.

  • Problems
  • Claims
  • Papers
  • Documents
  • Verification
  • Modules
  • Argument steps

Hover an object to preview it in the side panel; click to pin its card and list its connections. Drag to pan, scroll to zoom, press Esc to unpin. Loading the complete universe fetches about 1.4 MB once.

Problems (8)
Papers (13)
Repository documents (14)
Checked claims (103)
Comparator review families (50)
  • A bounded search records finite geometric evidence. not_applicable_not_a_lean_theorem
  • The Newton value equation and its exponential first integral are checked exactly. not_selected_compact_calculus_family
  • The paper identifies an invalid local saddle block in a claimed unrestricted proof. not_applicable_not_a_lean_proposition
  • Distinct positive rays exclude a finite Newton connection. represented_by_translation_avoidance_targets
  • A quantified small constant perturbation keeps every polynomial root inside the open unit disc. targeted
  • Collision translations are parameterised by real affine lines and an arbitrarily small common translation avoids finitely many of them. targeted
  • The coordinatewise corridor forces a power-versus-linear inequality and cannot occur at base 3/2. targeted
  • Endpoint residues at 2 and 3 exclude a common multiplier under unit-endpoint hypotheses. represented_by_selected_coordinatewise_no_go
  • Binary selectors collide in the four-jet signature at the stated rank and depth. not_selected_finite_combinatorial_family
  • Exact height-region inclusions and exclusions, Padé denominator-exponent bounds, and a rectangular Hermite-Padé threshold no-go are checked. not_selected_multiple_scoped_arithmetic_families
  • The exact rational-base cleared-tail recurrence exposes exponential denominator-base forcing absent at integer bases. targeted
  • Integer scalar content changes analytic error and exterior determinant by matching factors, yielding no margin by itself. represented_by_selected_coordinatewise_no_go
  • Irrationality at 7/2 is obtained from an external analytic criterion whose elementary height hypothesis is checked in Lean. not_applicable_to_external_irrationality_conclusion
  • Normalised vanishing excludes a cofinally bounded negative part and forces eventual Sylvester behaviour. targeted
  • A bounded-rise sequence cannot remain coprime to fresh pairwise-coprime moduli; reduced tails inherit this obstruction. represented_by_stronger_selected_boundary_theorem
  • Exact update and defect identities, scale equivariance, zero absorption, and eventual recovery of the Sylvester recurrence. represented_by_selected_boundary_theorems
  • Finite normalised negative mass forces eventual zero and hence the Sylvester recurrence. not_selected_deep_state_vocabulary
  • Constant, eventually constant, periodic, and eventually periodic negative-error orbits are excluded in their stated regimes. targeted_representative_periodic_theorem
  • Eventually periodic nonnegative rational weights give an irrational Lambert series. not_selected_prior_result
  • Rationality forces a tempered integral tail orbit with unbounded finite-level carry rank. not_selected_deep_orbit_vocabulary
  • Pointwise, cofinal, lcm-diagonal, and separated-window certificate supplies are exact or sufficient reformulations. not_selected_deep_certificate_vocabulary
  • A Farey denominator exclusion through 7.96e34, sharp for its selected window, and diagonal certificates through t=82. not_selected_finite_family_has_separate_receipt
  • For every base k at least 2, Lean checks the arithmetic reduction, exact nonmultiple-residue coordinates, unconditional canonical spanning, and exact rank k^e+1 conditional on canonical-family linear independence. not_selected_external_independence_boundary
  • An explicit odd-core basis and relation normal form for the full dyadic totient kernel. targeted
  • An independent constructive proof of exact finite-level dyadic rank 2^e+1, together with a kernel-checked full-kernel infinite-dimensionality corollary already implied by Coons's non-2-regularity theorem. targeted
  • The totient series is rewritten as a Lambert series with explicit nonnegative, unbounded prime-power coefficients. represented_by_basis_and_rank_targets
  • Prime gaps are unbounded and non-eventually-periodic, while an explicit nonperiodic unbounded countermodel still has rational sum. targeted_unboundedness_theorem_only
  • Block identities and exact denominator criteria classify rationality through integral positive tail shifts. not_selected_abstract_family_represented_in_manifest
  • Exact finite summation by parts, the unconditional infinite prime-gap identity, and irrationality equivalence. targeted
  • Cofinal adjacent small mismatches would rule out eventual integral shifts for the prime-gap tail. not_selected_open_producer_hypothesis
  • Odd rational denominators give totient-length integral shifts, and integrality propagates through the recurrence. represented_by_integral_shift_family
  • Compactness, perfectness, total disconnectedness, nowhere density, and measure one for the unrestricted achievement set. targeted_measure_theorem
  • The multiplicative order of the base modulo a reduced finite-sum denominator is the support lcm, forcing denominator growth. targeted
  • Exact greedy characterisations and finite-support exclusions isolate the remaining 1/2 and 1/21 alternatives. not_selected_deep_greedy_state_vocabulary
  • Full, factorial, power-of-two, multiple, pairwise-coprime, eventually periodic, residue-class, and odd supports are formalised. targeted_full_support_representative
  • Rational infinite supports force unbounded scaled tails, sublogarithmic zero windows, and reciprocal-mass constraints. not_selected_deep_support_vocabulary
  • Support-restricted coding is injective and the associated achievement set has exact finite-complement measure or zero for infinite complement. targeted_measure_dichotomy
  • Lean checks squarefree incidence and no-go statements; the irrationality conclusion uses an external analytic theorem in the paper. not_applicable_to_external_irrationality_input
  • Cofinal local-window residue escape would rule out bounded positive carries after an unproved rationality-to-carry bridge. not_selected_unproved_bridge_and_deep_predicates
  • The exact dyadic block alphabet is 2, 6, 10, and 30. represented_by_three_prime_structure_target
  • Finite height-fibre normal form and a quadratic smooth-shell multiplicity bound. represented_by_three_prime_structure_target
  • The 2,3,5 kernel is not rank one and its smallest displayed minor equals -1/15. targeted
  • A local-window checker searches 106666 denominator and start pairs and records small certificates. not_applicable_not_a_lean_theorem
  • Exact running-LCM product, logarithmic-cell constancy, coordinate jump ratios, and jump count. targeted_running_lcm_identity
  • Both two-prime running-lcm series are proved transcendental by an authored deduction from an external theorem. not_applicable_not_a_lean_declaration
  • Exact equivalence between irrationality, cofinally many non-unit carries, and cofinal strict-successor divisibility failures. targeted
  • Finite channel congruences, a two-term prime-channel corrector, and endpoint-weighted projection rigidity. represented_by_isolated_headline
  • Cofinal zero-branch or large private-factor hypotheses imply the required irrationality conclusion. not_selected_deep_project_predicate_stack
  • Lean checks small exact misses; a hash-bound GMP scan reaches index 300000 and yields the corresponding finite denominator exclusion. not_applicable_to_external_execution
  • A paper deduction gives a lower bound for the lcm of factorial-gap denominators using an external multiplicity theorem. not_applicable_not_a_lean_declaration
Lean modules (1,021)

The 40 modules with per-problem declaration counts are listed here; the complete set is in the loaded universe and in the repository.

Argument steps (79)

Steps of the recorded argument graph, published in graph.json with their relations.