F1 - GitLite

KO | EN

gitlite — search

#codex #agent #linux #generative-ai #typescript #nodejs #database #ruby #graphql #shell

F1

(★ 9)

Lean 4 research base: the 𝔽₁ square Spec ℤ ×_𝔽₁ Spec ℤ whose Hodge-index positivity is the Riemann Hypothesis (RH open).

File Explorer

ZIP Download

- devcontainer.json
- - ci.yml
- characteristic_1_constructions.md
- f1_square_intersection_theory.md
- missing_object_over_Q.md
- - AffineIntegral.lean
  - ArchTrend.lean
  - Arctan.lean
  - ArctanODE.lean
  - ArctanTan.lean
  - ArtanhAdd.lean
  - BandClamp.lean
  - Bernoulli.lean
  - BernoulliPoly.lean
  - Bernstein.lean
  - BernsteinMoments.lean
  - Binomial.lean
  - BumpPieces.lean
  - BurnolAlpha.lean
  - BurnolAlphaTwo.lean
  - CayleyMap.lean
  - ClampedInv.lean
  - ClampedInvLower.lean
  - ClampOne.lean
  - ClogAddBounded.lean
  - Complete.lean
  - CompletedZetaMellin.lean
  - Complex.lean
  - ComplexArg.lean
  - ComplexArgAdd.lean
  - ComplexArgLeft.lean
  - ComplexArgLeftAdd.lean
  - ComplexArgLower.lean
  - ComplexArgUpper.lean
  - ComplexArgUpperAdd.lean
  - ComplexBinomial.lean
  - ComplexConjAlgebra.lean
  - ComplexCore.lean
  - ComplexDigamma.lean
  - ComplexDigammaConj.lean
  - ComplexDigammaValue.lean
  - ComplexExp.lean
  - ComplexExpAdd.lean
  - ComplexGammaConj.lean
  - ComplexIntegral.lean
  - ComplexInv.lean
  - ComplexLimit.lean
  - ComplexLimitCore.lean
  - ComplexLog.lean
  - ComplexLogConj.lean
  - ComplexLogLeft.lean
  - ComplexLogLeftAdd.lean
  - ComplexLogLower.lean
  - ComplexLogLowerAdd.lean
  - ComplexLogUpper.lean
  - ComplexLogUpperAdd.lean
  - ComplexMod.lean
  - ComplexNormSqCore.lean
  - ComplexPow.lean
  - ComplexPowGen.lean
  - ComplexSeries.lean
  - ComplexXi.lean
  - ComplexXiConj.lean
  - ComplexXiConjFull.lean
  - ComplexXiFE.lean
  - ComplexXiHadamard.lean
  - ComplexZeta.lean
  - ComplexZetaConj.lean
  - CosSin.lean
  - CosSinAdd.lean
  - CosSinAddFormula.lean
  - CosSinBound.lean
  - CovRateQ.lean
  - CriticalZeta.lean
  - DigammaWindow.lean
  - DilateIntegral.lean
  - DilateTestR.lean
  - DilogPhi.lean
  - DilogPhiVal.lean
  - DilogPieces.lean
  - DilogValue.lean
  - DyadicIntegral.lean
  - EtaFunction.lean
  - EtaVariation.lean
  - Euler.lean
  - EulerMaclaurin.lean
  - ExactBounded.lean
  - Exp.lean
  - ExpAdd.lean
  - ExpBounds.lean
  - ExpGen.lean
  - ExpLog.lean
  - ExpReal.lean
  - ExpRealAdd.lean
  - ExpRealMono.lean
  - ExpVarGlobal.lean
  - Gamma.lean
  - GammaAccel.lean
  - GammaFour.lean
  - GammaFourBracket.lean
  - GammaFourLower.lean
  - GammaOne.lean
  - GammaOneBracket.lean
  - GammaThree.lean
  - GammaThreeBracket.lean
  - GammaThreeLower.lean
  - GammaTwo.lean
  - GammaTwoBracket.lean
  - GammaTwoUpper.lean
  - GammaUpper.lean
  - GammaZeroBracket.lean
  - GenSumGeom.lean
  - GenSumOfQ.lean
  - GenuineLi.lean
  - HaarDensity.lean
  - HaarInterval.lean
  - HarmonicLog.lean
  - HarmonicLog32.lean
  - HarmonicLogC.lean
  - ImproperIntegral.lean
  - IntegralBilinear.lean
  - IntegralCertIrrel.lean
  - IntegralEval.lean
  - IntegralInner.lean
  - IntegralLocal.lean
  - IntegralRsmul.lean
  - IntervalCert.lean
  - IntervalIntegral.lean
  - IntervalRsmul.lean
  - Inv.lean
  - LambdaFive.lean
  - LambdaFivePos.lean
  - LambdaFivePrecision.lean
  - LambdaFour.lean
  - LambdaFourPos.lean
  - LambdaFourThreeGap.lean
  - LambdaFourUpper.lean
  - LambdaGap.lean
  - LambdaOne.lean
  - LambdaThree.lean
  - LambdaThreePos.lean
  - LambdaThreeUpper.lean
  - LambdaTwo.lean
  - LambdaTwoThreePrecision.lean
  - LiComplete.lean
  - LiGrowth.lean
  - LiLinearize.lean
  - LiOne.lean
  - LiTwo.lean
  - Log.lean
  - LogDiffBound.lean
  - LogDiffBoundGen.lean
  - LogFourPiLower.lean
  - LogIntegralEval.lean
  - LogIntegrand.lean
  - LogOverX.lean
  - LogOverXEval.lean
  - LogOverXRate.lean
  - LogOverXSum.lean
  - LogPiLower.lean
  - LogPointVal.lean
  - LogRatBridge.lean
  - LogRatCert.lean
  - LogRiemann.lean
  - LogSqStep.lean
  - LogStep.lean
  - Mangoldt.lean
  - MellinDecay.lean
  - MomentCayley.lean
  - MomentEta.lean
  - MonotoneIntegral.lean
  - MulConvR.lean
  - MulConvRBound.lean
  - MulConvRCongr.lean
  - MulConvRDecay.lean
  - MulConvRDiff.lean
  - OffLineGrowth.lean
  - Pi.lean
  - Pow.lean
  - ProductTest.lean
  - PsiLine.lean
  - PsiQuarter.lean
  - QOrder.lean
  - RabsLemmas.lean
  - RAddNF.lean
  - RadiusGen.lean
  - RArctan.lean
  - RArctanCongr.lean
  - RArctanExt.lean
  - RArctanValue.lean
  - RartanhBounds.lean
  - Rat.lean
  - RdivBounds.lean
  - Real.lean
  - RealBinomial.lean
  - RealCompare.lean
  - RealDiv.lean
  - RealNullFamily.lean
  - RealOrderCore.lean
  - RealPow.lean
  - RealSquareDefinite.lean
  - RecipSmulEval.lean
  - Reflection.lean
  - ReflectTest.lean
  - RexpAbsLip.lean
  - RexpLogRat.lean
  - RHWitness.lean
  - RiemannConv.lean
  - RiemannSiegel.lean
  - RiemannSum.lean
  - RiemannZero.lean
  - RingNF.lean
  - RingTac.lean
  - RinvDilate.lean
  - RlimProps.lean
  - RlogAbsLip.lean
  - RlogMulPos.lean
  - RlogMulSigned.lean
  - RMax.lean
  - RmulLipschitz.lean
  - RMulNF.lean
  - ROrder.lean
  - RpowBaseLip.lean
  - RpowClamp.lean
  - RpowClampLip.lean
  - RQmaxClamp.lean
  - RrpowAbsLip.lean
  - RrpowAbsLipNat.lean
  - RrpowBounds.lean
  - RSeqApprox.lean
  - RSum.lean
  - RTendsToClose.lean
  - SqrtRat.lean
  - SqrtReal.lean
  - SqrtRealCmp.lean
  - SqrtRealOf.lean
  - SqrtRealSq.lean
  - T4ArchPieces.lean
  - T4PoleAAssembly.lean
  - T4PoleAPieces.lean
  - T4PoleBPieces.lean
  - T4TailImproper.lean
  - TanPiQuarter.lean
  - TentArchPiece.lean
  - TentArchTail.lean
  - TentLogPiece.lean
  - ThetaDecay.lean
  - ThetaFunction.lean
  - ThetaFunctionPos.lean
  - ThetaLipschitz.lean
  - ThetaLipschitzFn.lean
  - ThetaMellin.lean
  - ThetaMellinPow.lean
  - ThetaModular.lean
  - ThetaValueDecay.lean
  - TraceBridge.lean
  - Voros.lean
  - Weil.lean
  - WindowBoundReal.lean
  - ZeroGeometry.lean
  - Zeta.lean
  - ZetaTwo.lean
