test(int-factor): complete Phase 3 conformance

HexIntFactorMathlib/SPEC/hex-int-factor-mathlib.md

@@ -0,0 +1,69 @@
+# hex-int-factor-mathlib (depends on hex-int-factor + hex-primality-mathlib + Mathlib)
+
+## Correspondence-only classification
+
+This library is a `correspondence-only-layer`.
+
+Computational conformance owner: `HexIntFactor`
+Computational performance owner: `HexIntFactor`
+
+The companion proves that checked `HexIntFactor` data agrees with Mathlib's
+factorization, divisor, squarefree, totient, and multiplicative-order APIs. It
+does not search for factors or orders, replay a certificate, reify syntax, run
+a tactic, or install a decision procedure. All transported values are computed
+by `HexIntFactor`; this layer supplies proofs that identify those values with
+their Mathlib counterparts.
+
+## Factorization correspondences
+
+`HexIntFactorMathlib.Factorization` transports the core checker facts and
+arithmetic operations:
+
+- `factorization_entry`, `factorization_eq`, and
+  `CheckedFactorization.factorization_eq` identify checked multiplicities with
+  `Nat.factorization`;
+- `factorization_absent` pins zero multiplicity outside the listed prime
+  support;
+- `factors_eq` and `CheckedFactorization.primeFactorsList_eq` identify the
+  canonical expanded prime list;
+- `divisors_eq`, `divisors_list_eq`, and `numDivisors_eq_card` identify the
+  checked divisor enumeration and count;
+- `totient_eq`, `sigma_eq`, `primeFactors_eq`, and `radical_eq` transport the
+  corresponding arithmetic functions; and
+- `isSquarefree_iff_squarefree`, `squarefreePart_mathlib`, and
+  `squareDivisor_mathlib` transport the square-decomposition facts.
+
+Their computational coverage lives in
+`conformance/HexIntFactor/Conformance.lean`: complete-certificate acceptance
+and rejection, canonical factor support and multiplicity, divisor enumeration,
+generalized divisor sums, totient, radical, and squarefree decomposition all
+have typical, edge, and adversarial checks. The required PARI/python-flint
+oracle independently recomputes factorization and the transported arithmetic
+values from the original inputs.
+
+The private expanded-list helpers occur only in theorem statements and proofs.
+They are normal forms for correspondence, not a separately advertised runtime
+surface.
+
+## Order correspondences
+
+`HexIntFactorMathlib.Order` proves:
+
+- `orderOf_unitOfCoprime`, relating the core natural-number order to Mathlib's
+  order of the corresponding unit;
+- `orderOf_natCast`, including the nonunit case; and
+- `orderOf_eq`, specializing the correspondence to an accepted `OrderCert`.
+
+The transported `Hex.Nat.orderOf` computation is covered by the
+`HexPrimality` conformance suite. `HexIntFactor` conformance separately covers
+accepted, malformed, and nonminimal order certificates, primitive-root
+testing and bounded search, and Carmichael values and laws. This companion
+contains no bridge-local executable operation to test independently.
+
+## Boundary
+
+The public umbrella imports only the two correspondence modules. The library
+owns no conformance source, compiled benchmark, proof-probe root, oracle
+wrapper, executable checker, reifier, tactic, or global instance. It therefore
+has no ordinary Phase-3 conformance target and no separate Phase-4 runtime
+surface.

conformance-fixtures/HexIntFactor/intfactor.jsonl

