nx_axioms.nx

buildroot/runtime/nx_axioms.nx

10606 B192 linesdepth 0pulls 0 transitivereach 427 importersview sourcekind library

docs dependencies structs consts functions

about

nx_axioms.nx -- foundational axioms as sealed substrate constants. THE BUILD-FROM-ZERO DISCIPLINE: every higher primitive must trace its derivation back to these axioms via lineage_ids. No primitive ships without showing the chain (axiom -> ... -> primitive). This file is the substrate's MATHEMATICAL FLOOR. Nothing lives below it; every theorem above lives by citation through it. Citations: Peano (1889) "Arithmetices principia" Zermelo (1908) "Untersuchungen über die Grundlagen der Mengenlehre" Fraenkel (1922) replacement axiom Skolem (1923) first-order form of ZF Boole (1854) "An Investigation of the Laws of Thought" Aristotle (~350 BC) Organon (laws of thought) Tarski (1936) formal definition of truth Hilbert (1899) geometry axiomatization genealogy_id: peano_1889 + zfc + boole_1854 + aristotle_organon lineage_id: foundational

dependencies 0 imports · 71 importers

diagram shows first 10 each side; +0 more imports, +61 more importers in the complete lists below.

imports: none

imported by: nx_ac_monitor_census.nxnx_atp_to_derive.nxnx_atp_to_derive_test.nxnx_auto_verify.nxnx_auto_verify_test.nxnx_color_v2.nxnx_complex.nxnx_coq_ingest.nxnx_dedup_audit.nxnx_derive.nxnx_derive_test.nxnx_diagram.nxnx_features.nxnx_features_test.nxnx_five_systems_test.nxnx_func_extract.nxnx_geom.nxnx_graph.nxnx_group.nxnx_help.nxnx_help_test.nxnx_hol_ingest.nxnx_i256.nxnx_image.nxnx_ingest_pipeline.nxnx_ingest_pipeline_test.nxnx_input.nxnx_isabelle_ingest.nxnx_jargon.nxnx_lattice.nxnx_lean_ingest.nxnx_lex.nxnx_math.nxnx_measure.nxnx_mizar_ingest.nxnx_perf_bench.nxnx_poly.nxnx_proof_infinitude_primes.nxnx_proof_methods.nxnx_proof_sqrt2_irrational.nxnx_proofs_comprehensive.nxnx_proofs_machine_checked.nxnx_proofs_pvsnp_pending.nxnx_proofs_top100.nxnx_proofs_top100_batch2.nxnx_proofs_top100_batch3.nxnx_proofs_top100_batch4.nxnx_proofs_top100_batch5.nxnx_proofs_top100_batch6_closing.nxnx_prover.nxnx_prover_a1.nxnx_prover_a1_test.nxnx_prover_eval.nxnx_prover_eval_test.nxnx_prover_test.nxnx_qed_db.nxnx_qed_db_test.nxnx_qed_freek.nxnx_question_genealogy.nxnx_sensor_gap_census.nxnx_shard.nxnx_substrate_diagram.nxnx_substrate_diagram_ascii.nxnx_substrate_evolve.nxnx_substrate_propose.nxnx_termios.nxnx_theorem_card.nxnx_theorem_ingest.nxnx_tty.nxnx_validation_cycle.nxnx_validation_cycle_test.nx

structs

none

consts