- - AngleEmbeddingBound.lean
  - AngleGramDiagonal.lean
  - AngleGramRlim.lean
  - AngleRegDischarge.lean
  - AngleTargetAcc.lean
  - AngleTargetBound.lean
  - ArchimedeanPlace.lean
  - AtlasAddressing.lean
  - AtlasAnalyticFace.lean
  - AtlasAnchorAutocorr.lean
  - AtlasAnchorExtract.lean
  - AtlasAnchorKernel.lean
  - AtlasAnchorLocalize.lean
  - AtlasAngleFamily.lean
  - AtlasArchCoords.lean
  - AtlasArchGram.lean
  - AtlasBundle.lean
  - AtlasCalculus.lean
  - AtlasCarrier.lean
  - AtlasCarrier5.lean
  - AtlasChannels.lean
  - AtlasCharacteristics.lean
  - AtlasClasses.lean
  - AtlasCoherence.lean
  - AtlasCoherent5.lean
  - AtlasCoherentBridge.lean
  - AtlasColligation5.lean
  - AtlasComplete.lean
  - AtlasComposition.lean
  - AtlasConservation.lean
  - AtlasCoxeter.lean
  - AtlasCruxSynthesis.lean
  - AtlasCutRecovery.lean
  - AtlasDefectGram.lean
  - AtlasDefectReadback.lean
  - AtlasExceptional.lean
  - AtlasFarCoefStable.lean
  - AtlasFibers.lean
  - AtlasField2.lean
  - AtlasFiveSplit.lean
  - AtlasForcing.lean
  - AtlasFullCoherent5.lean
  - AtlasGammaAtom.lean
  - AtlasGenerator.lean
  - AtlasGrowth.lean
  - AtlasIncidence.lean
  - AtlasJoint5.lean
  - AtlasJointReadback.lean
  - AtlasModular.lean
  - AtlasOrbitAddress.lean
  - AtlasOrbitDecode.lean
  - AtlasOrbitFiber.lean
  - AtlasOrbitHaar.lean
  - AtlasOrbitModels.lean
  - AtlasParamIntegral.lean
  - AtlasPositivityStructure.lean
  - AtlasPrimeDirect.lean
  - AtlasPrimeDyadicReadback.lean
  - AtlasPrimeFold.lean
  - AtlasPrimePowerFold.lean
  - AtlasReynolds.lean
  - AtlasRHConnection.lean
  - AtlasRule.lean
  - AtlasScaleField.lean
  - AtlasSourceCoherent.lean
  - AtlasSourceLaws.lean
  - AtlasSpectralCore.lean
  - AtlasSpectrum.lean
  - AtlasSynthesis.lean
  - AtlasTailSplit.lean
  - AtlasTopology.lean
  - AtlasUniformEnergy.lean
  - AtlasWindowZero.lean
  - Attempt.lean
  - Autocorr.lean
  - BandBridge.lean
  - Bern2DDeviation.lean
  - Bern2DFinrankSymm.lean
  - Bern2DGeneralSwap.lean
  - Bern2DInnerClose.lean
  - Bern2DOperator.lean
  - Bern2DOuterClose.lean
  - Bern2DUniform.lean
  - Bern2DValue.lean
  - Bern2DWindowSwap.lean
  - BernsteinBasisZero.lean
  - BernsteinClampMatch.lean
  - BernsteinConverge.lean
  - BernsteinDevBound.lean
  - BernsteinDeviation.lean
  - BernsteinDeviationTransfer.lean
  - BernsteinEnergyBound.lean
  - BernsteinL2Density.lean
  - BernsteinL2Limit.lean
  - BernsteinOperatorTest.lean
  - BernsteinUniform.lean
  - BernsteinVariance.lean
  - BesselCauchyModulus.lean
  - BesselPartialNorm.lean
  - BesselSeqDist.lean
  - BlockLadderCandidate.lean
  - BLPipeline.lean
  - BumpSlot.lean
  - ClosedWeilBilin.lean
  - Cohomology.lean
  - CompactMomentDilate.lean
  - CompleteComplement.lean
  - Completion.lean
  - ConeSlot.lean
  - ConeTent.lean
  - ConstMulRight.lean
  - ConstScale.lean
  - ContinuousMoment.lean
  - ContinuousMomentAdd.lean
  - ContinuousMomentClamp.lean
  - ContinuousMomentClampValue.lean
  - ContinuousMomentExp.lean
  - ContinuousMomentFloor.lean
  - ContinuousMomentFloorReal.lean
  - ContinuousMomentGeneral.lean
  - ContinuousMomentGenFamily.lean
  - ContinuousMomentGenInjective.lean
  - ContinuousMomentGenLimit.lean
  - ContinuousMomentGenLinear.lean
  - ContinuousMomentGenNeg.lean
  - ContinuousMomentGenRate.lean
  - ContinuousMomentGenScale.lean
  - ContinuousMomentGenSub.lean
  - ContinuousMomentGenTail.lean
  - ContinuousMomentGenTwo.lean
  - ContinuousMomentLimit.lean
  - ContinuousMomentLinear.lean
  - ContinuousMomentMono.lean
  - ContinuousMomentNatExp.lean
  - ContinuousMomentNatLimit.lean
  - ContinuousMomentNatTail.lean
  - ContinuousMomentOne.lean
  - ContinuousMomentTailBound.lean
  - ContinuousMomentTwo.lean
  - ContinuousMomentValue.lean
  - ContinuousMomentValueAll.lean
  - ContinuousMomentZero.lean
  - ConvAutocorrFactor.lean
  - ConvMellinHat.lean
  - ConvMellinHatFactor.lean
  - ConvMellinHatIntWhead.lean
  - ConvMellinIntegrand.lean
  - ConvPartialInterchange.lean
  - ConvSummedIntegrand.lean
  - ConvTwTailIntU.lean
  - ConvTwTailSchedule.lean
  - ConvTwTermBound.lean
  - CoSupportChain.lean
  - CoSupportCompletion.lean
  - CoSupportDimension.lean
  - CoSupportDimThree.lean
  - CoSupportDistinct.lean
  - CoSupportEnergy.lean
  - CoSupportFamily.lean
  - CoSupportFunction.lean
  - CoSupportMember.lean
  - CoSupportPairing.lean
  - CoSupportPairwise.lean
  - CoSupportStrict.lean
  - CoSupportSubspace.lean
  - CoSupportTrivial.lean
  - CoSupportWeld.lean
  - CoupledWeilComplement.lean
  - CoupledWeilCrux.lean
  - CoupledWeilDiagDominant.lean
  - CoupledWeilDichotomy.lean
  - CoupledWeilGenuine.lean
  - CoupledWeilIndefinite.lean
  - CoupledWeilKernel.lean
  - CoupledWeilMono.lean
  - CoupledWeilOperator.lean
  - CoupledWeilPlaceValue.lean
  - CoupledWeilSonine.lean
  - CoupledWeilVHat.lean
  - CovarianceAtClampedInv.lean
  - CovarianceAtQk.lean
  - CovarianceAtRational.lean
  - CovarianceHead.lean
  - CovCombHbound.lean
  - CovCombScaleCont.lean
  - CovConnectClampedInv.lean
  - CovConnectPure.lean
  - CoxeterCandidate.lean
  - CruxFrontierN3.lean
  - CruxFrontierN4.lean
  - CruxFrontierN5.lean
  - CruxN5Closed.lean
  - CubicMember.lean
  - DeepMember.lean
  - DeepMemberFive.lean
  - DeepMemberFour.lean
  - DeepMemberSix.lean
  - DeepMemberThree.lean
  - DiagDominant.lean
  - DiagonalOperatorCore.lean
  - DigammaMidxCommon.lean
  - DilateTestBridge.lean
  - DilateTestFineDecay.lean
  - DilateTestRDecay.lean
  - DilMellinFEval.lean
  - DilMellinFRiwI.lean
  - DilTailCommute.lean
  - DilTailPartialClose.lean
  - DilTailUniformBound.lean
  - Divisors.lean
  - DlimBasisCore.lean
  - DlimCompletedInner.lean
  - DlimCompletionCauchy.lean
  - DlimCompletionComplete.lean
  - DlimCompletionCoord.lean
  - DlimCompletionCS.lean
  - DlimCompletionDense.lean
  - DlimCompletionLimit.lean
  - DlimCompletionPreHilbert.lean
  - DlimCompletionProj.lean
  - DlimCompletionSpace.lean
  - DlimHilbertCompletion.lean
  - DlimMultiplier.lean
  - DlimMultiplierAdjoint.lean
  - DlimMultiplierClosed.lean
  - DlimMultiplierSymm.lean
  - DlimProjHardening.lean
  - Dominance.lean
  - DurrmeyerCentral.lean
  - DurrmeyerConst.lean
  - DurrmeyerConverge.lean
  - DurrmeyerLinear.lean
  - DurrmeyerMoments.lean
  - DurrmeyerMomentSum.lean
  - DurrmeyerReconstruct.lean
  - DurrmeyerTendsTo.lean
  - DurrmeyerTest.lean
  - DurrmeyerWeights.lean
  - DyadicApprox.lean
  - DyadicClamp.lean
  - DyadicDense.lean
  - DyadicDenseReal.lean
  - DyadicDescent.lean
  - E8Seed.lean
  - FinAtlasOperator.lean
  - FinDirectLimit.lean
  - FinInnerProduct.lean
  - FiniteRankFubini.lean
  - FinPreHilbert.lean
  - Forced.lean
  - FrobForm.lean
  - GateA.lean
  - GateAFiniteList.lean
  - GateSanity.lean
  - GaugeTower.lean
  - GeneralWindowDilate.lean
  - GenSumCloseRlim.lean
  - GramSchmidt.lean
  - GramSchmidtConcrete.lean
  - GramSchmidtFamily.lean
  - GramSchmidtOrtho.lean
  - HaarInvariant.lean
  - HalfLineExhaustion.lean
  - HatVanishes.lean
  - HdecWeaken.lean
  - HeadTest.lean
  - HilbertGram.lean
  - HilbertPolyaBridge.lean
  - HilbertPolyaFinite.lean
  - HilbertPolyaMetric.lean
  - HilbertPolyaSpec.lean
  - HtileDischarge.lean
  - ImproperFinite.lean
  - ImproperScheduleIndep.lean
  - IntegralCell.lean
  - IntegralCS.lean
  - IntegralCSFull.lean
  - IntegralDist.lean
  - IntegralFiniteLin.lean
  - IntegralInversion.lean
  - IntegralInversionGeom.lean
  - IntegralMono.lean
  - IntegralPiece.lean
  - IntegralSplit.lean
  - IntegralTailBound.lean
  - IntervalAddTest.lean
  - IntervalMinorant.lean
  - IntervalPiece.lean
  - IntervalSplit.lean
  - IntervalSplitAt.lean
  - IntervalSplitAtCap.lean
  - IntervalTelescope.lean
  - IntervalUpperLip.lean
  - KillTest.lean
  - L2Complete.lean
  - L2Definite.lean
  - L2DefiniteDensity.lean
  - L2DefiniteIff.lean
  - L2ElementSpace.lean
  - L2MetricIff.lean
  - L2MomentBridge.lean
  - L2Separation.lean
  - Lattice.lean
  - LefschetzCoupling.lean
  - LogReflect.lean
  - MellinConv.lean
  - MellinConvFubini.lean
  - MellinConvGPull.lean
  - MellinConvInt.lean
  - MellinHat.lean
  - MellinHatBound.lean
  - MellinHatCovariance.lean
  - MellinHatDecayIndep.lean
  - MellinHatDilateCovarianceReal.lean
  - MellinHatDilateCovarianceRealClean.lean
  - MellinHatDilateCovarianceRealDerived.lean
  - MellinHatDilateCovarianceRealGe1.lean
  - MellinHatDilateCovarianceRealSeq.lean
  - MellinHatDilateScaled.lean
  - MellinHatIdBound.lean
  - MellinHatScaleCont.lean
  - MellinHatUniform1.lean
  - MellinInjective.lean
  - MellinInjectivePair.lean
  - MellinLinear.lean
  - MellinLinearNeg.lean
  - MellinMomentScaleLip.lean
  - MellinWindowDilate.lean
  - MomentCompletion.lean
  - MomentCovLip.lean
  - MomentCube.lean
  - MomentDecay.lean
  - MomentDefinite.lean
  - MomentDeterminacy.lean
  - MomentDurrmeyer.lean
  - MomentEnergyDetect.lean
  - MomentFiniteDiff.lean
  - MomentFunctional.lean
  - MomentGram.lean
  - MomentInvariant.lean
  - MomentInversionRaw.lean
  - MomentLaw.lean
  - MomentMember.lean
  - MomentMulConvDilated.lean
  - MomentNorm.lean
  - MomentPairing.lean
  - MomentPairingBilinear.lean
  - MomentPairingCS.lean
  - MomentPairingLaws.lean
  - MomentPairingNeg.lean
  - MomentProblemWellPosed.lean
  - MomentQuadratic.lean
  - MomentQuartic.lean
  - MomentQuintic.lean
  - MomentRangeNecessary.lean
  - MomentRealize.lean
  - MomentReconConverge.lean
  - MomentReconEnergy.lean
  - MomentReconSum.lean
  - MomentSquare.lean
  - MomentSummable.lean
  - MomentValue.lean
  - Monoid.lean
  - MulConv.lean
  - MulConvClampIndep.lean
  - MulConvCongr.lean
  - MulConvRLip.lean
  - MulConvRTest.lean
  - MultShift.lean
  - Pairing.lean
  - PairingBernBasisZero.lean
  - PairingBernOpZero.lean
  - PairingIUCongr.lean
  - PairingIUEnergy.lean
  - PairingIULinear2.lean
  - PairingIUReschedule.lean
  - PairingLimit.lean
  - PairingLimitI.lean
  - PairingMomentDeterminacy.lean
  - PairingMomentInjective.lean
  - PairingUnitCongr.lean
  - PairingUnitDist.lean
  - PairingUnitZero.lean
  - Parallelogram.lean
  - ParamIntegral.lean
  - Parseval.lean
  - PartialCoarseRefine.lean
  - PartialCommonRefine.lean
  - Pencil.lean
  - Polarized.lean
  - PolyDeterminacy.lean
  - PolyMember.lean
  - PolyMoment.lean
  - PreHilbert.lean
  - ProdParamTest.lean
  - Projection.lean
  - QCoSupportExists.lean
  - QHilbertBilinear.lean
  - QHilbertComb.lean
  - QHilbertForm.lean
  - QHilbertPos.lean
  - QHilbertSymm.lean
  - QHilbertTrunc.lean
  - QHilEVec.lean
  - QLinearKernel.lean
  - QPolyApart.lean
  - QPolyCoefCongr.lean
  - QPolyDimInv.lean
  - QPolyDistBridge.lean
  - QPolyMember.lean
  - QSumList.lean
  - RationalWindowDilate.lean
  - RationalWindowPower.lean
  - RealWindowIntegral.lean
  - RescheduleFinite.lean
  - RieszBessel.lean
  - RieszCoeff.lean
  - RieszDimInv.lean
  - RieszMoment.lean
  - RieszParseval.lean
  - RieszRealize.lean
  - RiwILimit.lean
  - RiwIMomentCovariance.lean
  - RiwSeqMoment.lean
  - ScaledTwistedTail.lean
  - SelfAdjoint.lean
  - SelfDualAutocorr.lean
  - SelfDualMomentSymmetry.lean
  - SelfDualPointwise.lean
  - SelfDualTest.lean
  - SeparableFubini.lean
  - SineSquareSOS.lean
  - SinglePrime.lean
  - SonineProjection.lean
  - Spectral.lean
  - StableInner.lean
  - StageG.lean
  - TailPartialScaleLip.lean
  - Tensor.lean
  - TentSlot.lean
  - TestAlgebra.lean
  - TwoSidedWeaken.lean
  - TwTailScaleCont.lean
  - TwTermDilateWindow.lean
  - TwTermMulConvDilated.lean
  - TwTermPowBand.lean
  - TwTermScaleLip.lean
  - UniformClosure.lean
  - UniformCompletion.lean
  - UniformPartialCap.lean
  - ValueInvolution.lean
  - WeilArchIdent.lean
  - WeilArchKern.lean
  - WeilArchKernCore.lean
  - WeilArchLimit.lean
  - WeilArchNear.lean
  - WeilArchNum.lean
  - WeilArchNumC.lean
  - WeilArchReconcile.lean
  - WeilArchRegSplit.lean
  - WeilArchSemantic.lean
  - WeilArchTailFar.lean
  - WeilArchTailLaws.lean
  - WeilArchTrunc.lean
  - WeilCoupledForm.lean
  - WeilCrossF.lean
  - WeilCrossFTwo.lean
  - WeilDensity.lean
  - WeilDominance.lean
  - WeilFormLaws.lean
  - WeilGeom.lean
  - WeilInvSqrt.lean
  - WeilInvSqrtTwo.lean
  - WeilLattice.lean
  - WeilMellinPole.lean
  - WeilPoleForm.lean
  - WeilPrimeShift.lean
  - WeilPrimeShiftAutocorr.lean
  - WeilPrimeShiftBridge.lean
  - WeilPrimeShiftCrux.lean
  - WeilPrimeShiftHaarForm.lean
  - WeilPrimeShiftNorm.lean
  - WeilPrimeShiftOperator.lean
  - WeilPrimeShiftRecip.lean
  - WeilPrimeShiftRecipAutocorr.lean
  - WeilPrimeShiftRH.lean
  - WeilPrimeShiftSonine.lean
  - WeilPSD.lean
  - WeilRecipCanon.lean
  - WeilRecipQ.lean
  - WeilRecipReal.lean
  - WeilShiftTest.lean
  - WeilStageFalsify.lean
  - WeilStageReport.lean
  - WindowDilatePow.lean
  - WindowMomentReflect.lean
  - WindowMomentScaleLip.lean
  - WindowPower.lean
