FullLevitationCert
plain-language theorem explainer
FullLevitationCert defines the complete levitation certificate by extending the unconditional version with an explicit existence claim for an external phase field. It would be cited by researchers closing the integration from RS primitives to acoustic weight reduction. The structure directly encodes the gradient-cancellation condition together with vanishing modified coherence defect, serving as a packaging definition with no additional proof steps.
Claim. A structure extending the unconditional levitation certificate that asserts: for every differentiable processing potential function and every extended object, there exists an external phase function whose derivative at the object's center of mass exactly opposes the processing gradient, and the modified coherence defect (absolute difference of combined potentials at head and feet) equals zero.
background
A ProcessingField is a structure carrying a potential function from position to real numbers. An ExtendedObject carries a center-of-mass position and positive spatial extent. An ExternalPhaseField carries its own phase function whose gradient is the ordinary derivative. The modified_coherence_defect function evaluates the absolute difference of the modified total potentials (gravitational plus external) evaluated at the head and feet of the object at zero acceleration.
proof idea
This is a structure definition extending UnconditionalLevitationCert. It adjoins a single field concrete_field_exists whose body is the quantified existence statement; no lemmas are invoked and no tactics are used.
why it matters
FullLevitationCert supplies the final integration step that closes all four gaps listed in the module comment and feeds the full_levitation_cert theorem, which instantiates the complete certificate. It realizes the concrete-field construction that completes the chain through EnergyProcessingBridge, WeakFieldSuperposition, CoherenceGain, and EightTickResonance, corresponding to the eight-tick octave (T7) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.