Low-energy series 2 · 2026-10-11
Two Minuses, One Plus, and a Bare Trace Under Oath
Ordered Closed Traces and Whole-Ball Response Curvature
两负一正,裸迹宣誓:有序闭迹与整球响应曲率
- 6claims
- 46Lean modules
- 567declarations
- ✓ all kernel checks passed
Abstract
With the identity matrix on the stand, the bare trace reports and the originally normalized prepared state reports : the first evaluates the trace over the full matter carrier, the second the action within the fixed preparation. For the fixed external source with the co-directional readout operator, zero output momentum, double Laplace parameters , the same preparation, and an incoming/observing two-ball window of radius , we prove that in the complete five-term response both the uncentred (raw) and the centred (connected) quadratic coefficient tensors have two negative and one positive eigenvalue. Here “curvature” means the quadratic coefficient after the non-analytic linear term of the sharp window is removed, not the Hessian of the complete response at the origin.
Read the full abstract
Two branches start from the same action containing an independent dual matter field; that action, its background, matter carrier, and constants are generated from common source data with no fitted parameter. Under the grading, the closed trace of any finite admissible ordered gauge-propagation word equals the closed trace of its block-diagonal part; the prescribed one-directional scalar-insertion closed trace vanishes, and so does every open chain with an arbitrary admissible propagation word between two co-directional insertions. The prepared state, the boundary weight and the complete second-quantized word give different evaluations; the actual return operator produces a nonzero reading, while an intermediate preparation projection erases it. The field-equation branch passes from fields through auxiliary, Ward and symmetry reductions to a -field system, counts matter feedback once, and constructs a rational -dimensional bosonic kernel together with field/source recovery maps. The matter block at the origin has rank ; keeping six light matter directions yields a -dimensional second-order system whose constant term has rank , and its five-dimensional light kernel gives both linear and quadratic momentum time scales and is read out as propagation through the dynamical source.
The two quantum source legs, the readout contact term and the two field propagation legs form the complete five-term response. The non-analytic linear term of the true ball intersection, the full complex Gram matrix, implicit root derivatives, full-direction integrals over paired frames and outward-rounded rational remainders together determine the quadratic tensor. The raw three-axis coefficients lie in , and times in the units of the original action; a uniform bound on all mixed terms makes the inertia statement apply to the complete tensor. The mean term is kept separately; its second-axis interval contains zero.
The actual Fourier Hessian of the same original action is also identified with the complete 289-field matrix. Five origin directions and a 98-dimensional coordinate complement generate an exact Schur kernel for all four complex momenta, a source-generated invertibility radius and a strict cubic remainder. The actual ordered current reconstructs the denominator-cleared whole field, retaining contact and all nine null directions. For another original configuration preparation, the complete ordered five-factor word, its actual Noether contact and four Fourier keys generate a real-field half-axis response operator. A source-generated created-unit/background difference then observes the same history: within its positive source-generated nonlinear time interval, it produces the full quantum tensor , and the finite integral of the mother-Euler amplitude derivative is exactly . Coincident clocks give ; the complete linearized half-axis retains its own growth condition. The same original Green returns this preparation's response to all fields, with conditions stated separately from those of the specified two-ball window.
Claims and proofs
Every claim is registered in the claim map. Open one to see its statement, where it appears in the paper, and the Lean modules and replay programs that prove it. Statements registered in Chinese are shown in English translation.
In reading order. Black: proved in Lean, kernel check passed; grey: supported by replay programs, no Lean declarations.
Q1Closed trace of any finite admissible ordered Dirac word and the one-directional scalar§3
Lean modules · 3
Replay programs and evidence · 1
Q2Original preparation and independent-dual readback of the complete Fock word§4
Lean modules · 5
Replay programs and evidence · 1
Q3One matter feedback, the five-dimensional light kernel and original field/source recovery§5
Lean modules · 12
Replay programs and evidence · 8
Q4Complete five terms and full-tensor inertia for the specified two-ball window§6
Replay programs and evidence · 4
Q5Complete four-momentum Schur complement of the same original action and actual denominator-cleared whole-field recovery§12.1
Lean modules · 4
LowEnergy.AlphaSource.CanonicalPreparationSourceFullOriginInverse38 declarations
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 declarations
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 declarations
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
Q6Half-axis of the genuine Noether ordered preparation, the actual nonlinear full-289 quantum window and original-field return§13.1
Lean modules · 23
LowEnergy.AlphaSource.CanonicalPreparationSourceHalfAxisCurrentOperator15 declarations
sourceWeightedCurrentsourceWeightedCurrent_generatedsourceCurrentPricesourceCurrentPrice_nonnegativesourceWeightedCurrent_pricesourceWeightedCurrent_continuoussourceWeightedCurrent_integrablesourceHalfCurrentsourceHalfCurrent_generatedsourceWindowJacobian_integralsourceCurrentTailPricesourceHalfCurrent_tailsourceHalfCurrent_pricesourceCurrentTailPrice_zerosourceWindowJacobian_operatorNormLowEnergy.AlphaSource.CanonicalPreparationSourceHalfAxisFieldOperator15 declarations
sourceHalfFieldOperatorsourceHalfCurvatureOperatorsourceFieldOperatorFactorsourceCurvatureOperatorFactorsourceHalfFieldOperator_generatedsourceHalfCurvatureOperator_generatedsourceHalfFieldOperator_tailsourceHalfCurvatureOperator_tailsourceHalfFieldOperator_pricesourceHalfCurvatureOperator_pricesourceHalfFieldOperator_nativesourceFieldJacobian_operatorNormsourceCurvatureJacobian_operatorNormsourceHalfCurrent_realitysourceHalfCurvatureOperator_mateLowEnergy.AlphaSource.CanonicalPreparationSourceNativeRealFourierSignal14 declarations
sourcePhasesourcePhase_applysourcePhase_coordinatesourceRealSignalsourceSignalAmplitudesourceRealSignal_smoothsourceRealFirstJetsourceRealSecondJetsourceRealSignal_firstJetsourceRealSignal_secondJetsourceRealJet_coefficientsourceRealEuler_FouriersourceRealSignal_originalDensitysourceRealSignal_originalEulerLowEnergy.AlphaSource.CanonicalPreparationSourceOrderedSignalOperator18 declarations
SignalAmplitudeSourceOpsourceHistoryInputsourceHistoryInput_actualsourceHistoryInput_continuoussourceRightDrivesourceLeftDrivesourceRightDrive_continuoussourceLeftDrive_continuoussourcePrimalOperatorsourceIndependentDualOperatorsourcePrimalOperator_actualsourceIndependentDualOperator_actualsourceMiddleOperatorsourceHistoryOperatorsourceHistoryOperator_actualsourceCurrentOperatorsourceCurrentOperator_actualLowEnergy.AlphaSource.CanonicalPreparationSourcePreparedSignalEuler13 declarations
sourceSignalDurationsourceSignalDuration_positivesourceSignalCurrentsourceRawSignalEuler_generatedsourcePreparedQuadrature_generatedsourceSignalCurrent_actualsourceSignalOrdinaryRemainder_generatedsourceSignalForcingsourceSignalFieldsourceSignalForcing_actualsourceSignalField_nativesourceSignalField_native36sourceSignalForcing_cosourcesLowEnergy.AlphaSource.CanonicalPreparationSourceNativeSignalLaplaceReturn20 declarations
sourcePlaneWindowScalarsourceNativePlaneWindowsourceNativeBoundarysourcePlaneWindowScalar_derivativesourceNativeBoundary_initialsourceNativePlaneWindow_ordinarysourceNativeSignal_weightedsourceNativeEulerWindowsourceNativeEulerWindow_actualsourcePreparedEulerWindowsourcePreparedEulerWindow_generatedsourcePreparedEulerWindow_nativesourceNativeTimeValuesourceNativeTimeFirstsourceNativeTimeValue_actualsourceNativeTimeFirst_actualsourceNativeBoundary_historysourcePlaneHalfScalarsourcePlaneHalfScalar_actualsourcePlaneWindowScalar_limitLowEnergy.AlphaSource.CanonicalPreparationSourceSignalOperatorPrice22 declarations
sourceClockGrowthsourceClockGrowth_nonnegativesourceHistoryInput_pricesourcePrimalCoefficientsourceDualCoefficientsourceRightDrive_pricesourceLeftDrive_pricesourcePrimalOperator_pricesourceIndependentDualOperator_pricesourceMaterialMapsourceContactMapsourceMiddleOperator_source_mapssourceMiddleCoefficientsourceMiddleOperator_pricesourceHistoryLinearCoefficientsourceHistoryConstantCoefficientsourceHistoryOperator_pricesourceCurrentLinearCoefficientsourceCurrentConstantCoefficientsourceCurrentCoefficient_nonnegativesourceCurrentOperator_pricesourceCurrentOperator_continuousLowEnergy.AlphaSource.CanonicalPreparationSourceSignalCausalResponse25 declarations
sourceQuadratureOperatorsourceQuadratureCurrentsourceQuadratureCurrent_actualsourceQuadratureCurrent_continuoussourceQuadratureCurrent_pricesourceReadGapsourceCausalEtasourceCausalCoefficientsourceWeightedQuadraturesourceWeightedQuadrature_pricesourceWeightedQuadrature_continuoussourceWeightedQuadrature_integrablesourceCausalWindowsourceCausalHalfOperatorsourceCausalWindow_actualsourceCausalWindow_noethersourceCausalWindow_operatorNormsourceCausalTailPricesourceCausalHalfOperator_tailsourceCausalFieldOperatorsourceCausalCurvatureOperatorsourceCausalCurvatureOperator_actualsourceCausalFieldOperator_nativesourceCausalCurvatureOperator_nativesourceCausalWindow_cosourcesLowEnergyPhenomenology.AlphaSource.SourceUnitPhysicalCurrent11 declarations
AlphaSource.EmIdentification.ActualDressedNoetherHistory9 declarations
AlphaSource.EmIdentification.ActualDressedNoetherResponse15 declarations
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 declarations
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 declarations
dressedSignalCausalCoefficientdressedSignalWeighteddressed_signal_weighted_pricedressed_signal_weighted_continuousdressed_signal_weighted_integrabledressedSignalWindowdressedSignalHalfOperatordressed_signal_window_actualdressed_signal_window_noetherdressed_signal_window_operator_normdressedSignalTailPricedressed_signal_half_operator_tail
Check it yourself
Run the entry check from the repository root:
python3 tools/edition_release.py --edition low-energy verify-map
Building the Lean proofs and the full acceptance run: Reproduction guide