32	const NX_AX_PEANO_PA1_ZERO_EXISTS: i64 = 101
33	const NX_AX_PEANO_PA2_SUCCESSOR: i64 = 102
34	const NX_AX_PEANO_PA3_ZERO_NOT_SUCC: i64 = 103
35	const NX_AX_PEANO_PA4_SUCC_INJECTIVE: i64 = 104
36	const NX_AX_PEANO_PA5_INDUCTION: i64 = 105
51	const NX_AX_ZFC_EXTENSIONALITY: i64 = 201
52	const NX_AX_ZFC_EMPTY_SET: i64 = 202
53	const NX_AX_ZFC_PAIRING: i64 = 203
54	const NX_AX_ZFC_UNION: i64 = 204
55	const NX_AX_ZFC_POWER_SET: i64 = 205
56	const NX_AX_ZFC_INFINITY: i64 = 206
57	const NX_AX_ZFC_SEPARATION: i64 = 207
58	const NX_AX_ZFC_REPLACEMENT: i64 = 208
59	const NX_AX_ZFC_FOUNDATION: i64 = 209
60	const NX_AX_ZFC_CHOICE: i64 = 210
64	const NX_AX_LOGIC_IDENTITY: i64 = 301 // A -> A
65	const NX_AX_LOGIC_NONCONTRADICTION: i64 = 302 // ~(A ^ ~A)
66	const NX_AX_LOGIC_EXCLUDED_MIDDLE: i64 = 303 // A v ~A
67	const NX_AX_LOGIC_DISTRIBUTIVITY: i64 = 304 // A^(BvC) = (A^B)v(A^C)
68	const NX_AX_LOGIC_DEMORGAN: i64 = 305 // ~(A^B) = ~A v ~B
69	const NX_AX_LOGIC_MODUS_PONENS_RULE: i64 = 306 // A, A->B \|- B (rule)
70	const NX_AX_LOGIC_UNIVERSAL_INSTANT: i64 = 307 // forall x P(x) \|- P(t)
71	const NX_AX_LOGIC_EXISTENTIAL_GEN: i64 = 308 // P(t) \|- exists x P(x)
75	const NX_AX_REL_REFLEXIVITY: i64 = 401 // a R a
76	const NX_AX_REL_SYMMETRY: i64 = 402 // a R b -> b R a
77	const NX_AX_REL_TRANSITIVITY: i64 = 403 // a R b ^ b R c -> a R c
78	const NX_AX_REL_ANTISYMMETRY: i64 = 404 // a R b ^ b R a -> a = b
79	const NX_AX_REL_TOTALITY: i64 = 405 // a R b v b R a
80	const NX_AX_REL_TRICHOTOMY: i64 = 406 // exactly one of <, =, >
84	const NX_AX_ALG_ASSOCIATIVITY: i64 = 501 // (ab)c = a(bc)
85	const NX_AX_ALG_COMMUTATIVITY: i64 = 502 // ab = ba
86	const NX_AX_ALG_IDENTITY_ELEMENT: i64 = 503 // exists e: a*e = a
87	const NX_AX_ALG_INVERSE_ELEMENT: i64 = 504 // exists a': a*a' = e
88	const NX_AX_ALG_DISTRIBUTIVITY: i64 = 505 // a(b+c) = ab + a*c
89	const NX_AX_ALG_CLOSURE: i64 = 506 // a,b in S -> a*b in S
93	const NX_AX_ORD_LEAST_UPPER_BOUND: i64 = 601 // every bounded set has sup
94	const NX_AX_ORD_ARCHIMEDEAN: i64 = 602 // for any x, exists n: n>x
95	const NX_AX_ORD_DEDEKIND_COMPLETENESS: i64 = 603 // Dedekind cut existence
103	const NX_AX_PROB_NONNEGATIVITY: i64 = 701
104	const NX_AX_PROB_NORMALIZATION: i64 = 702
105	const NX_AX_PROB_COUNTABLE_ADDITIVITY: i64 = 703
109	const NX_AX_MEAS_NULL_EMPTY: i64 = 801 // mu(empty) = 0
110	const NX_AX_MEAS_MONOTONICITY: i64 = 802 // A subset B -> mu(A) <= mu(B)
111	const NX_AX_MEAS_SUBADDITIVITY: i64 = 803 // mu(A u B) <= mu(A)+mu(B)
115	const NX_AX_GEO_TWO_POINTS_DETERMINE_LINE: i64 = 901
116	const NX_AX_GEO_LINE_EXTENDS: i64 = 902
117	const NX_AX_GEO_CIRCLE_FROM_CENTER_RADIUS: i64 = 903
118	const NX_AX_GEO_RIGHT_ANGLES_EQUAL: i64 = 904
119	const NX_AX_GEO_PARALLEL_POSTULATE: i64 = 905
123	const NX_AX_CAT_IDENTITY_MORPHISM: i64 = 1001
124	const NX_AX_CAT_COMPOSITION: i64 = 1002
125	const NX_AX_CAT_COMPOSITION_ASSOC: i64 = 1003

functions

135	func nx_axiom_name(code: i64) -> *u8 called by 1: nx_deriv_walk
180	func nx_axiom_is_valid(code: i64) -> i64 called by 3: nx_deriv_add_axiom nx_deriv_verify nx_prover_add_axiom