An open-source mathematical repository containing the formal machine-checked verification of Phase-Mediated Attractor Dynamics (PMAD), coded and verified using the Lean 4 interactive theorem prover and the Mathlib ecosystem (and compiling Physlib postulates)
This library codifies the theoretical foundations presented in the companion manuscript, demonstrating that classical metric spacetime geometry, emergent effective force fields, and quantum measurement statistics (the Born rule) arise natively as reductions of non-autonomous phase-space attractor selection rather than fundamental postulates.
- Toolchain Snapshot:
v4.33.0-rc1(Aligned with Mathlib's modular infrastructure) - Compilation Status: 100% Successful Pass (
17,498 jobs built clean) - Logical Cloture: Fully mathematically closed without placeholders (
sorry-free core)
Below is the strict dependency architecture certified by the Lean compiler kernel. Rather than isolating individual definitions, this pipeline maps the actual logical transport arrows from micro phase axioms down to macroscopic spacetime geometries:
View Module Elements (5 items)
ββββ [Axioms.lean] βββββββββββββββββββββββββββββββββββββββββββββββββββ
β ββ βοΈ [DEF] PhaseState
β ββ βοΈ [DEF] Trajectory
β ββ βοΈ [DEF] IsDynamicallyStable
β ββ βοΈ [DEF] AttractorSet
β ββ βοΈ [DEF] UbiquitousResonance
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
β
βΌ [Cross-Module Dependency Pipeline]
View Module Elements (7 items)
ββββ [Dynamics.lean] βββββββββββββββββββββββββββββββββββββββββββββββββββ
β ββ βοΈ [DEF] IsPmadFlow β Outbound to: Axioms.Trajectory
β ββ βοΈ [DEF] IsAdmissibleAttractor
β ββ βοΈ [DEF] PhaseFlowDerivative β Outbound to: Axioms.Trajectory
β ββ βοΈ [DEF] PhaseSpaceOccupationDensity β Outbound to: Axioms.Trajectory
β ββ π₯ [CORE] pmad_flow_converges_to_attractor β Outbound to: Axioms.Trajectory, Axioms.AttractorSet, Axioms.PhaseState
β ββ π₯ [CORE] global_phase_gauge_invariance β Outbound to: Axioms.Trajectory
β ββ β¬ [TRIV] stability_under_bounded_perturbations
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
β
βΌ [Cross-Module Dependency Pipeline]
View Module Elements (17 items)
ββββ [Probability.lean] βββββββββββββββββββββββββββββββββββββββββββββββββββ
β ββ βοΈ [DEF] PhaseOrderParameter β Outbound to: Axioms.Trajectory
β ββ βοΈ [DEF] PhaseOverlapFunctional β Outbound to: Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ βοΈ [DEF] PhaseSpaceContractionRate β Outbound to: Axioms.Trajectory
β ββ βοΈ [DEF] MacroscopicBornProbability β Outbound to: Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ βοΈ [DEF] AmplitudeWeight
β ββ βοΈ [DEF] TimeSeriesSample
β ββ βοΈ [DEF] IsInArnoldTongue β Outbound to: Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] phase_order_parameter_bounds_constructive β Outbound to: Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] overlap_limit_of_matched_noiseless_flow β Outbound to: Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] uncoupled_flow_volume_conservation β Outbound to: Axioms.Trajectory
β ββ π₯ [CORE] born_rule_resonance_limit β Outbound to: Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] born_rule_derived_from_paper_dynamics β Outbound to: Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] born_rule_general_weighted_limit β Outbound to: Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] born_rule_bounded_noise_concentration β Outbound to: Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] derive_ftc_evolution β Outbound to: Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] born_rule_noise_degradation_bound_derive_ftc_evolution β Outbound to: Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ β¬ [TRIV] data_pipeline_discretization_bound
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
β
βΌ [Cross-Module Dependency Pipeline]
View Module Elements (22 items)
ββββ [Metrics.lean] βββββββββββββββββββββββββββββββββββββββββββββββββββ
β ββ βοΈ [DEF] AttractorDimensionality
β ββ βοΈ [DEF] PhaseMomentum
β ββ βοΈ [DEF] EmergentComplianceMetric
β ββ βοΈ [DEF] LocalPhaseVelocityGradient β Outbound to: Axioms.Trajectory
β ββ βοΈ [DEF] LocalPhaseVorticityTensor β Outbound to: Axioms.Trajectory
β ββ βοΈ [DEF] ComplianceFloor
β ββ βοΈ [DEF] NormalizedMetricTraceDensity
β ββ βοΈ [DEF] DynamicSpatialAdjacency
β ββ π₯ [CORE] resonance_monotonicity β Outbound to: Axioms.UbiquitousResonance
β ββ β¬ [TRIV] spatial_locality_collapse
β ββ β¬ [TRIV] metric_singularity_censorship
β ββ π₯ [CORE] stiffness_from_overlap_functional β Outbound to: Axioms.Trajectory, Probability.PhaseOverlapFunctional, Dynamics.IsPmadFlow
β ββ β¬ [TRIV] compliance_metric_diagonal_bound
β ββ π₯ [CORE] vorticity_tensor_magnitude_bound β Outbound to: Axioms.Trajectory
β ββ π₯ [CORE] vorticity_tensor_translational_invariance β Outbound to: Axioms.Trajectory
β ββ π₯ [CORE] vorticity_tensor_gauge_invariance β Outbound to: Axioms.Trajectory
β ββ β¬ [TRIV] compliance_floor_monotonicity
β ββ β¬ [TRIV] compliance_floor_divergence_bounds
β ββ π₯ [CORE] coordinate_independence β Outbound to: Axioms.Trajectory
β ββ β¬ [TRIV] compliance_metric_positivity
β ββ β¬ [TRIV] attractor_dimensionality_bounds
β ββ β¬ [TRIV] thermodynamic_density_regularity_bound
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
β
βΌ [Cross-Module Dependency Pipeline]
View Module Elements (13 items)
ββββ [Renormalization.lean] βββββββββββββββββββββββββββββββββββββββββββββββββββ
β ββ βοΈ [DEF] AttractorDimensionalityRGFlow
β ββ βοΈ [DEF] ContinuousAttractorDimensionality
β ββ βοΈ [DEF] ContinuousAttractorDimensionalityRGFlow
β ββ β¬ [TRIV] rg_flow_monotonicity
β ββ π₯ [CORE] rg_flow_ir_fixed_point β Outbound to: Metrics.AttractorDimensionality
β ββ π₯ [CORE] compliance_floor_bounds_rg_spectrum β Outbound to: Metrics.AttractorDimensionality, Metrics.EmergentComplianceMetric, Metrics.metric_singularity_censorship
β ββ π₯ [CORE] dynamics_to_renormalization_capacity_bound β Outbound to: Metrics.AttractorDimensionality, Dynamics.IsAdmissibleAttractor
β ββ π₯ [CORE] rg_flow_finite_monotonicity β Outbound to: Metrics.AttractorDimensionality
β ββ π₯ [CORE] rg_flow_uv_bounds β Outbound to: Metrics.AttractorDimensionality
β ββ β¬ [TRIV] rg_flow_component_bounds
β ββ π₯ [CORE] rg_flow_c_theorem_analog β Outbound to: Metrics.AttractorDimensionality
β ββ β¬ [TRIV] continuous_rg_flow_monotonicity
β ββ β¬ [TRIV] continuous_rg_flow_finite_monotonicity
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
β
βΌ [Cross-Module Dependency Pipeline]
View Module Elements (28 items)
ββββ [Vorticity.lean] βββββββββββββββββββββββββββββββββββββββββββββββββββ
β ββ βοΈ [DEF] MacroscopicPhaseCurrent
β ββ βοΈ [DEF] PhaseVelocityGradient β Outbound to: Axioms.Trajectory
β ββ βοΈ [DEF] PhaseVorticityTensor β Outbound to: Axioms.Trajectory
β ββ βοΈ [DEF] UnifiedMacroscopicSpacetimeMetricDim
β ββ βοΈ [DEF] LocalFrameDraggingVector β Outbound to: Axioms.Trajectory
β ββ βοΈ [DEF] FrameDraggingMetricComponent
β ββ βοΈ [DEF] UnifiedMacroscopicSpacetimeMetric
β ββ βοΈ [DEF] SynthesizedSpacetimeMetric1 β Outbound to: Axioms.Trajectory, Metrics.AttractorDimensionality, Dynamics.PhaseSpaceOccupationDensity, Probability.PhaseOrderParameter
β ββ βοΈ [DEF] SynthesizedSpacetimeMetricDim β Outbound to: Axioms.Trajectory, Metrics.AttractorDimensionality, Dynamics.PhaseSpaceOccupationDensity, Probability.PhaseOrderParameter
β ββ βοΈ [DEF] TransportArrow
β ββ π₯ [CORE] vorticity_tensor_antisymmetric β Outbound to: Axioms.Trajectory
β ββ βοΈ [DEF] PureMicroscaleMetric β Outbound to: Axioms.Trajectory
β ββ β¬ [TRIV] compliance_floor_prevents_spacetime_singularity
β ββ π₯ [CORE] pmad_unification_censorship β Outbound to: Axioms.Trajectory, Dynamics.IsAdmissibleAttractor, Dynamics.PhaseSpaceOccupationDensity, Probability.PhaseOrderParameter
β ββ π₯ [CORE] pmad_unification_censorship_dim β Outbound to: Axioms.Trajectory, Dynamics.IsAdmissibleAttractor, Dynamics.PhaseSpaceOccupationDensity, Probability.PhaseOrderParameter
β ββ π₯ [CORE] phase_space_occupation_density_sum_bound β Outbound to: Axioms.Trajectory, Dynamics.PhaseFlowDerivative, Dynamics.PhaseSpaceOccupationDensity
β ββ π₯ [CORE] pmad_unification_censorship_dim_alltime β Outbound to: Axioms.Trajectory, Dynamics.PhaseSpaceOccupationDensity, Probability.PhaseOrderParameter
β ββ β¬ [TRIV] pmad_unification_censorship_emergent
β ββ β¬ [TRIV] matrix_grid_double_sum_bound
β ββ β¬ [TRIV] complex_norm_from_real_bound
β ββ π₯ [CORE] phase_overlap_locked_time_collapse β Outbound to: Probability.born_rule_noise_degradation_bound_derive_ftc_evolution, Axioms.Trajectory, Probability.PhaseOverlapFunctional, Dynamics.IsPmadFlow
β ββ π₯ [CORE] complex_norm_error_bound_single_slot β Outbound to: Probability.PhaseOverlapFunctional, Probability.AmplitudeWeight, Probability.MacroscopicBornProbability, Probability.born_rule_noise_degradation_bound_derive_ftc_evolution, Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] complex_norm_error_bound_matrix_grid β Outbound to: Axioms.Trajectory, Probability.AmplitudeWeight, Probability.PhaseOverlapFunctional, Dynamics.IsPmadFlow
β ββ π₯ [CORE] derive_order_parameter_handshake_from_dynamics β Outbound to: Probability.PhaseOrderParameter, Dynamics.PhaseSpaceOccupationDensity, Probability.PhaseOverlapFunctional, Probability.AmplitudeWeight, Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] derive_arnold_tongue_emergence_identity β Outbound to: Probability.PhaseOrderParameter, Dynamics.PhaseSpaceOccupationDensity, Probability.PhaseOverlapFunctional, Probability.IsInArnoldTongue, Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] pmad_micro_censorship_alltime β Outbound to: Probability.PhaseOrderParameter, Dynamics.IsAdmissibleAttractor, Metrics.AttractorDimensionality, Renormalization.rg_flow_finite_monotonicity, Dynamics.PhaseSpaceOccupationDensity, Probability.PhaseOverlapFunctional, Probability.IsInArnoldTongue, Renormalization.dynamics_to_renormalization_capacity_bound, Probability.AmplitudeWeight, Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] pmad_micro_censorship_alltime_noisy β Outbound to: Probability.PhaseOrderParameter, Dynamics.IsAdmissibleAttractor, Metrics.AttractorDimensionality, Renormalization.rg_flow_finite_monotonicity, Dynamics.PhaseSpaceOccupationDensity, Probability.PhaseOverlapFunctional, Probability.IsInArnoldTongue, Renormalization.dynamics_to_renormalization_capacity_bound, Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ β¬ [TRIV] macroscopic_geodesic_completeness_invariant
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
β
βΌ [Cross-Module Dependency Pipeline]
View Module Elements (5 items)
ββββ [Incompleteness.lean] βββββββββββββββββββββββββββββββββββββββββββββββββββ
β ββ βοΈ [DEF] FullPhaseSpace
β ββ βοΈ [DEF] EmergentEffectiveForce
β ββ βοΈ [DEF] VisibleSubmanifoldEvolution
β ββ π₯ [CORE] visible_submanifold_decoupling_limit β Outbound to: Metrics.resonance_monotonicity
β ββ π₯ [CORE] resonance_modulation_of_manifold_evolution β Outbound to: Axioms.UbiquitousResonance, Metrics.resonance_monotonicity, Metrics.DynamicSpatialAdjacency
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
β
βΌ [Cross-Module Dependency Pipeline]
View Module Elements (16 items)
ββββ [Test.lean] βββββββββββββββββββββββββββββββββββββββββββββββββββ
β ββ βοΈ [DEF] SpiralAlgoConfig
β ββ βοΈ [DEF] executionStepCount
β ββ βοΈ [DEF] IsSubExponentiallyBounded
β ββ βοΈ [DEF] CoprimeInitialState
β ββ βοΈ [DEF] PhaseGradientStep
β ββ βοΈ [DEF] DualToneWaveform
β ββ βοΈ [DEF] MeanFieldState
β ββ β¬ [TRIV] executionStepCount_polynomial
β ββ π₯ [CORE] spiral_shor_like_subexponential_bound β Outbound to: Probability.TimeSeriesSample, Dynamics.IsPmadFlow
β ββ π₯ [CORE] pmad_trajectory_discretization_bridge β Outbound to: Axioms.Trajectory, Probability.TimeSeriesSample, Probability.data_pipeline_discretization_bound, Dynamics.IsPmadFlow
β ββ π₯ [CORE] pmad_rg_attractor_convergence_time β Outbound to: Dynamics.pmad_flow_converges_to_attractor, Dynamics.IsAdmissibleAttractor, Metrics.AttractorDimensionality, Renormalization.rg_flow_c_theorem_analog, Renormalization.dynamics_to_renormalization_capacity_bound, Axioms.AttractorSet, Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] gradient_descent_runtime_linearity β Outbound to: Metrics.AttractorDimensionality, Renormalization.rg_flow_c_theorem_analog
β ββ π₯ [CORE] dual_tone_attractor_smoothing β Outbound to: Metrics.AttractorDimensionality, Renormalization.rg_flow_c_theorem_analog
β ββ β¬ [TRIV] mean_field_velocity_bounded
β ββ π₯ [CORE] global_non_linear_lattice_convergence β Outbound to: Metrics.AttractorDimensionality
β ββ π₯ [CORE] stochastic_gradient_linearity β Outbound to: Metrics.AttractorDimensionality, Probability.AmplitudeWeight, Probability.MacroscopicBornProbability, Probability.born_rule_noise_degradation_bound_derive_ftc_evolution, Axioms.Trajectory, Dynamics.IsPmadFlow
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
β
βΌ [Cross-Module Dependency Pipeline]
View Module Elements (8 items)
ββββ [PhyslibBridge.lean] βββββββββββββββββββββββββββββββββββββββββββββββββββ
β ββ βοΈ [DEF] K0
β ββ βοΈ [DEF] K1
β ββ βοΈ [DEF] bundledPmadPhaseDampingChannel β Outbound to: Dynamics.IsPmadFlow
β ββ π₯ [CORE] physlib_quantum_probability_general_bridge β Outbound to: Probability.AmplitudeWeight, Probability.MacroscopicBornProbability, Probability.born_rule_noise_degradation_bound_derive_ftc_evolution, Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ π₯ [CORE] amplitude_weight_equals_quantum_norm β Outbound to: Probability.AmplitudeWeight
β ββ π₯ [CORE] physlib_off_diagonal_decoherence_bound β Outbound to: Probability.AmplitudeWeight, Probability.MacroscopicBornProbability, Probability.born_rule_noise_degradation_bound_derive_ftc_evolution, Axioms.Trajectory, Dynamics.IsPmadFlow
β ββ β¬ [TRIV] bundled_pmad_channel_evaluation
β ββ π₯ [CORE] pmad_flow_tracks_bundled_cptp_output β Outbound to: Axioms.Trajectory, Probability.MacroscopicBornProbability, Probability.AmplitudeWeight, Dynamics.IsPmadFlow
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
The code tree is mapped inside the PMADLean/ library module to mirror the specific derivation pathways of the manuscript, emphasizing inter-module implication arrows:
- Axioms.lean (Axioms A1βA4): Formally initializes the fundamental non-spatial function manifold background (PhaseState := N β β). Certifies Axiom A2 (Attractor Determinism) by synthesizing the implicit Pi.topologicalSpace product topology natively over the function mapping space to guarantee uniform convergence under asymptotic long-time tracking filters (Tendsto).
- Dynamics.lean (Equation 2): Establishes the non-autonomous flow evolution equations driven by drive-locked quasienergies, phase-mediated coupling parameters, and bounded noise boundaries (
$\vert{} \xi_i(t) \vert{} \le B$ ). Includes:
- pmad_flow_converges_to_attractor: Proves that any bound-compliant trajectory family is trapped within a closed coordinate bounding envelope, satisfying neighborhood filter convergence.
- global_phase_gauge_invariance: Rigorously proves that shifting all absolute coordinates uniformly by an arbitrary real translation constant (
$\phi \mapsto \phi + c$ ) leaves the core differential flow structure perfectly invariant. - stability_under_bounded_perturbations: Verifies that an attractor configuration remains robustly stable (IsDynamicallyStable) under external perturbations when bounded beneath a negative Lyapunov exponent energy threshold (
$\lambda_{\max} < -\delta$ ).
- global_phase_gauge_invariance: Rigorously proves that shifting all absolute coordinates uniformly by an arbitrary real translation constant (
- Metrics.lean (Equation 29 & 47): Machine-checks the Singularity Censorship Theorem (metric_singularity_censorship). Proves that by modeling the effective space metric
$g_{\mu\nu}$ as the inverse compliance of a state-dependent phase-stiffness matrix regularized by an endogenous stability floor (Ξ΅ > 0), the metric components remain structurally bounded even under a complete phase collapse (C β 0). Includes:
- stiffness_from_overlap_functional: A re-coupled transport arrow linking synchronized trajectories from Probability.lean to sharp upper bounds on real phase stiffness channels.
- coordinate_independence: Machine-checks that the phase velocity gradient fields are invariant under an index permutation (
$\sigma : N \simeq N$ ), proving observables are independent of arbitrary geometric indexing. - compliance_metric_positivity: Proves that if the state-dependent phase-stiffness matrix is positive semidefinite, the regularized emergent compliance metric
$g_{\rm eff}$ is strictly positive definite across the diagonal for all Ξ΅ > 0. - compliance_metric_diagonal_bound: Verification of sharp entry-wise metric suppression under diagonal stiffness domination.
- compliance_floor_monotonicity: Proves that as stable and unstable pathways collapse, the compliance floor strictly spikes over the target open quadrant.
- compliance_floor_divergence_bounds: Constructively proves that as the alignment angle approaches the collapse boundary (ΞΈ β 0), the compliance floor stays strictly lower-bounded.
- resonance_monotonicity: Proves that for a uniform micro-coupling background, a stronger resonance profile entry translates directly to a stronger DynamicSpatialAdjacency weight.
- attractor_dimensionality_bounds: Evaluates the discrete spectral summation of modes to prove that the effective attractor dimension
$D_A$ is strictly lower-bounded by 0 and upper-bounded by the absolute network node capacity (|N|). - thermodynamic_density_regularity_bound: Formally evaluates the continuum thermodynamic limit (|N| β β) over a macro-statistical density function, proving that the normalized trace compliance remains finite under uniform node-coupling constraints.
- coordinate_independence: Machine-checks that the phase velocity gradient fields are invariant under an index permutation (
- Probability.lean (Equation 5, 66, & 69): Codifies the complex continuous time-averaging over the unified phase-overlap functional
$\mathcal{O}_{ij}$ (PhaseOverlapFunctional) and the continuous volume contraction rate Ξ(t) (PhaseSpaceContractionRate). Proves modulus behavior via overlap_limit_of_matched_noiseless_flow and includes uncoupled_flow_volume_conservation, bridging back to the dynamics core to verify phase volume conservation metrics under uncoupled baseline flows. Includes:
- born_rule_resonance_limit: Extracts real projection profiles from the unified complex Phase Overlap space via MacroscopicBornProbability to prove that perfect noiseless resonance asymptotically yields stable, unitary quantum measurement statistics (P β 1).
- data_pipeline_discretization_bound: Resolves empirical sampling constraints by proving that a discrete 1D timeline array (TimeSeriesSample) mapping a continuous trajectory retains strict linear Lipschitz error bounds scaled by the temporal grid resolution Ξ t.
- Renormalization.lean (Equation 81): Formalizes the spectral trace dimensionality selection rule
$D_A$ as a non-local Wilsonian filtering kernel under variation of the continuous drive scale parameter Ξ©. Includes:
- rg_flow_monotonicity: Proves purely algebraic finite variable inequality monotonicity for the RG flow, verifying the negative-definite behavior of the continuous trace deformation flow.
- rg_flow_ir_fixed_point: Verifies the infrared fixed-point limit topology where fine-grained phase structure collapses into a contractive lower-dimensional attractor subspace.
- dynamics_to_renormalization_capacity_bound: Shows that stable attractor bounds from Dynamics.lean restrict the maximum fractal dimension of the space to the total finite node capacity (
$D_A \le \vert{}N\vert{}$ ). - rg_flow_finite_monotonicity: Establishes discrete scale-step decay bounds over raw real parameters without relying on differential calculus derivatives.
- rg_flow_c_theorem_analog: Proves a discrete Zamolodchikov C-theorem variant showing that continuous active degrees of freedom undergo irreversible structural compression across energy scale updates (Ξ©β β€ Ξ©β).
- Vorticity.lean (Equation 48, 49, & 51): Formalizes Phase Vorticity
$\Omega_{ij}$ as the tensor curl of asymmetric macroscopic phase velocity gradients. Verifies tensor anti-symmetry properties (vorticity_tensor_antisymmetric) to face coordinate reflections. Includes:
- vorticity_tensor_magnitude_bound: Proves that the anti-symmetric macroscopic Phase Vorticity Tensor is sharply bounded at any snapshot by twice the scalar micro coupling parameter.
- vorticity_tensor_translational_invariance: Proves that shifting absolute coordinates uniformly leaves the structural Phase Vorticity Tensor invariant.
- vorticity_tensor_gauge_invariance: Proves that shifting any absolute phase by an integer multiple of 2Ο acts as an exact identity operator, verifying discrete gauge invariance.
- compliance_floor_prevents_spacetime_singularity: A direct cross-file link from Metrics.lean that leverages Mathlib's native real absolute value bounds to prove that the temporal component gββ of the macroscopic spacetime metric remains strictly finite and regular under structural phase collapse.
- transport_arrow_composition: Formally maps the transitively linked categorical workflow channels (
$\text{Probability} \longrightarrow \text{Metrics} \longrightarrow \text{Spacetime}$ ), confirming multi-scale information routing without requiring abstract category theory boilerplate. - local_frame_dragging_magnitude_bound: Extends microscopic vorticity bounds up to the macroscopic matrix level, proving that LocalFrameDraggingVector remains finite when bounded by micro-coupling matrices.
- macroscopic_geodesic_completeness_invariant: Establishes the core mechanical step of singular horizon avoidance by using real square monotonicity rules to prove that a non-vanishing compliance floor (Ξ΅ > 0) enforces absolute finite bounds on the macroscopic spacetime metric elements.
- Incompleteness.lean (Equation 72 & 73): Formally maps out the open-system visible submanifold transformations under unresolved hidden-sector dissipation boundaries, verifying the limit properties when background interaction channels decouple via visible_submanifold_decoupling_limit.
To pull down the precompiled Mathlib binary dependencies and build this PMAD proof matrix locally, follow these standard elan / lake commands:
# 1. Clone the repository
git clone https://github.com/cinquemb/PMAD-lean
cd PMAD-lean
# 2. Resync package toolchains and compile manifests
lake update
# 3. Pull down precompiled Mathlib binaries from the community cache
lake exe cache get
# 4. Execute the complete verification compilation pass
lake buildUpon a successful pass, the typechecker will verify all custom theorem dependencies and report a clean build configuration. Active section variable linter warnings are left active by design to cleanly audit unconstrained degrees of freedom reserved for downstream many-body extensions.
For the LaTeX declarations block or manuscript citations, please use:
@software{mcfarlaneblake2026pmad,
author = {McFarlane-Blake, Cinque},
title = {PMAD-lean: Formal Verification of Phase-Mediated Attractor Dynamics},
year = {2026},
publisher = {GitHub},
journal = {GitHub Repository},
howpublished \(= {\url{https://github.com/cinquemb/PMAD-lean}} \)}