- - Closure.lean
  - EulerProduct.lean
  - FurtherConstructions.lean
  - Siblings.lean
  - Signature.lean
  - Spectrum.lean
  - WalkCounts.lean
- Bridge.lean
- BridgeFF.lean
- CharOne.lean
- Crux.lean
- CycleCounts.lean
- Li.lean
- Mechanism.lean
- Template.lean
- audit_axioms.lean
- honesty_audit.sh
.gitignore
CHANGELOG.md
CITATION.cff
F1Square.lean
lake-manifest.json
lakefile.lean
lean-toolchain
LICENSE
README.md
ROADMAP.md

# Use via CDN

jsDelivr

jsDelivr serves any public GitHub repository as a CDN with zero setup. Pick a version and a file to get a ready-to-paste link and snippet.

Version

File

Link

Example

# Project Badges

DOI Visit

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

**An active research program toward `Spec ℤ ×_{𝔽₁} Spec ℤ` — the missing surface whose
intersection-positivity is the Riemann Hypothesis.**

> **Status: the Riemann Hypothesis is OPEN.** This repository is the research *base*, not a
> solution. It states the construction problem with precision and formalizes the honest status of
> every piece. The central open object — a 2-dimensional self-product of `Spec ℤ` over `𝔽₁` carrying
> an intersection pairing with a **Hodge index theorem** — is *named, shaped, and partially built*,
> not constructed. The crux is **never** asserted as proven anywhere in this repository.

