JT0002 jordan_tuple_equal_symmCoordinate equality is symmetric without selecting canonical codes.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableActual finite enumerations · tuple CRT · multiplicativity
Construct and count primitive tuples, prove Jordan-totient multiplicativity, and explore exact unit-modulus and prime-power primitivity laws.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0002 jordan_tuple_equal_symmCoordinate equality is symmetric without selecting canonical codes.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0003 jordan_tuple_equal_transA real decoded middle coordinate witnesses transitivity.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0004 jordan_tuple_common_divisor_transportDivisibility of all coordinates is extensional across tuple encodings.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0005 jordan_primitive_tuple_transportPrimitive means common-divisor one and is independent of beta presentation.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0006 jordan_primitive_tuple_divisor_modulusPrimitivity descends from a modulus to a genuine divisor of it.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0007 jordan_tuple_divisor_downwardA divisor of a common coordinate divisor is again a common divisor.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0008 jordan_primitive_tuple_modulus_oneEvery finite tuple is primitive modulo one, including the zero tuple.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0009 jordan_order_zero_excludedJordan is intentionally restricted to positive tuple order.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT000A jordan_modulus_zero_excludedJordan never counts a purported finite complete residue system modulo zero.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT000B jordan_primitive_tuple_coprime_productActual coprime divisor decomposition proves primitivity for the product modulus.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT000C jordan_primitive_tuple_product_componentsBoth primitive projections follow even without coprimality of the moduli.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT000D jordan_divisibility_congruence_transportA genuine common modulus divisor survives balanced congruence, including divisor zero.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT000E jordan_tuple_congruence_symmPointwise balanced congruence is symmetric on every finite prefix.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT000F jordan_primitive_tuple_congruence_transportPrimitivity is invariant under actual coordinatewise residue transport, not field evaluation.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0010 jordan_tuple_all_divisible_emptyEvery divisor vacuously divides all entries of an empty tuple.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0011 jordan_tuple_all_divisible_extendAdjoining an actually decoded divisible entry preserves common divisibility.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0012 jordan_tuple_all_divisible_decidableFinite induction decides common divisibility from genuine beta entries; no bounded-code oracle.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0013 jordan_tuple_divisor_test_decidableDecide each actual common-divisor-one implication constructively.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0014 jordan_tuple_primitive_bounded_decidableA finite sweep decides the primitive common-divisor condition up to any natural bound.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0015 jordan_primitive_tuple_decidableAt positive modulus every possible common divisor lies below S n, giving genuine tuple-predicate decidability.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0016 jordan_tuple_equal_emptyAll actual empty tuples are coordinatewise equal.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0017 jordan_tuple_equal_drop_lastRestrict coordinate equality to the actual predecessor prefix.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0018 jordan_tuple_equal_extendExtend equal prefixes using two actual equal last entries.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0019 jordan_tuple_equal_decidableInductively decide decoded coordinate equality, never equality of beta codes.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT001A jordan_tuple_listed_emptyAn empty actual outer list contains no representative.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT001B jordan_tuple_listed_liftAn existing list position remains below the successor bound.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT001C jordan_tuple_listed_decidableFinite list membership is decided by actual outer entries and coordinate equality.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT001D jordan_tuple_scan_emptyEmpty scan has soundness, no duplicate positions, and vacuous code coverage.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT001E jordan_tuple_prefix_equalAn actual one-way beta prefix extension preserves decoded coordinates.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT001F jordan_tuple_equal_entryCoordinate equality transports an actual beta entry with unchanged value.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0020 jordan_tuple_bounded_transportThe canonical coordinate bound is independent of tuple encoding.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0021 jordan_tuple_outer_append_existsConstruct both outer beta streams after an append; no list witness is assumed.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0022 jordan_tuple_listed_equal_transportList membership is a property of the represented coordinate tuple.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0023 jordan_tuple_scan_skipSkip precisely when the current admissible tuple is already represented.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0024 jordan_tuple_scan_completeA completed duplicate-free scan of a genuine representative box is the independent enumeration graph.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0025 jordan_totient_from_complete_scanPackage a genuinely completed scan as a Jordan cardinality, without assuming totality.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0026 jordan_tuple_scan_appendAppend an actually absent primitive tuple and prove full soundness, distinctness and prefix coverage.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0027 jordan_tuple_scan_existsConstruct the duplicate-free finite scan by HA induction and three genuine finite decisions.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0028 jordan_tuple_representatives_existsExtract an actual finite coordinate-representative box from the existing beta recoding theorem.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0029 jordan_totient_existsObtain an actual finite tuple cardinality from independently constructed duplicate-free enumeration.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT002A jordan_crt_tuple_emptyThe empty simultaneous coordinate congruence has no missing witness.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT002B jordan_crt_tuple_extendAppend one genuine scalar CRT solution using an actual beta prefix extension.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT002C jordan_crt_tuple_existsConstruct simultaneous residue representatives coordinate by coordinate, without any tuple totality premise.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT002D jordan_crt_tuple_leftEvery actual output coordinate has the required left congruence.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT002E jordan_crt_tuple_rightEvery actual output coordinate has the required right congruence.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT002F jordan_tuple_normalize_existsCanonical coordinate reduction works for every nonzero modulus, not just fields.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0030 jordan_tuple_congruence_transActual decoded middle entries witness transitivity of coordinate congruence.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0031 jordan_tuple_congruence_divisorCoordinate congruence descends along actual divisibility of moduli.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0032 jordan_canonical_crt_tuple_existsConstruct an actual tuple bounded by the product modulus with both prescribed residue tuples.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0033 jordan_primitive_crt_tuple_existsThe constructed canonical CRT tuple is primitive collectively, by coprime common-divisor decomposition.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0034 jordan_rectangle_width_nonzeroA genuine index below u*v forces the rectangle width to be positive.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0035 jordan_rectangle_quotient_boundAn actual bounded row-major index has a row index below u; no division oracle is assumed.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0036 jordan_rectangle_flat_boundEvery actual pair of bounded indices has a row-major index below the literal product.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0037 jordan_rectangle_pair_uniqueActual bounded quotient/remainder decomposition uniquely recovers both indices.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0038 jordan_tuple_equal_congruenceEqual decoded coordinates are congruent at every modulus, including zero.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0039 jordan_tuple_bounded_congruence_equalActual canonical residues with pointwise congruence are equal as coordinate functions.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT003A jordan_tuple_congruence_coprime_productThe actual universal-property lcm merges both coordinate congruences.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT003B jordan_crt_component_recoveryEqual output tuples recover equal canonical input components, not equal raw beta codes.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT003C jordan_canonical_crt_tuple_uniqueThe actual two-coordinate CRT output is unique below the product modulus.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT003D jordan_enumeration_actual_valueEvery actual decoded enumeration entry is bounded and primitive.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT003E jordan_enumeration_completeExtract an actual list position for any primitive canonical tuple.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT003F jordan_enumeration_distinctThe independent enumeration graph identifies equal coordinate tuples with equal positions.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0040 jordan_rectangle_crt_appendAt the next flat index, construct the actual primitive CRT tuple and append its code and scale to fresh beta lists.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0041 jordan_rectangle_crt_successorEliminate the four actual prefix witnesses and append one CRT output in a separate constructive proof scope.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0042 jordan_rectangle_crt_existsHA induction constructs the genuine rectangular CRT output table at every prefix through u*v, including zero-width rectangles.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0043 jordan_rectangle_crt_actual_entryDecode an arbitrary actual output entry without identifying distinct beta representations.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0044 jordan_rectangle_crt_pair_valueThe actual rectangular table realizes every prescribed pair of source entries at its unique flat index.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0045 jordan_enumeration_reduce_primitiveReduce any primitive tuple to an actual canonical enumeration entry, retaining coordinate congruences and the genuine index.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0046 jordan_rectangle_crt_distinctEqual decoded CRT output tuples recover equal source positions and hence the same flat index.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0047 jordan_rectangle_crt_coversEvery primitive product-modulus tuple reduces to a genuine source pair and is formally equal to its table output.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0048 jordan_rectangle_crt_enumerationThe constructed table is a duplicate-free exhaustive primitive tuple enumeration of literal length u*v.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0049 jordan_product_enumeration_existsConstruct an actual product enumeration; no count-uniqueness or multiplicativity premise is used.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT004A jordan_totient_coprime_productActual finite tuple-count Jordan values multiply at coprime moduli.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT004B jordan_totient_multiplicativity_existsThe requested constructive G008 coprime multiplicativity endpoint with all three actual counts supplied.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT004C jordan_enumeration_position_match_from_entriesActual outer beta functionality transports chosen tuple equality to every decoding at the same two positions.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT004D jordan_enumeration_position_match_existsEvery actual source position has a bounded target position representing precisely the same coordinate tuple.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT004E jordan_enumeration_index_map_emptyThe zero-length index map is vacuous, independently of target length.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT004F jordan_enumeration_index_map_appendAppend one genuine matched target index and preserve all previous mapped positions by beta extension.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0050 jordan_enumeration_index_map_existsFinite induction constructs an actual beta map for every source prefix, with no finite-choice axiom.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0051 jordan_enumeration_index_map_entryEvery actual decoded map value is bounded and matches the represented source tuple.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0052 jordan_enumeration_index_map_bounded_injectiveEqual decoded map indices force coordinate-equal source tuples and hence equal source positions, not equal raw tuple codes.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0053 jordan_enumeration_cardinality_leA genuinely constructed bounded injection implies the source count is at most the target count, including empty lists.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0054 jordan_enumeration_cardinality_uniqueTwo complete duplicate-free enumerations of the same primitive coordinate tuples have equal lengths.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0055 jordan_totient_count_uniqueThe independently defined Jordan relation has a unique count, regardless of all chosen beta encodings.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0056 jordan_totient_multiplicativity_unique_countsAny three genuine Jordan counts at coprime moduli obey multiplication, by the independently constructed product enumeration and count uniqueness.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0057 jordan_tuple_bounded_one_entry_zeroEvery decoded coordinate in a tuple bounded by one equals zero.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0058 jordan_zero_tuple_bounded_oneThe literal beta tuple (0,0) has every coordinate below one, at every length.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0059 jordan_tuples_bounded_one_equalAny two canonical tuples modulo one represent the same coordinate tuple.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT005A jordan_unit_modulus_singleton_enumerationAn actual one-position beta list is sound, complete and duplicate-free for primitive tuples modulo one.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT005B jordan_totient_at_oneFor every positive rank k, J_k(1)=1, proved by the explicit singleton enumeration.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT005C jordan_totient_at_one_uniqueEvery genuine Jordan count modulo one equals one, independently of its beta encoding.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT005D jordan_primitive_tuple_avoids_prime_common_divisorA prime divisor of the modulus cannot divide every coordinate of a primitive tuple.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT005E jordan_prime_power_tuple_primitive_of_not_all_divisibleEvery nonunit common divisor has an actual prime divisor; prime-power support then forces a forbidden common factor p.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT005F jordan_prime_power_tuple_primitive_characterizationOver every positive power of a prime, a tuple is primitive exactly when p does not divide all its coordinates.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StableJT0060 jordan_prime_power_tuple_primitivity_invariantPrimitivity of an actual beta tuple is invariant under changing the positive exponent of its prime-power modulus.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not StablePD0001 Le(a,b)Witness-defined non-strict order on natural numbers.
Conservative definition · notation layer 0PD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0PD0003 Dvd(d,n)The natural number d divides n.
Conservative definition · notation layer 0PD0004 Prime(p)p is nonunit and every factorization of p has a unit factor.
Conservative definition · notation layer 0PD0005 Coprime(a,b)Every common divisor of a and b is one.
Conservative definition · notation layer 1PD0007 DivRem(n,d,q,r)q and r are a quotient and a strict remainder for n by d.
Conservative definition · notation layer 1PD0008 ModEq(m,a,b)Balanced-natural congruence modulo m.
Conservative definition · notation layer 0PD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0PD0014 Product(b,c,l,z)z is the product of a beta-coded prefix of length l.
Conservative definition · notation layer 1PD0019 Repeat(b,c,a,l)The decoded prefix repeats a for l positions.
Conservative definition · notation layer 1PD0020 Pow(a,e,z)z is the relational e-th power of a.
Conservative definition · notation layer 2ND0001 Beta(b,c,i,x)Exact hygienic Gödel-beta extraction; a signature-identical alias of checked BetaAt.
Conservative definition · notation layer 0ND0003 MatrixAt(b,c,w,i,j,z)The exact natural matrix entry stored at flattened beta index i*w+j.
Conservative definition · notation layer 1ND0023 CanonicalModularResidue(m,a,r)A strictly bounded canonical natural residue r<m together with exact balanced congruence to a modulo m.
Conservative definition · notation layer 1ND0112 UniformBetaPrefixBox(c,T,l,B)One fixed scale c and positive finite code bound T recode every actual length-l prefix with values below B; completeness is part of the relation.
Conservative definition · notation layer 1ND0113 FiniteMatrixSelector(b,c,l,B)Actual beta-decoded matrix coordinates are all below B and pairwise distinct; the list may be empty.
Conservative definition · notation layer 1ND0121 IntegerVectorZero(ab,ac,db,dc,l)Every actual positive component equals its negative component, so each represented integer is zero.
Conservative definition · notation layer 1ND0262 BetaPrefixInto(b,c,l,B)Every actual beta entry below the strict length l has a witnessed value below B. The same generic graph describes canonical polynomial coefficients when B is the modulus; empty prefixes are allowed.
Conservative definition · notation layer 1ND0263 BetaPrefixEqual(b,c,d,e,l)Every decoded source entry at i<l also decodes in the target. Actual beta totality and functionality make this extensional prefix equality, not equality of the two code parameters.
Conservative definition · notation layer 1ND0269 FpCoefficientReduction(p,b,c,d,e,l)Actual source and target coefficient entries are related by the existing canonical-residue graph at each i<l. Normalization exists even at composite nonzero moduli; field laws require their own prime hypotheses.
Conservative definition · notation layer 2ND0317 DivisorFactorPair(m,n,d,a,b)Actual positive a,b divide m,n respectively and d=a*b. Coprimality of m,n, coordinate bounds, gcd recovery, existence and uniqueness are separate hypotheses or proved consequences, not clauses of this relation.
Conservative definition · notation layer 1ND0371 JordanTupleAllDivisible(d,b,c,k)The natural d divides every actual decoded coordinate in the finite prefix.
Conservative definition · notation layer 1ND0372 JordanPrimitiveTuple(n,b,c,k)Every common divisor of n and all decoded coordinates equals one; boundedness is separate.
Conservative definition · notation layer 2ND0373 JordanTupleCongruence(n,b,c,d,e,k)All paired actual decoded coordinates are congruent modulo n, without imposing a canonical range.
Conservative definition · notation layer 1ND0374 JordanTupleEnumeration(k,n,B,C,D,E,j)Sound, complete and duplicate-free enumeration of canonical primitive tuples; both code and scale columns are actual beta data.
Conservative definition · notation layer 3ND0375 JordanTotient(k,n,j)Positive order and modulus with an actual tuple enumeration of length j. No product identity or existence theorem is a clause.
Conservative definition · notation layer 4ND0376 JordanTupleListed(b,c,k,B,C,D,E,j)An actual decoded tuple occurs, up to coordinate equality, at an actual position in the two-column enumeration.
Conservative definition · notation layer 2ND0377 JordanTupleScan(k,n,c,limit,B,C,D,E,j)A duplicate-free partial enumeration covers precisely the primitive bounded tuples tested by the finite code scan.
Conservative definition · notation layer 3ND0378 JordanTupleRepresentatives(k,n,c,T)Every bounded tuple has a coordinate-equal representative with common scale c and code below T.
Conservative definition · notation layer 2ND0379 JordanTupleCRT(m,n,b,c,d,e,f,g,k)Actual output coordinates satisfy both component congruences. Neither coprimality nor canonicality is implicit.
Conservative definition · notation layer 1ND0380 JordanCanonicalTupleCRT(m,n,b,c,d,e,f,g,k)The output tuple is bounded by m*n and congruent to each actual input tuple at its component modulus.
Conservative definition · notation layer 2ND0381 JordanRectangleCRT(m,n,k,A,B,C,D,u,E,F,G,H,v,P,Q,R,T,q)At each flat rectangle index below q the output has actual entries giving a canonical primitive CRT tuple of the actual source entries.
Conservative definition · notation layer 3Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.