← The Shadow of Existence
The formalisation
Each of these 111 rows is one calculation a receipt performs and a paper relies on. This says, for each, whether that calculation is also proved in Lean — and where a proof exists, the theorem is linked. Beside a row, each theorem name links to its proof, and a description shown there without a link is a calculation not yet proved. 822 theorems are linked across 111 rows.
Proved
The calculation the receipt performs is proved in Lean, and the theorem that proves it is linked.
111 of 111 rows.
0 curvature invariants of max-symmetric spaces, R of a slicing frw_scal_weyl_k frw_closed_slicing RECEIPT 1 Weyl^2 (C^2) as a polynomial in shear bianchi_weyl2 row1_shear RECEIPT 2 Weyl^2 = 0 on FRW frw_scal_weyl_k frw_closed_slicing RECEIPT 3 rank of curvature-invariant basis, Weyl^2 = 0 row3_rank RECEIPT 4 curvature invariants; Ricci scalar of a layer frw_scal_weyl_k frw_closed_slicing frw_scal layer_scal RECEIPT 5 Ricci scalar of two slicings frw_scal_weyl_k frw_closed_slicing layer_late RECEIPT 6 Einstein tensor and its divergence (contracted Bianchi identity) contracted_bianchi nRic_eq bianchi2_lc compat_lc curv_metric_antisymm nabla_metric_antisymm RECEIPT 7 ADM identity for extrinsic curvature K_ij of a slice adm_trace_split tfSym_finrank adm_rho tr_sq_sym adm_rho_shear_lowers RECEIPT 8 TT mode function of a field on de Sitter conf_box ds_tt_mode lcGam_diag4 RECEIPT 9 plane sections of the dS hyperboloid as submanifolds with radius row9_checks section_quadric RECEIPT 10 plane sections of the dS quadric identified as dS_{D-1} / sphere row10_checks section_quadric RECEIPT 11 surface gravity and the accelerated (Unruh-type) temperature unruh_ds_limits RECEIPT 12 Killing norm: static region pinches off at the double root; blueshift factor row12_checks row12_blueshift row104_nariai_root RECEIPT 13 LTB Einstein tensor with matter, equation of motion ltb_Gtt ltb_bend RECEIPT 14 closed-FRW dust scale factor equals a cycloid (a function) frw_cycloid RECEIPT 15 LTB turnaround radius (functions of r) ltb_turnaround RECEIPT 16 LTB turnaround time (functions) ltb_turnaround_time RECEIPT 17 Kretschmann scalar on the Nariai cut nariai_curvature GE_nondeg ef_kretschmann RE_tab RUE_tab sds_kretschmann_ef nariai_horizon_kretschmann RECEIPT 18 branched covering and its canonical flat connection the discriminant, which locates the branch points — proj_isCoveringMap fibre_card lift_half_nonreal swap_plus swap_minus monodromy_surjective monodromyGroup_equiv_S3 cubicQ_irreducible cubicQ_disc_not_square cubicQ_gal_full cubicQ_gal_equiv monodromy_equiv_gal cubic_disc_roots family_disc disc_square_iff equilateral_iff no_triple_root RECEIPT 19 Weyl^2, Gauss-Bonnet as a total derivative gb_total_derivative frw_closed frw_gb_k frw_gb_three gb_total_derivative_k frw_weyl frw_scal layer_scal layer_late frw_invariants tv_identity ledger_general ledger_layer ledger_ds_point RECEIPT 20 momentum constraint, mode ODE, div G contracted_bianchi tt_waves superposition_transverse mode_equation shear_square RECEIPT 21 Nariai limit identified as dS2 x S2 row21_checks nariai_curvature row104_nariai_root RECEIPT 22 de Sitter curvature invariants curv_T ds_invariants RECEIPT 23 quadratic counterterm reduction to GB + EOM terms frw_invariants tv_identity ledger_general ledger_layer ledger_ds_point RECEIPT 24 heat-kernel coefficient b_4 decomposition b4_rewrite trace_relation shear_onset row1_shear RECEIPT 25 one metric in four charts; Killing norm at the horizon schw_charts schw_pg_shift RECEIPT 26 horizons sorted by completion (global) row26_checks RECEIPT 27 continuation reproduces exterior metric coefficients (a metric in a chart) circle_continuation RECEIPT 28 Kretschmann along a curve row28_curves RECEIPT 29 cycloid solves the radial geodesic equation unitU_geodesic interior_chart interior_geodesic cycloid_proper_time RECEIPT 30 interior metric in cycloid coordinates; causal character of eta interior_cycloid interior_gtt_zero RECEIPT 31 complex continuation lands on real r on three axes three_axes RECEIPT 32 geodesic acceleration equals r times a slice's Gaussian curvature accel_rKG sds_accel_is_rKG RECEIPT 33 parity split of the lapse polynomial rnds_parity rnds_core schw_core_minus RECEIPT 34 a slice's Gaussian curvature equals -f'/(2r) diag_curv lcGam_diag slice_gauss RECEIPT 35 Einstein tensor; vacuum field equation solved by Tangherlini-dS tangherlini5_Gtt tangherlini5_kernel tangherlini4_Gtt tangherlini4_kernel tangherlini6_Gtt tangherlini6_kernel tangherlini7_Gtt tangherlini7_kernel tangherlini8_Gtt tangherlini8_kernel RECEIPT 36 slice Gaussian curvature zero locus and the Nariai discriminant sds_flat_locus sds_nariai_iff sds_slice_gauss RECEIPT 37 continuation through a throat: C1-not-C2 join with signature flip throat_join RECEIPT 38 geodesic acceleration = r K_G (slice curvature) sds_balance_is_flat RECEIPT 39 points on the ambient quadric and values of the ambient interval hinge_interval RECEIPT 40 deck group Z_{D-1} from the imaginary period row40_checks RECEIPT 41 zero-energy radial orbit; null flow fixed points with kappa = f'/2 surface_gravity kappa_half_fprime RECEIPT 42 I20: conformal Killing, charge on null geodesics, 1+z conformalKilling_cov charge_const xi_isConformalKilling a_omega_const one_plus_z RECEIPT 43 homothety charge conserved on null geodesics only flat_isLeviCivita homothety_nabla homothety_charge RECEIPT 44 photon-sphere Lyapunov exponent of the geodesic flow lcGam_diag3 null_radial sds_photon_lyapunov RECEIPT 45 SdS Kretschmann from Riemann sds_kretschmann RECEIPT 46 horizon areas and entropies of two readings photon_sphere nariai_seam areas_entropies RECEIPT 47 shear of a foliation from extrinsic curvature leaf_K RECEIPT 48 Einstein tensor and p_r + rho of a matter source static_Gtt_Grr RECEIPT 49 Einstein tensor = 8 pi T; vacuum solution SdS; density m' static_AeqF static_density RECEIPT 50 flat slicing as an embedding with its induced metric flat_on_quadric flat_dtau flat_dx flat_induced flat_horosphere RECEIPT 51 TOV system from the Einstein tensor static_tov RECEIPT 52 closed/open slicings as hyperboloid embeddings, 3-curvature open_leaf_curv horo_on_hyperboloid RECEIPT 53 parameter count of vacuum-equation solutions; isotropy groups the number of free parameters in each family of solutions, which the receipt counts — sds_essImage sds_equiv sds_fibre sds_dim td_essImage td_equiv td_dim strata_finrank sds_kernel skew_finrank sds_kernel typeD_four skew_finrank RECEIPT 54 Kantowski-Sachs stress-energy vanishes ks_stress RECEIPT 55 pp-wave Ricci/Riemann, vacuum iff harmonic, Petrov type N pp_Ruxux pp_kretschmann pp_riemann pp_vacuum_iff RECEIPT 56 Killing algebra of the plane wave (Heisenberg), null orbits killing_lie pw_bracket pw_dv_null pw_killing pw_wronskian_const xiPW_deriv RECEIPT 57 curvature invariants on an anomaly-deformed background, zeta residue turnover_unique eps_size inv_exp source_moves gradient_six gradient_eight realizable_cubics dK_split sector_orders P_closed ranks_by_order second_direction no_fourth_convention L_coeff harmonic_closed log_coeff zeta_face trace_face curvature_face control_weight faces_together two_halves vertex_scaled rank_eq_of_factor Exp3 RECEIPT 58 ADM kinetic term and Legendre transform row58_adm_kinetic row58_det_gate row58_legendre row58_hamiltonian row58_legendre_needs_sign row58_euler_lagrange row58_sign row58_measure_power RECEIPT 59 algebraic quartic of a curvature expansion quartic_identity quartic_traceless euler_volume milnor_scalar rad_coframes chart_trace_pow h4_invariants h4_chart floor_taylor tt_dim_five jet_dim_twelve sector_rank_eight basis_independent gp_onto hp_onto frame_series rad_row_frame section_e_integrals algebraic_prediction RECEIPT 60 coincidence-limit level sums (heat-kernel expansion) invariant_basis C_minor trace_relation_fixes full_traces level_tensors_cond second_order_identity B_unique scal_second_order control_frame_constant part_B seven_level_values weights_nonzero level_sums_sign part_C cross_factorises sign_algebra faulhaber RECEIPT 61 horizon induced metric degenerate of rank two ef_det ef_horizon_degenerate ef_horizon_rank RECEIPT 62 scalar curvature on S^3 frame jets jet_series jet_series4 jet_series frame_constant_closed_form fast4_correct fastD_correct tA_eq tB_eq tQ_eq tD_eq tC_eq falsRows_eq sector_ranks_computed control_raises_A_computed sel8_independent_computed seven_plus_five_span_computed identity_pointwise_computed identity_unique_computed six_configurations_integrals box_evR rad_rows_frame six_configurations_computed jets_TT jets_frame_commutator eps4_values sector_ranks control_raises_A sel8_independent seven_plus_five_span identity_pointwise identity_unique coefficients_192 kvecs_computed frame_constant_rank_one six_configurations_rank_four frame_constant_anchor six_predictions identity_fails_off_transversality identity_fails_off_transversality_computed enumeration moments moment4 RECEIPT 63 trace anomaly C_controls C_tower C_receipt A1_cosh A2_variance A2_const A2_sign A2_sample A3_radiation A3_flat B1_bare B2_trace B3_R B3_slope B3_iff rank_one_of_const moment_det_neg adot_sq Rtow_eq zeta_rule_eq Bj_zero B3_zero zeta_free_tower zeta_protected zeta_odd series_inputs rule_is_limit RECEIPT 64 curvature-scalar ranks under an anomaly deformation rank_A kernel_A phase_A R_deformed inv_poly log_structure ranks_by_order L_coeff rate_factor log_coeff control_weight conventions_three kernel_rotates one_number A6_factor substrate orders RECEIPT 65 curvature shifts a TT mode frequency milnor_scalar const_curv_tt zeta_count tt_mode_eom s3_ricci summand_split slope_tendsto slope_tendsto_new slope_tendsto_old slope_tendsto_dis bracket_new_2000 bracket_new_4000 bracket_old_2000 bracket_old_4000 bracket_dis tt_level_multiplicity frame_bracket lap_K K_TT TU_lap TL_lap seed_TT sU_TT sL_TT mem_spec tt_level_multiplicity_N tt_m345 tt_complete integral_Ea lap_symm neg_lap_nonneg lap_spectrum degree_bound tt_spectrum tt_count tt_count_real polyS_closure_eq_top tt_level_multiplicity frame_bracket lap_K K_TT TU_lap TL_lap seed_TT sU_TT sL_TT mem_spec tt_level_multiplicity_N tt_m345 lap_spectrum degree_bound tt_spectrum tt_count tt_count_real tt_level_multiplicity frame_bracket lap_K K_TT TU_lap TL_lap seed_TT sU_TT sL_TT mem_spec tt_level_multiplicity_N tt_m345 integral_Ea lap_symm neg_lap_nonneg polyS_closure_eq_top polyL2_dense RECEIPT 66 cubic kinetic vertex on S^3 milnor_scalar s3_ricci s3_tt_eigen traceless_cube euler_volume halfline_integral euler_coframe euler_structure euler_tt_trace euler_tt_transverse euler_s3_curvature milR66_exp r_exp_series mtw_bianchi_ix commutator_trace milR66_perm kinetic_volume_split kinetic_linear_split kinetic_splits_differ tt_level_multiplicity frame_bracket lap_K K_TT TU_lap TL_lap seed_TT sU_TT sL_TT mem_spec tt_level_multiplicity_N tt_m345 tt_complete integral_Ea lap_symm neg_lap_nonneg lap_spectrum degree_bound tt_spectrum tt_count tt_count_real polyS_closure_eq_top tt_level_multiplicity frame_bracket lap_K K_TT TU_lap TL_lap seed_TT sU_TT sL_TT mem_spec tt_level_multiplicity_N tt_m345 lap_spectrum degree_bound tt_spectrum tt_count tt_count_real tt_level_multiplicity frame_bracket lap_K K_TT TU_lap TL_lap seed_TT sU_TT sL_TT mem_spec tt_level_multiplicity_N tt_m345 integral_Ea lap_symm neg_lap_nonneg polyS_closure_eq_top polyL2_dense RECEIPT 67 TT harmonics on S^3, eigenvalue 6 (spectral) s3_tt_eigen traceless_cube det_frame_conj euler_volume kos_unit euler_s3_curvature euler_coframe euler_structure euler_tt_trace euler_tt_transverse RECEIPT 68 completeness relation, level overlap (spectral) trace_P level_three drop_one exponent_zero two_point wick_receipt eight_values eight_homogeneous value_rank_one pow_homogeneous_3_to_6 combo_homogeneous completeness orthonormal traceless wick support factorises contract trivia RECEIPT 69 Pontryagin density of a Gowdy wave pontryaginLC_eq gowdy_pontryagin gowdy_plane_wave_pontryagin gowdy_areal_pontryagin gowdy_areal_weight cycle_average reflection_is_half_turn eps4_sign eps4_det eps4_zero_of_not_injective eps4_antisymm sum_eps GW_apply gowdy_areal_silenced gowdy_areal_psi_constant gowdy_areal_omega_constant areal_profile_exists cycle_average_quarter cycle_average_in_step cycle_average_anti_phase cycle_average_bound RECEIPT 70 oscillator identity for the energy shift dE2_closed conj_zero conj_q3 conj_q3qpq gen_solves fake_vev fake_zero cubic_nonres fake_receipt no_cancellation pure_cubic_even g3_derivs trace_cube trace_cube_cases closed_dS frame_values frame_weyl eight_homogeneous bianchi_connection bi_gradient ratios_distinct derivative_test gauge_ratio combo_homogeneous residue_scheme cited_bound any_target cubic_channel dE2_receipt_sizes frw_tab_k fRk_maxsym ms_q RiemQ_eq RlT_bi bi_scal bi_q deviation locus bookkeeping control ranks RECEIPT 71 C^2 = E4 + 2(Ric^2 - R^2/3) weyl2_gb_identity row71_sds RECEIPT 72 ranks of FRW curvature invariants frw_closed RECEIPT 73 Bianchi-IX curvature expansion, vertices, vacuum shift R3_round R3_milnor kinetic_linear kinetic_exponential unit_jacobian quartic_vev cubic_three_quanta one_quantum_cancels cubic_shift fock_receipt total_shift at_level_three density_a6 linear_solves rank_two dmu_residues dovmu_residues log_coeff residue_product misner unimodular taylor shapes calibration normalisation threshold faulhaber RECEIPT 74 Gowdy-dS background field equation 3H^2 = Lambda, shear charge gowdy_ds_field gowdy_shear_charge RECEIPT 75 Einstein tensor of Gowdy-dS equals the wave/constraint equations gowdy_tz_field RECEIPT 76 Mukhanov variable mode equation on de Sitter ds_app mukhanov RECEIPT 77 Killing equation: exactly two Killing vectors killing_of_invariant gowdy_killing killF_model killF_coord coord_not_killing gowdy_coord_not_killing rot_killF gowdy_rot_not_killing RECEIPT 78 Brinkmann wave Ricci-flat lcGam_pp pp_ricci pw_ricci_flat RECEIPT 79 extrinsic curvature K_ab = 0 of leaves, leaf scalar curvature sds_leaf_K_zero leaf_scal sds_leaf_R3 RECEIPT 80 dS as a coset space with the Killing-form metric killing_on_coset RECEIPT 81 Ricci = Lambda g; Kretschmann carries M row81_separator RECEIPT 82 Dirac spectrum on S^5/S^4 friedrich_saturation RECEIPT 83 scalar curvature of a squashed S^5 row83_squashed_S5_everywhere curvG_eq row83_squashed_S5 RECEIPT 84 Dirac gap on S^5 one_scale mass_bounds RECEIPT 85 leaf tetrad and spin connection give the superpotential W tetrad_metric superpotential_values horizon_W throat_check RECEIPT 86 branches of a height function on the quadric how many branches the height function has outside the throat, on it, and inside it — action_faithful_order3 preserves_quadric fixedPoints_eq orbit_three orbit_free throat_points_permuted branches_eq axis_pair singlet_obstructed loci flip branch_count RECEIPT 87 imaginary roots of X0^2 = -alpha^2 axis_vantage RECEIPT 88 power-of-a-point height: a point on the quadric axis_vantage RECEIPT 89 Pontryagin density from a metric kerr_pontryagin kerrClosed_odd kerr_odd kerr_receipt_odd kerr_receipt_zero kerr_receipt_ne kerr_psi2 kerr_static_zero baryon_charge diquark_charge meson_charge seat_charge trivial_charge eig_scalar wall_content vector_like one_seat turnaround_lift local_residual global_residual dirac_fixes div_onShell div_offShell density_count static_pontryagin_zero diag_static_zero static_f_zero static_fhS_zero static_weyl_zero static_named_zero gowdy_pontryagin gowdy_grading grading_exact gowdy_twist_odd gowdy_const_twist gowdy_shift member_pontryagin member_odd member_zero member_ne member_transgression member_ratio ratio_neg_one member_divK_ne member_divK_odd eps4_det pontryaginLC_eq pontryagin_parity tabs_bridge Kcontr_ok vector_like_both_conventions wall_conventions local_residual_ne div_offShell_ne Wcontr_ok transgression clifford RECEIPT 90 the quadric has no real point on the axis axis_vantage RECEIPT 91 sinh^(2/3) satisfies the radial geodesic first integral row91_checks sinh23_flow RECEIPT 92 sinh^(2/3) solves the E = 1 radial geodesic rain_geodesic sds_rain_geodesic sinh23_flow RECEIPT 93 SdS Kretschmann; Weyl to Lambda ratio row93_weyl_split RECEIPT 94 umbilic locus of a foliation leaf_umbilic_iff RECEIPT 95 separated wave operator (Killing vectors via Lie derivative on the way) so3_killing killF95_model sph_wave_sep harm_1_0 harm_1_1 harm_2_0 harm_2_1 harm_2_2 harm_3_0 harm_3_1 harm_3_2 harm_3_3 s3_levels RECEIPT 96 Pontryagin density of three metrics pontryagin_parity cs_parity warped_pontryagin warped_cs nariai_pontryagin_zero nariai_rotated_pontryagin_zero nariai_general_pontryagin_zero polarised_pontryagin_zero unpolarised_nonzero gowdy_plane_wave_pontryagin gowdy_areal_pontryagin gowdy_areal_silenced gowdy_pontryagin gowdy_cs member_cs member_pontryagin member_divergence member_stokes member_volume sph_pontryagin_zero sph_cs_zero net_count eps4_sign eps4_det sum_eps pontryaginLC_eq riemLC_tab csLC_tab tabs_bridge csArr_three nariai_apply GW_apply areal_profile_exists GM_apply ratio_neg_one riemLC_tab RECEIPT 97 induced slice identified as R x S^2, not S^3 row97_checks layer_ricci s3_ricci kretschmann_on_worldline sds_kretschmann sinh23_flow RECEIPT 98 Einstein condition and optical tidal matrix row98_einstein_tidal static_radial_tidal RECEIPT 99 surface gravities at the two roots two_surface_gravities RECEIPT 100 proper-frame metric tends to dS2 x S2 (identification) row100_checks row100_exact row100_flow row100_rates row100_decades row100_deviation_instance row100_simple_instance chi_block_gauss warped_table planar_invariants sds_kretschmann_W row100_kretschmann_at_rN nariai_curvature row104_nariai_root RECEIPT 101 derivatives of r(s) along a collapse leg row101_checks row101_ratio row101_frac row104_nariai_root sinh23_flow RECEIPT 102 extrinsic-curvature shear of a foliation leaf_shear RECEIPT 103 Gaussian curvature of the slicing surface sds_two_ranges RECEIPT 104 dS2 x S2 radii (with flat induced 3-metric, Kretschmann) row104_flat_slice row104_nariai_root nariai_curvature RECEIPT 105 f = f' = 0 at the Nariai root row105_checks row104_nariai_root RECEIPT 106 Wick rotation identifies the dS5 quadric with S^5 row106_checks cc_invariants dS5_constant_curvature RECEIPT 107 a confocal quadric family as a foliation confocal_degree RECEIPT 108 SdS as a cut of dS5; hyperplane sections of constant curvature section_quadric dS5_constant_curvature sds_K_radial boost_pullback cut_defect cut_closure_iff cut_closes_only_at_M_zero cut_control RECEIPT 109 de Sitter surface gravity and entropy ds_horizon_iff ds_surface_gravity RECEIPT 110 SdS Petrov invariant vanishes row110_petrov RECEIPT
Generated from the repository. Source.