## The problem, in one paragraph

Over a function field `C/𝔽_q`, the Riemann Hypothesis is a theorem: Frobenius acts on the étale
cohomology of `C × C`, and the **Hodge index theorem** (a positivity) confines its eigenvalues to the
critical circle. Over ℚ the analogous object is missing. RH is exactly the statement that a
still-unconstructed cohomology of "`Spec ℤ` as a curve over `𝔽₁`" carries a Frobenius (the scaling
flow) whose intersection-positivity holds. Every other ingredient — the characteristic-1 base, the
scaling flow, the prime orbits, the trace formula — is built. The one unbuilt thing is the
**2-dimensional square `Spec ℤ ×_{𝔽₁} Spec ℤ` with a Hodge index theorem**, and that
negative-definiteness *is* RH.

## What is in this repository

| path | what it is |
|---|---|
| [`F1Square.lean`](F1Square.lean) | Lean 4 formalization of the target object and its intersection theory (`UOR.Bridge.F1Square`), with the honest status of each result and a `F1SquareStatus` roll-up, now imports the proof layer and carries an elaboration-checked `example` tying each established field to a genuine theorem. |
| [`F1Square/`](F1Square/) | The **genuine-proof layer** — real Lean 4 theorems (no Mathlib, no `sorry`): the function-field Hodge mechanism (`Mechanism`, `Template`), the characteristic-1 base (`CharOne`), exact Bowen–Lanford counts (`CycleCounts`), the mechanism bridge + §2.3 control (`Bridge`), the crux stated faithfully (`Crux`), the tropical κ/spectrum stack incl. the κ⊥spectrum counterexample (`Tropical/`), and the analysis substrate — exact ℚ (a verified ordered field), a reflective ℤ ring normalizer with a from-scratch `ring` tactic (`ring_uor`), constructive ℝ as Bishop regular sequences and ℂ = ℝ×ℝ — both **commutative rings up to `≈`** (multiplication well-defined on the setoid, with associativity and distributivity, via a linear-bound criterion built on the generalized Archimedean lemma), ℝ is **Cauchy complete** (every regular sequence of reals converges to its diagonal limit, choice-free), and the **transcendentals are built from first principles** (`Analysis/`) — beginning with Euler's number `e = Σ 1/i!` and the general exponential `exp(q) = Σ qⁱ/i!` on the rational interval `[0,1]`, both via the exponential series with a rigorous rational error bound (the `exp(q)` bound reuses `e`'s tail bound by termwise domination, `qⁱ/i! ≤ 1/i!`), and extended below to all of ℝ. The **λₙ / RH proof boundary** is now pinned faithfully (`Li`): by Li's criterion RH ⟺ `λₙ > 0 ∀ n ≥ 1`, stated as `LiPositive` on the (unconstructed) genuine ζ-derived Li sequence — the **analytic face** of the crux, encoded open (`none`), with a finite-check guard (`LiPositive = ⋀ all finite truncations`, so no `decide` is a proof) and the Bombieri–Lagarias / Weil-explicit-formula substrate stated as honest interfaces. **ζ and λₙ ship as exact-bounded objects** (`ExactBounded`, `Zeta`): a constructive real is a stream of certified rational enclosures of width `2/(n+1)`, and `ζ(s) = Σ 1/iˢ` for integer `s ≥ 2` is a concrete such object (with a rigorous rational tail bound) — honestly in the convergent regime `Re(s) > 1` only (no zeros; the critical-strip continuation and the genuine `λₙ` values are deferred, not fabricated). ℝ carries a genuine **order `≤`** (`ROrder`): the Bishop `xₙ ≤ yₙ + 2/(n+1)`, reflexive, antisymmetric up to `≈`, and transitive via the Archimedean lemma. ℝ is now a constructive **field with powers** (`Pow`, `Inv`): real powers `Rpow`, the reciprocal `1/x` of a positive real (positivity-as-data, full Bishop regularity), and division `Rdiv`. And the **everywhere-defined exponential `exp` on ℝ** (`ExpReal`) is built as the diagonal of rational partial sums `S_{R j}(x_{R j})` — itself a Bishop-regular sequence of rationals, so a constructive real directly (no limit needed), rigorous via three rational bounds on `expSum`: a geometric truncation tail, a uniform Lipschitz bound, and a factorial-growth estimate. The **transcendentals are now complete** (v0.13.0): **`cos`/`sin`** (`CosSin`) as the alternating diagonal `Σ(−x²)ⁿ/(2n+off)!` dominated by `exp(M²)`, and **`log` on positive reals** (`Log`) as `2·artanh((x−1)/(x+1))` — the artanh odd series on every `[−ρ,ρ]` (`ρ<1`) tamed by a general Bernoulli reindex, composed with the Möbius t-map `q↦(q−1)/(q+1)` (cleared difference identity, 2-Lipschitz on `x≥0`, range bound keeping the argument in `[−ρ,ρ]`). `log` is genuine **positivity-as-data** — the *same* idiom as the reciprocal `Rinv`: from a witness `x_k > 1/(k+1)`, `RlogPos x k` **derives** the rational modulus `1/M ≤ x ≤ M` (`M = |x₀| + 2 + 1/L`, `L = δ/2` the witness floor) rather than demanding it of the caller (constructively a modulus is *necessary* — `log` has no uniform modulus of continuity on `(0,∞)`). The example binds `log 2` built through this path. The **analytic constants of the Li/Keiper bridge** are now built (v0.14.0): **π** (`Pi`) via Machin's `16·arctan(1/5) − 4·arctan(1/239)` as one Bishop-regular diagonal (with `π ≥ 6/5` for `Pos π` and the tight `π ≤ 3.142` from the alternating arctan truncation at the tightest radius), the clean logs **`log 2`/`log π`/`log 4π`** with kernel-certified upper bounds (`log 2 ≤ 0.6931`, `log π ≤ 1.1453`; the varying `π`-argument is dominated by the constant `15/29 = tmap(22/7)` then geometrically truncated), and the **convergence-accelerated Euler–Mascheroni constant** `γ = Σ(1/i − 2·artanh(1/(2i+1)))` with `γ ≥ 0.54` — feasible where the alternating-ζ-series `γ` is not (that series' running `lcm` denominator already has ~7000 digits at depth 2). These culminate in the **first Li/Keiper coefficient `λ₁ = ½·(2 + γ − log 4π)` as a *positivity-certified* constructive real**: `Rlambda1_pos : Pos Rlambda1` (`λ₁ ≈ 0.0231 > 0`), carried through the ℝ-order bridges. This realizes the `n = 1` slice of Li's criterion as **evidence** — it does **not** assert `λₙ > 0 ∀ n` (which *is* RH); the crux stays `none` and RH stays open. The **complex analytic engine — exponential core** is now built (v0.15.0): `exp` is a genuine **homomorphism on all of ℝ** (`ExpRealAdd`, `RexpReal_add : exp(x+y) ≈ exp x · exp y`), the diagonal lift of the rational Cauchy-product functional equation (signed corner bound → deep-reference reconciliation); the **Pythagorean identity `cos² + sin² ≈ 1`** (`CosSinAdd`) via the trig Cauchy product, giving `|cos|,|sin| ≤ 1` (`CosSinBound`); the **complex exponential** `Cexp z = exp(re z)·(cos(im z) + i·sin(im z))` (`ComplexExp`); and `nˢ = Cexp(s·log n)` (`ComplexPow`) with the **modulus identity** `|Cexp z|² = (exp Re z)²` (`ComplexMod`) — the squared modulus depends only on `Re s`. The **ζ-convergence gate `exp∘log = id`** is now closed (v0.15.1): the power-series composition identity **`exp(2·artanh τ) = (1+τ)/(1−τ)`** (`Rexp_two_artanh_ofQ`) — composing the exp factorial series with the artanh geometric series from scratch (corner bound `exp_corner_le`, rational identity `exp_artanh_rat_cleared`, diagonal reconciliation `Rexp_two_artanh_via`) — and its corollary **`exp(log n) = n` for the *literal* `Rlog` term** (`Rexp_log_nat_Rlog`: `RexpReal (Rlog (ofQ n) …) ≈ n`; the radius-general construction matches `Rlog`'s own convergence radius by definitional equality, so no `τ²≤½` smallness is needed), both axiom-clean. This unlocks the squared-modulus tail `|n^{-s}| = n^{-Re s}`. **ζ for complex argument is now built (v0.15.2):** `Czeta s = Σ_{n≥1} n^{-s}` for *complex* `s` with `Re s > 1` (witnessed by a rational `τ > 0`, `τ ≤ (Re s − 1)·log 2`) is a genuine constructive ℂ — its real and imaginary parts are Bishop diagonal limits (`Rlim`) of the reindexed dyadic partial sums `Σ_{n<2^{M(j)}} Re/Im(n^{-s})`, converging with the canonical rate `2/(k+1)` (`Czeta_re/im_tendsTo`). The convergence proof is the full dyadic-geometric stack: log-multiplicativity `log(2ᵏ) = k·log 2` via exp injectivity (`RexpReal_inj`, re-routing the artanh addition boundary wall), the block modulus bound `≤ ofQ(rᵏ)` (`r = 1/(1+τ) < 1`), the geometric tail `Σ rᵏ ≤ rʲ/(1−r)` (`geoFrom_le`), the Bernoulli reindex `r^{M(j)}/(1−r) ≤ 1/(j+1)` (`geom_reindex`, `M(j) = (j+1)·r.den²`), and the completeness bridge `seq_diff_le`/`RReg_of_real_bound` (a real bound becomes the rational Cauchy condition `RReg`) feeding Bishop's `Rlim`. This is ζ across its *full* convergent half-plane `Re s > 1` (no zeros), not merely integer `s ≥ 2`; the critical-strip continuation and the genuine `λₙ` stay deferred (`liPositivityHolds = none`, RH open); nothing is faked. The **explicit formula's arithmetic ingredient is now built (v0.15.3):** the **von Mangoldt function** `Λ` (`Mangoldt`, via the smallest factor `spf` — `Λ(4) = log 2`, `Λ(6) = 0`, `Λ ≥ 0`, computable so the values hold by reduction) and the **prime side** `Σ_p Σ_k log p · h(k log p) = Σ_{n≥2} Λ(n)·h(log n)` (`primeSide`) — a finite sum for compactly-supported `h` (constant past the support cutoff, `primeSide_stable`), hence a genuine real. And the **Bombieri–Lagarias decomposition of `λ₁`** (`LiOne`, `Rlambda1_decomposition`): `λ₁ = λ₁^{arith} + λ₁^{∞} = γ + (1 − γ/2 − ½·log 4π)`, the finite/arithmetic place `S_f(1) = −η₀ = γ` plus the archimedean `S_∞(1)`, **promoting `Li.LiDecomposition` from the trivial inhabitant `λ = λ + 0` to a proven non-trivial instance** (`li_decomposition_realized`) whose `n = 1` slice is the genuine two-place split (deriving `γ` from the prime sum needs `ζ'/ζ` continuation, deferred and faithfully labelled, not fabricated; the crux stays `none`, RH open). **Stage B is now complete (v0.16.0)** — the three goals: **(B) `ζ(s)` on the critical strip `0 < Re s < 1`** via the integration-free **Dirichlet-eta** route, where `η(s) = Σ(−1)^{n−1}n⁻ˢ` converges by bounded variation across the whole strip the raw `ζ` series cannot reach: `Ceta` (`EtaVariation`) is `η(s)` for every `Re s > 0` as a constructive ℂ (the diagonal limit of the reindexed paired partial sums through the full dyadic-geometric `RReg` stack adapted to `σ > 0`), and `CzetaStrip` (`CriticalZeta`) is `ζ(s) = η(s)/(1 − 2^{1−s})` with the non-vanishing `etaDenom_Pos_normSq` (`|1 − 2^{1−s}|² ≥ (2^{1−σ}−1)² > 0`, the spurious zeros all on `Re s = 1`) and the certificate `CzetaStrip_functional : (1 − 2^{1−s})·ζ ≈ η` — the real/imaginary parts are `ExactBoundedReal` automatically; **(A) the archimedean `Γ′/Γ` place** (`Gamma`): the single real-power combinator `RrpowPos x y = exp(y·log x)` (so `√(2π) = exp(½·log 2π)` — no sqrt primitive, no complex `Clog`), the **exact** digamma `ψ = Γ′/Γ` (`Digamma`, the convergent series `−γ + Σ[1/(n+1) − 1/(n+z)]` → `RReg`/`Rlim`, reusing `Rgamma_h`), and `SpougeGamma`, Spouge's `Γ`-approximant built only from `exp`/`log`/reciprocal of positive reals (Spouge's explicit relative-error bound is cited, not formalized — a rigorous proof presupposes an independent `Γ`, so the exact archimedean place is carried by `Digamma`); **(C) `Pos λ₂`** (`LambdaTwo`, `Rlambda2_pos`, certified `λ₂ ≥ 0.0043`; true value `λ₂ ≈ 0.0923457`) — the higher-Stieltjes-`γₙ` → `λₙ` capstone, a `λ₁`-style positivity certificate at `n = 2`, **evidence** for Li's criterion (not the crux): `liPositivityHolds` stays `none`, `λₙ > 0 ∀ n` (= RH) and the off-line zeros remain deferred, RH open. **Stage C is now complete (v0.17.0)** — the **canonical arithmetic square `𝕊 = Spec ℤ ×_𝔽₁ Spec ℤ` is constructed and mechanized** (`Square/`): Deitmar 𝔽₁-algebras are commutative monoids and `𝔽₁` (the trivial monoid) is proved **initial**, so the tensor `F ⊗_𝔽₁ F` is the plain coproduct — realized as `ℕ₊ × ℕ₊` with the **universal property proved** (`copair_unique`; canonicality = the universal property, not a candidate model), strictly 2-dimensional (`gen2_injective` — the §3.1 ℤ-collapse avoided by theorems), projections recovering the curve; the **intersection lattice is derived, never entered by hand** (every primitive number a point count with translation-pencil moving, `Δ² = 0` from the parallel-pencil disjointness itself, `E₃² = −2` forced by bilinearity, the sourced product-of-curves template **emerging** as a consistency theorem `sqPair_eq_template`, the five §2.2 gate self-checks as theorems, the class lattice finitely generated); the **parallel pencil carries the arithmetic as constructive-real shift lengths** (`pencil_separation`: constant `log n`; `= Λ(p) = log p` at primes — the explicit-formula prime weight, reached geometrically); and the polarized instance `squarePolarized` (now `𝕊`'s own lattice) satisfies the **Hodge index** (`square_hodgeIndex`) — **which is provably pencil-blind** (`square_hodge_pencil_blind`: `[Γ_n] = [Δ]`, `Δ·Γ_n = 0` ∀n — no spectral input, the §2.3-control geometric face), so it is **not** the crux: the crux is the Hodge index / Weil positivity of the `H¹`-bearing pairing (⟺ `λₙ ≥ 0`), `hodgeIndexHolds`/`liPositivityHolds` stay `none`, RH open. **Stage D is now complete (v0.18.0)** — **the bridge and the crux attempt**: the function-field anchor is a genuine lattice derivation (`BridgeFF.ff_hodge_iff_hasse`: Hodge-index negativity on the primitive `{Δ,Γ}`-span ⟺ the Hasse bound `a² ≤ 4q`, with the trace datum `Δ·Γ = q+1−a` inside the lattice — the v0.1.0 governor is now DERIVED); the λ₂ Bombieri–Lagarias split is a theorem (`Rlambda2_decomposition`) and `Li.LiDecomposition` is realized with two genuine certified slices; **the geometric and analytic faces of the crux are proven equivalent** (`Square/Spectral.lean`: the `SpectralSquare` interface with the dictionary `⟨Cₙ,Cₙ⟩ = −2λₙ`, and `crux_faces_equivalent : SpectralCrux S ⟺ Li.LiCrux S.lam` — a genuine constructive theorem), inhabited with the certified `λ₁, λ₂` (`⟨C₁,C₁⟩ < 0`, `⟨C₂,C₂⟩ < 0`) and guarded by theorems (`spectralTwoSlice_not_crux`: no finite assembly of certified slices can be passed off as RH); and **the crux attempt ran under the gate** (`Square/Attempt.lean`): certified through `n = 2`, frontier exact (`crux_attempt_frontier`: the crux ⟺ `∀ n ≥ 3, λₙ > 0`; the next slice needs the second Stieltjes constant `γ₂`), post-mortem recorded — **the universal did not close**, so `hodgeIndexHolds`/`liPositivityHolds` stay `none` and RH stays open, with the bridge substrate shipped exactly as scoped. **Stage E is now complete (v0.19.0)** — **completion**: the **explicit-formula trace is completed** (`Analysis/LiComplete.lean`: `Li.ExplicitFormulaTrace` realized with the genuine three-sided reading at both built slices — zero side `λ₁`/`λ₂` whose sum-over-zeros reading is [CLASSICAL] BL 1999, finite-place closed forms, archimedean parts — packaged as the `WeilTrace` ladder `weilTraceTwo`), the **remaining `Li` interfaces are retired at the built slices** (`liAgreesWith_two_realized`: the direct certified builds agree non-reflexively with the BL closed-form assemblies; the `Li.lean` realization ledger records that every interface is realized exactly as far as the built slices reach), and **THE DOMINANCE FACE** is proven (`Square/Dominance.lean`): the crux as ONE uniform bound — `Dominated` (a single `B` with `−B(n) ≤ λₙ^{arith}` and `λₙ^{∞} − B(n) > 0`, sign-agnostic, no enumeration) with **`dominance_crux_equivalent`: `Dominated ⟺ SpectralCrux ⟺ LiCrux`** — the crux now has **three provably equivalent faces**, and the assembly shape is exact (`crux_closure_route`: the certified head plus one tail bound from `n = 3` on yields the crux). The classical sourcing is deep-research-verified against the primary PDFs (Voros's strict dichotomy, *MPAG* 9 (2006) — tempered `½n(log n − 1 + γ − log 2π)` under RH vs exponential oscillation under ¬RH, no third option; Lagarias, *Ann. Inst. Fourier* 57 (2007) — the archimedean trend `(n/2)log n + cn`, `c = (γ−1−log 2π)/2`, **unconditional**, and the `O(√n·log n)` excursion bound, a theorem under RH): `Dominated`(genuine parts) is TRUE iff RH — both directions — and **no unconditional tail bound exists in the verified literature**, so the non-closure of the crux is a *sourced result*. The final roll-up records the **v1.0.0-candidate state**: complete construction, honest crux — every surrounding field `some true`, `hodgeIndexHolds`/`liPositivityHolds` stay `none`, **RH stays open**, the open content one proposition with three faces, relocated into a single object (the tail bound for the genuine parts, governed by the zeros' location). **The genuine-pairing arc completes the release** — **the Weil functional is assembled** (`Analysis/Weil.lean`, `Square/Pairing.lean`): in the pinned Connes–Consani normalization, `W(f) = poles − (primes + archimedean)` with **the zero side as the defect of the built sides (no zeros as inputs)** — the whole finite-place side `Σ_{n≤X} Λ(n)(f(n)+n⁻¹f(1/n))` and the archimedean constant `(log 4π+γ)f(1)` CONSTRUCTED (the two integral components stay interface: their piecewise-linear closed forms are unverified in print), on a test class (piecewise-linear, rational breakpoints — via the new tent calculus `Rabs`/`RmaxZero`) that is admissible to Weil's criterion directly (Bombieri's Clay class `W`); **the fourth face**: `weilSpectralSquare` — the first `SpectralSquare` whose `cSq` comes from a pairing-valued assembly — with `weil_strict_iff_crux`: positivity of the pairing family ⟺ the crux ⟺ Li positivity ⟺ dominance (for the genuine family this is Weil positivity = RH; Weil 1952/Burnol math/9810169, both directions elementary, deep-research-verified); the **first computed pairing value** (`weilPrime_demo`: the finite-place side at the tent peaked at 2 is exactly `log 2` — the pairing sees the prime); and the **unconditional territory recorded** (Connes–Consani's prime-free window `[2^{−1/2}, 2^{1/2}]`, Selecta Math. 27 (2021); Burnol's explicit multiplier `α(τ) = 8√2cos(τ log 2)/(1+4τ²) + h₊(τ)` as the pinned next mechanization target). **The crux is ONE proposition with FOUR provably equivalent faces; it closes iff RH is proven; the fields stay `none` until then — complete construction, honest crux.** |
| [`scripts/honesty_audit.sh`](scripts/honesty_audit.sh) | The mechanized-honesty gate (run in CI): `#print axioms` over **every** proof-layer theorem must show only `{propext, Quot.sound}` — the proof layer is **choice-free** (`Classical.choice` is eliminated; the two surviving axioms are forced by `omega`/`simp`/`Int` core internals and constructively uncontroversial) — no `sorry`, no `native_decide`, no stray axioms. Coverage is **self-enforcing**: the gate fails CI if any non-private proof-layer theorem is left un-audited. |
| [`docs/f1_square_intersection_theory.md`](docs/f1_square_intersection_theory.md) | Precise specification of the target object (§1), the candidate-construction gap table (§2), the named obstructions (§3), and the T1–T5 verification ladder (§4). |
| [`docs/missing_object_over_Q.md`](docs/missing_object_over_Q.md) | The four equivalent solution routes and the `λₙ` / Hodge-index convergence map. |
| [`docs/characteristic_1_constructions.md`](docs/characteristic_1_constructions.md) | The verified characteristic-1 / tropical stack (R1–R16) that supplies the 1-dimensional arithmetic-site curve. |

## The epistemic convention

The formalization is deliberately honest about what is and is not established. It mirrors the
convention of the upstream UOR-Foundation library:

- `universallyValid := some true` ⇒ asserted established (verified in a runtime, or a classical
  theorem, cited).
- `universallyValid := none` ⇒ **not** asserted proven in this encoding (open or conditional).

The open crux — the Hodge index theorem for the square, which is RH — is encoded with `none` because
it is open. The mechanized audit ([`scripts/honesty_audit.sh`](scripts/honesty_audit.sh)) makes this
honesty a **verifier, not a prohibition**: it forbids `sorry` / `native_decide` / stray axioms in the
proof layer, not a genuine proof. No field asserts an unproven claim as true; if the crux is ever
genuinely (axiom-clean, faithfully) proved, its status becomes `some true` because that is then the
truth. Results that *are* established
(the intersection-pairing template, the ample class on the template, the parallel-pencil structure)
carry their genuine status; the crux does not.

## Dependency

The Lean formalization extends the **UOR-Foundation** library and is pinned, for reproducibility, to
[`UOR-Framework` **v0.5.2**](https://github.com/UOR-Foundation/UOR-Framework/releases/tag/v0.5.2) —
the latest UOR-Framework release that ships the `lean4/` library. The exact revision is frozen in
[`lake-manifest.json`](lake-manifest.json).

## Building

Requires [`elan`](https://github.com/leanprover/elan) (the Lean toolchain manager). The toolchain
version (`leanprover/lean4:v4.16.0`) is read from [`lean-toolchain`](lean-toolchain).

```sh
lake update   # resolve and fetch the pinned `uor` dependency (first time only)
lake build    # compile F1Square against UOR-Framework v0.5.2
```

CI runs `lake build` on every push and pull request.

## Versioning

This project uses [Semantic Versioning](https://semver.org), starting at **v0.0.1**. See
[`CHANGELOG.md`](CHANGELOG.md) for the release history and [`ROADMAP.md`](ROADMAP.md) for the remaining
construction of the F1 square, scoped into releases v0.15.0–v0.22.0 (the crux stays `none` until RH is
genuinely proven — v0.20.0 derives the Hodge-index dictionary `⟨Cₙ,Cₙ⟩ = −2λₙ` as a theorem and the
gate locates the frontier: the forced signature is exactly `λₙ > 0 ∀n` = RH, still open; v0.20.0 also
constructs the second Stieltjes constant `γ₂` and closes its numeric bracket `γ₂ ≥ −0.02`
(`Rgamma2_ge_neg002`, discrete Euler–Maclaurin) — a certified constant bound, not a positivity-of-all-`λₙ` claim;
v0.21.0 ships stage G — the missing-object embedding route and the UOR Atlas formalized as facets of one `{T,O}`-object —
which **localizes** the crux to the prime–archimedean coupling sign, the fields still `none`, RH still open).
v0.22.0 is the **final** planned release: it carries both Track 1 (discharging the Bombieri–Lagarias /
Voros classical interfaces) and Track 2 (the `α`-band / Sonine-projection crux frontier; the post-v0.21.0
thread already proves `α(2) < 0` — the archimedean multiplier is pointwise *indefinite*, the obstruction
to single-place positivity), pursued to exhaustion until the crux closes or the work is published.

## Publishing (Zenodo)

This repository is prepared for archival on [Zenodo](https://zenodo.org) the same way
`UOR-Framework` is: metadata flows from [`CITATION.cff`](CITATION.cff) (no `.zenodo.json` is used),
and a tagged GitHub release triggers a DOI. The remaining, account-gated steps for the maintainer:

1. Confirm the `repository-code` URL in `CITATION.cff` matches the published GitHub repo.
2. Enable the repository in the Zenodo ↔ GitHub integration.
3. Tag and publish the current release: `git tag -a vX.Y.Z -m "vX.Y.Z" && git push --tags` (with the
   version being released), then create the GitHub release for that tag.
4. After Zenodo mints the DOI, add a `doi:` field (the concept DOI) to `CITATION.cff` in a follow-up
   commit — exactly the pattern UOR-Framework follows.

## Citation

See [`CITATION.cff`](CITATION.cff). Until the first Zenodo deposit assigns a DOI, cite the repository
and the current release tag (e.g. `v0.21.0`).

## License

F1

Owner Repos

File Explorer

# Use via CDN

# Project Badges

Was this content helpful?

Recent Feedback

F1

Owner Repos

File Explorer

# Use via CDN

# Project Badges

Was this content helpful?

Recent Feedback

Download README