低能系列 2 · 2026-10-11
两负一正,裸迹宣誓
有序闭迹与整球响应曲率
Two Minuses, One Plus, and a Bare Trace Under Oath: Ordered Closed Traces and Whole-Ball Response Curvature
- 6条主张
- 46个 Lean 模块
- 567个声明
- ✓ 内核检查全部通过
摘要
单位矩阵登台,裸迹报出 ,原归一准备态报出 :两者分别评价全物质载体的迹与固定准备中的作用。对固定的 外源及同向读出算子、零输出动量、双 Laplace 参数 、同一准备和半径 的入射/观察双球窗,我们证明:完整五项响应中,未中心化(raw)与中心化(connected)的二次系数张量均为两负一正。这里的“曲率”是扣除尖窗非解析一次项后的二次系数,不是完整响应在原点的 Hessian。
展开全文
两条支路从同一个含独立对偶物质场的作用出发;该作用及其背景、物质载体与常数由共同源数据生成,没有拟合参数。在 分级下,任意有限合法有序规范传播词的闭迹等于其块对角部分的闭迹;规定的单向标量插入闭迹为零,两次同向插入之间夹任意合法传播词的开放链亦为零。准备态、边界权 与完整二次量子化词给出不同的评价;实际返回算子产生非零读数,中途准备投影则将它抹去。场方程支路从 场的辅助、Ward 与对称约化得到 场系统,将物质反馈计入一次,构造有理 维玻色核及场/外源恢复映射。原点物质块秩为 ,保留六个轻物质方向后得到 维二阶系统;其常项秩为 ,五维轻核同时给出线性与二次动量时间尺度,并由动态 源读出传播。
两条量子源腿、读出接触项和两条场传播腿组成完整五项响应。真实球交集的非解析一次项、完整复 Gram、隐式根导数、成对标架的全方向积分及向外有理余项共同确定二次张量。raw 三轴系数依次落在 、、 乘 的原作用单位区间内;全部混合项另有统一界,使惯性结论适用于完整张量。均值项(mean)独立保留,其第二轴区间跨零。
同一原作用的真实 Fourier Hessian还认回完整289场矩阵。五原点方向与98维坐标补空间生成全四复动量的精确Schur核、源生可逆半径和严格三阶余项,实际有序电流恢复带原分母的全场,接触与九零方向一并保留。另一原配置准备的完整有序五因子,经真实Noether接触与四个Fourier键生成实场半轴响应算子;同一历史被源生成的创建单位态/背景差读口消费后,在正的源生非线性时窗内产生完整 量子张量 ,母Euler幅度导数的有限积分严格为 。同钟 ,完整线性化半轴保自身增长条件。新准备的响应由同一原Green返回全部场,其条件与指定双球窗分别陈述。
主张与证明
每条主张都登记在逐主张映射中。展开一条,可以看到它的陈述、在论文中的位置,以及证明它的 Lean 模块与复现程序。
按阅读顺序排列。黑孔:Lean 证明,内核检查已通过;灰孔:由复现程序支撑,不含 Lean 声明。
Q1任意有限合法有序Dirac词的闭迹与单向标量§3
Lean 模块 · 3
复现程序与证据 · 1
Q2完整Fock词的原准备与独立对偶读回§4
Lean 模块 · 5
复现程序与证据 · 1
Q3一次物质反馈、五轻核与原场/源恢复§5
Lean 模块 · 12
复现程序与证据 · 8
Q4指定双球窗完整五项与全张量惯性§6
复现程序与证据 · 4
Q5同原作用的完整四动量Schur与实际清分母全场恢复§12.1
Lean 模块 · 4
LowEnergy.AlphaSource.CanonicalPreparationSourceFullOriginInverse38 个声明
flagprojectionoriginTermsinverseTermsinverseorigin_generatedinverse_leftinverse_left_supportinverse_right_supportcomponentInverseTermscomponentOriginTermscomponentFlagcomponentInversecomponentOrigincomponentProjectioncomponent_inverse_leftcomponent_inverse_left_supportcomponent_inverse_right_supportcomponent_inverse_crossfullComplementFlagfullComplementProjectionfullOriginTermsfullOriginfullInversefullProjection_sumfullProjection_piecepiece_fullProjectionfullOrigin_sumfullOrigin_generatedfullInverse_leftfullInverse_left_supportfullInverse_right_supportfullProjection_squarecomplementKerneloriginInverseoriginInverse_leftoriginInverse_rightorigin_determinantLowEnergy.AlphaSource.CanonicalPreparationSourceFullOriginSchur72 个声明
dualInjectionTermsdualInjectionfullKernelTermsfullKernelFramefullKernel_generatedfullKernel_origincomplementRegularcomplementOrigincomplementKernel_continuouscomplementRegular_near_origincomplementGreencomplementKernel_rightcomplementKernel_leftcomplementGreen_left_supportcomplementGreen_right_supportcomplementGreen_leftcomplementGreen_rightcomplementGreen_origineffectiveReadereffectiveKerneleffectiveFramenativeEffectiveFrameeffectiveKernel_frameeffectiveReader_complementeffectiveKernel_generatedeffectiveKernel_origincomplement_responsefrozenTensoreffectiveKernel_complete_returnfullInverseTermsfullInverse_generatedfullLeadingTermsfullHigherTermsleadingTensorhigherTensorfullResidualTermsfullInverseResidualTermsfullResidual_generatedfullInverseResidual_generatedfrozenTensor_generatedleading_degreeshigher_degreeseffectiveKernel_source_tensorinverseBudgetsourceRadiusinverseBudget_ge_onesourceRadius_possourceRadius_le_onefullComplementProjection_pricefullInverse_priceoriginInverse_pricecomplement_delta_pricesource_neumann_pricesourceRadius_regularcontrolledPointcomplement_full_inverse_pricecomplementGreen_priceinversePrice_exactsourceRadius_exactcomplementGreen_deltacomplementGreen_delta_pricekernelBudgethigherBudgeteffectiveErrorBudgetkernelBudget_nonneghigherBudget_nonnegfullKernel_pricehigherTensor_priceeffectiveKernel_leading_priceeffectiveErrorBudget_nonnegkernelPrice_exacthigherPrice_exactLowEnergy.AlphaSource.CanonicalPreparationSourceFullOriginCurrent34 个声明
active_squareactive_nullactiveKernel_rightselectorTermsmodeSelectorblockCoordinatesblockComplementblockComplement_supportedblockComplement_generatedeffective_actual_equationeffective_field_reconstructionfullKernel_coordinatesfullKernel_independentactualMomentumactualCurrentactualCosourceactualNativeFieldactualFieldactualForcingactual_current_wardactual_whole_nativeactual_sourceactual_insideactual_effective_dynamicsactual_complement_returnactual_native_reconstructionorigin_kernel_completeactual_forcing_twoSectorsactual_whole_reconstructionfullNativeOriginTermsfullNativeOriginfullNativeOrigin_generatedactual_origin_kernel_readactual_effective_response_price
Q6真实Noether有序准备的半轴、实际非线性全289量子窗与原场返回§13.1
Lean 模块 · 23
LowEnergy.AlphaSource.CanonicalPreparationSourceHalfAxisCurrentOperator15 个声明
sourceWeightedCurrentsourceWeightedCurrent_generatedsourceCurrentPricesourceCurrentPrice_nonnegativesourceWeightedCurrent_pricesourceWeightedCurrent_continuoussourceWeightedCurrent_integrablesourceHalfCurrentsourceHalfCurrent_generatedsourceWindowJacobian_integralsourceCurrentTailPricesourceHalfCurrent_tailsourceHalfCurrent_pricesourceCurrentTailPrice_zerosourceWindowJacobian_operatorNormLowEnergy.AlphaSource.CanonicalPreparationSourceHalfAxisFieldOperator15 个声明
sourceHalfFieldOperatorsourceHalfCurvatureOperatorsourceFieldOperatorFactorsourceCurvatureOperatorFactorsourceHalfFieldOperator_generatedsourceHalfCurvatureOperator_generatedsourceHalfFieldOperator_tailsourceHalfCurvatureOperator_tailsourceHalfFieldOperator_pricesourceHalfCurvatureOperator_pricesourceHalfFieldOperator_nativesourceFieldJacobian_operatorNormsourceCurvatureJacobian_operatorNormsourceHalfCurrent_realitysourceHalfCurvatureOperator_mateLowEnergy.AlphaSource.CanonicalPreparationSourceNativeRealFourierSignal14 个声明
sourcePhasesourcePhase_applysourcePhase_coordinatesourceRealSignalsourceSignalAmplitudesourceRealSignal_smoothsourceRealFirstJetsourceRealSecondJetsourceRealSignal_firstJetsourceRealSignal_secondJetsourceRealJet_coefficientsourceRealEuler_FouriersourceRealSignal_originalDensitysourceRealSignal_originalEulerLowEnergy.AlphaSource.CanonicalPreparationSourceOrderedSignalOperator18 个声明
SignalAmplitudeSourceOpsourceHistoryInputsourceHistoryInput_actualsourceHistoryInput_continuoussourceRightDrivesourceLeftDrivesourceRightDrive_continuoussourceLeftDrive_continuoussourcePrimalOperatorsourceIndependentDualOperatorsourcePrimalOperator_actualsourceIndependentDualOperator_actualsourceMiddleOperatorsourceHistoryOperatorsourceHistoryOperator_actualsourceCurrentOperatorsourceCurrentOperator_actualLowEnergy.AlphaSource.CanonicalPreparationSourcePreparedSignalEuler13 个声明
sourceSignalDurationsourceSignalDuration_positivesourceSignalCurrentsourceRawSignalEuler_generatedsourcePreparedQuadrature_generatedsourceSignalCurrent_actualsourceSignalOrdinaryRemainder_generatedsourceSignalForcingsourceSignalFieldsourceSignalForcing_actualsourceSignalField_nativesourceSignalField_native36sourceSignalForcing_cosourcesLowEnergy.AlphaSource.CanonicalPreparationSourceNativeSignalLaplaceReturn20 个声明
sourcePlaneWindowScalarsourceNativePlaneWindowsourceNativeBoundarysourcePlaneWindowScalar_derivativesourceNativeBoundary_initialsourceNativePlaneWindow_ordinarysourceNativeSignal_weightedsourceNativeEulerWindowsourceNativeEulerWindow_actualsourcePreparedEulerWindowsourcePreparedEulerWindow_generatedsourcePreparedEulerWindow_nativesourceNativeTimeValuesourceNativeTimeFirstsourceNativeTimeValue_actualsourceNativeTimeFirst_actualsourceNativeBoundary_historysourcePlaneHalfScalarsourcePlaneHalfScalar_actualsourcePlaneWindowScalar_limitLowEnergy.AlphaSource.CanonicalPreparationSourceSignalOperatorPrice22 个声明
sourceClockGrowthsourceClockGrowth_nonnegativesourceHistoryInput_pricesourcePrimalCoefficientsourceDualCoefficientsourceRightDrive_pricesourceLeftDrive_pricesourcePrimalOperator_pricesourceIndependentDualOperator_pricesourceMaterialMapsourceContactMapsourceMiddleOperator_source_mapssourceMiddleCoefficientsourceMiddleOperator_pricesourceHistoryLinearCoefficientsourceHistoryConstantCoefficientsourceHistoryOperator_pricesourceCurrentLinearCoefficientsourceCurrentConstantCoefficientsourceCurrentCoefficient_nonnegativesourceCurrentOperator_pricesourceCurrentOperator_continuousLowEnergy.AlphaSource.CanonicalPreparationSourceSignalCausalResponse25 个声明
sourceQuadratureOperatorsourceQuadratureCurrentsourceQuadratureCurrent_actualsourceQuadratureCurrent_continuoussourceQuadratureCurrent_pricesourceReadGapsourceCausalEtasourceCausalCoefficientsourceWeightedQuadraturesourceWeightedQuadrature_pricesourceWeightedQuadrature_continuoussourceWeightedQuadrature_integrablesourceCausalWindowsourceCausalHalfOperatorsourceCausalWindow_actualsourceCausalWindow_noethersourceCausalWindow_operatorNormsourceCausalTailPricesourceCausalHalfOperator_tailsourceCausalFieldOperatorsourceCausalCurvatureOperatorsourceCausalCurvatureOperator_actualsourceCausalFieldOperator_nativesourceCausalCurvatureOperator_nativesourceCausalWindow_cosourcesAlphaSource.EmIdentification.ActualDressedNoetherResponse15 个声明
dressedKinematicPointdressed_kinematic_transferdressedEulerObserverdressed_euler_observer_originaldressedNoetherJetdressed_noether_jet_generateddressed_noether_jet_continuousdressed_noether_jet_originaldressedNoetherForcingdressed_noether_forcing_originaldressedNoetherFielddressed_noether_field_equationdressedVoltageForcingdressedVoltageUpdatedressed_voltage_update_originalAlphaSource.EmIdentification.ActualDressedSignalOperator12 个声明
dressed_euler_observer_pricedressedSignalOperatordressed_signal_operator_actualdressed_signal_operator_continuousdressedSignalQuadraturedressed_signal_quadrature_actualdressed_signal_quadrature_continuousdressed_signal_quadrature_phasedressedSignalDurationdressed_signal_duration_positivedressedSignalNonlineardressed_signal_nonlinear_generatedAlphaSource.EmIdentification.ActualDressedSignalCausal12 个声明
dressedSignalCausalCoefficientdressedSignalWeighteddressed_signal_weighted_pricedressed_signal_weighted_continuousdressed_signal_weighted_integrabledressedSignalWindowdressedSignalHalfOperatordressed_signal_window_actualdressed_signal_window_noetherdressed_signal_window_operator_normdressedSignalTailPricedressed_signal_half_operator_tail
亲手检验
在仓库根目录运行入口检查:
python3 tools/edition_release.py --edition low-energy verify-map
构建 Lean 证明与完整验收的步骤见复现指南