@@ -87,21 +87,21 @@
 {"kind":"factor","lib":"HexIntFactor","case":"factor/below100/49","n":49}
 {"kind":"result","lib":"HexIntFactor","case":"factor/below100/49","op":"factor","value":[[7,2]]}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/1","n":1}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/1","op":"divisorfn","value":{"tau":1,"sigma0":1,"sigma1":1,"sigma2":1,"phi":1,"rad":1,"sqfpart":1,"sqdiv":1}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/1","op":"divisorfn","value":{"divisors":[1],"tau":1,"sigma0":1,"sigma1":1,"sigma2":1,"phi":1,"rad":1,"sqfpart":1,"sqdiv":1}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/2","n":2}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/2","op":"divisorfn","value":{"tau":2,"sigma0":2,"sigma1":3,"sigma2":5,"phi":1,"rad":2,"sqfpart":2,"sqdiv":1}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/2","op":"divisorfn","value":{"divisors":[1,2],"tau":2,"sigma0":2,"sigma1":3,"sigma2":5,"phi":1,"rad":2,"sqfpart":2,"sqdiv":1}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/4","n":4}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/4","op":"divisorfn","value":{"tau":3,"sigma0":3,"sigma1":7,"sigma2":21,"phi":2,"rad":2,"sqfpart":1,"sqdiv":2}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/4","op":"divisorfn","value":{"divisors":[1,2,4],"tau":3,"sigma0":3,"sigma1":7,"sigma2":21,"phi":2,"rad":2,"sqfpart":1,"sqdiv":2}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/12","n":12}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/12","op":"divisorfn","value":{"tau":6,"sigma0":6,"sigma1":28,"sigma2":210,"phi":4,"rad":6,"sqfpart":3,"sqdiv":2}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/12","op":"divisorfn","value":{"divisors":[1,2,3,4,6,12],"tau":6,"sigma0":6,"sigma1":28,"sigma2":210,"phi":4,"rad":6,"sqfpart":3,"sqdiv":2}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/72","n":72}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/72","op":"divisorfn","value":{"tau":12,"sigma0":12,"sigma1":195,"sigma2":7735,"phi":24,"rad":6,"sqfpart":2,"sqdiv":6}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/72","op":"divisorfn","value":{"divisors":[1,2,3,4,6,8,9,12,18,24,36,72],"tau":12,"sigma0":12,"sigma1":195,"sigma2":7735,"phi":24,"rad":6,"sqfpart":2,"sqdiv":6}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/360","n":360}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/360","op":"divisorfn","value":{"tau":24,"sigma0":24,"sigma1":1170,"sigma2":201110,"phi":96,"rad":30,"sqfpart":10,"sqdiv":6}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/360","op":"divisorfn","value":{"divisors":[1,2,3,4,5,6,8,9,10,12,15,18,20,24,30,36,40,45,60,72,90,120,180,360],"tau":24,"sigma0":24,"sigma1":1170,"sigma2":201110,"phi":96,"rad":30,"sqfpart":10,"sqdiv":6}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/248832","n":248832}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/248832","op":"divisorfn","value":{"tau":66,"sigma0":66,"sigma1":745108,"sigma2":92875849430,"phi":82944,"rad":6,"sqfpart":3,"sqdiv":288}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/248832","op":"divisorfn","value":{"divisors":[1,2,3,4,6,8,9,12,16,18,24,27,32,36,48,54,64,72,81,96,108,128,144,162,192,216,243,256,288,324,384,432,486,512,576,648,768,864,972,1024,1152,1296,1536,1728,1944,2304,2592,3072,3456,3888,4608,5184,6912,7776,9216,10368,13824,15552,20736,27648,31104,41472,62208,82944,124416,248832],"tau":66,"sigma0":66,"sigma1":745108,"sigma2":92875849430,"phi":82944,"rad":6,"sqfpart":3,"sqdiv":288}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/1296000","n":1296000}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/1296000","op":"divisorfn","value":{"tau":160,"sigma0":160,"sigma1":4813380,"sigma2":2624308792820,"phi":345600,"rad":30,"sqfpart":10,"sqdiv":360}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/1296000","op":"divisorfn","value":{"divisors":[1,2,3,4,5,6,8,9,10,12,15,16,18,20,24,25,27,30,32,36,40,45,48,50,54,60,64,72,75,80,81,90,96,100,108,120,125,128,135,144,150,160,162,180,192,200,216,225,240,250,270,288,300,320,324,360,375,384,400,405,432,450,480,500,540,576,600,640,648,675,720,750,800,810,864,900,960,1000,1080,1125,1152,1200,1296,1350,1440,1500,1600,1620,1728,1800,1920,2000,2025,2160,2250,2400,2592,2700,2880,3000,3200,3240,3375,3456,3600,4000,4050,4320,4500,4800,5184,5400,5760,6000,6480,6750,7200,8000,8100,8640,9000,9600,10125,10368,10800,12000,12960,13500,14400,16000,16200,17280,18000,20250,21600,24000,25920,27000,28800,32400,36000,40500,43200,48000,51840,54000,64800,72000,81000,86400,108000,129600,144000,162000,216000,259200,324000,432000,648000,1296000],"tau":160,"sigma0":160,"sigma1":4813380,"sigma2":2624308792820,"phi":345600,"rad":30,"sqfpart":10,"sqdiv":360}}
 {"kind":"order","lib":"HexIntFactor","case":"order/primitive/3mod7","base":3,"modulus":7}
 {"kind":"result","lib":"HexIntFactor","case":"order/primitive/3mod7","op":"order","value":6}
 {"kind":"order","lib":"HexIntFactor","case":"order/nonprimitive/2mod7","base":2,"modulus":7}