#!/usr/bin/env python3 """Audit documentary gaps between a software claim and a small source registry. This is a manifest linter. It does not establish mathematical applicability, verify evidence contents, execute proof code or certify a numerical model. """ import argparse import json from pathlib import Path COMMIT='fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb' CONTRACTS={ '125-metric-facility-threshold':dict(family='125',statement_type='fixed_epsilon_deterministic_metric_kmedian_approximation',formal_scope_covers_claim=True, required_model=dict(distance='finite_binary_rational_strict_metric',clients='unweighted_set_of_locations', facilities='specified_candidate_subset',budget='nonempty_at_most_k', constraints='uncapacitated_no_extra_constraints',accuracy='each_fixed_positive_epsilon', guarantee='one_plus_two_over_e_plus_epsilon_relative_to_integral_optimum'), obligations=['full_metric_and_exact_input_mapping_checked','unweighted_demand_and_candidate_identity_preserved', 'capacity_cost_fairness_and_time_constraints_scoped_separately','fixed_accuracy_parameters_selected_and_actual_resources_measured', 'full_preparation_rounding_history_and_budget_reduction_implemented', 'returned_facilities_assignments_and_cost_independently_checked', 'source_ratio_separate_from_instance_specific_primal_dual_gap', 'recovery_anchor_proxy_promise_not_assumed_for_arbitrary_inputs', 'source_proof_imports_and_independent_acceptance_recorded','existing_solver_and_actual_review_value_compared'], excluded_uses=['weighted_capacitated_directed_road_model_inherits_theorem','uniform_practical_runtime_in_inverse_epsilon', 'endpoint_factor_attained','generic_local_search_inherits_source_ratio', 'arbitrary_anchor_satisfies_recovery_promise','solver_status_is_independent_optimality_certificate', 'symmetrized_distances_preserve_original_objective','proven_customer_savings_from_theorem'], source_locations=['lean/docs/125.md','lean/ComparatorChallenges/MetricKMedian.lean','lean/ComparatorChallenges/MetricKMedian.json', 'lean/ComparatorChallenges/KMedianRefinedRecovery.lean','lean/OAI/Combinatorics/KMedian/Main.lean', 'lean/OAI/Combinatorics/KMedian/Geometry/RationalAllParameters.lean', 'lean/OAI/Combinatorics/KMedian/Geometry/RationalParameterizedHistory.lean', 'lean/OAI/Combinatorics/KMedian/Reduction/ReductionClosure.lean', 'preprints/The-Approximation-Threshold-for-Metric-k-Median-September-24-2026/main.pdf', 'preprints/Single-Exponential-Recovery-and-Bounded-Price-Strictness-for-Metric-k-Median-September-24-2026/paper.pdf']), '325-complete-polynomial-numerical-range':dict(family='325',statement_type='finite_complete_Crouzeix_polynomial_inequality',formal_scope_covers_claim=True, required_model=dict(matrix_domain='arbitrary_finite_complex_matrix_positive_dimension', coefficient_domain='finite_complex_square_matrices_one_positive_common_dimension', polynomial_model='one_complex_variable_finite_degree_ascending_coefficients', norm_model='Euclidean_operator_2',evaluation_model='sum_A_power_k_tensor_B_k_base_first', comparison_domain='entire_numerical_range',source_constant=2), obligations=['matrix_input_and_Euclidean_norm_model_fit','matrix_coefficient_tensor_order_preserved', 'rigorous_outer_enclosure_of_entire_numerical_range','covered_supremum_bound_with_matrix_norm_and_error_control', 'arithmetic_rounding_input_uncertainty_and_budget_accounted','new_source_constant_separate_from_published_prior_bound', 'finite_reference_not_formally_verified_source_program','error_polynomial_target_and_physical_or_discretization_bridge', 'source_proof_imports_and_independent_check_status_recorded','existing_direct_norm_cost_and_actual_workflow_value_compared'], excluded_uses=['eigenvalue_maximum_bounds_arbitrary_nonnormal_norm','sampled_boundary_max_is_rigorous_upper', 'finite_test_agreement_accepts_source_theorem','general_nonlinear_stability_from_polynomial_norm', 'arbitrary_rational_poles_without_domain_bridge','source_verified_Fraction_or_SciPy_implementation', 'production_speedup_from_sharper_constant'], source_locations=['lean/docs/325.md','lean/ComparatorChallenges/DirectCrouzeix.lean','lean/ComparatorChallenges/DirectCrouzeix.json', 'lean/OAI/Analysis/DirectCrouzeix/Main.lean','lean/OAI/Analysis/DirectCrouzeix/CompleteBound.lean', 'lean/OAI/Analysis/DirectCrouzeix/Sharpness.lean', 'preprints/A-direct-proof-of-the-complete-Crouzeix-inequality-September-26-2026/build/main.tex']), '128-constructed-superstring-two-approximation':dict(family='128',statement_type='deterministic_polynomial_constructed_superstring_two_approximation',formal_scope_covers_claim=True, required_model=dict(input_representation='explicit_finite_list_of_ordinary_strings',symbol_model='finite_encoded_symbol_labels', containment='exact_contiguous_substring',output_model='one_common_superstring',approximation_measure='symbol_length', comparison_optimum='unrestricted_common_superstring_length',time_model='deterministic_polynomial_in_encoded_input_bits', backend_model='forced_counts_periodic_layers_requests_cycle_opening_Euler_output'), obligations=['explicit_input_and_byte_to_symbol_encoding_bridge','empty_duplicate_contained_preprocessing_preserves_instance', 'forced_count_blocking_and_period_rules_correct','full_layer_request_link_cycle_output_construction_correspondence', 'exact_contiguous_original_ID_coverage_checked','actual_bit_operation_memory_and_runtime_costs_measured', 'symbol_bound_separate_from_serialized_compressed_byte_objective','terminator_mutability_identity_and_alignment_API_bridge', 'source_proof_imports_and_independent_check_status_recorded','existing_linker_packer_and_complete_artifact_comparison'], excluded_uses=['maximum_overlap_greedy_inherits_source_factor_two','count_stage_alone_is_full_source_backend', 'arbitrary_substring_view_is_drop_in_C_string','shortest_blob_is_smallest_compressed_artifact', 'practical_latency_from_polynomial_classification','assembly_with_errors_or_wildcards', 'source_verified_conventional_DP_or_greedy','production_storage_cost_savings'], source_locations=['lean/docs/128.md','lean/ComparatorChallenges/Superstring.lean','lean/ComparatorChallenges/Superstring.json', 'lean/OAI/Computability/Superstring/Main.lean', 'preprints/A-Polynomial-Time-2-Approximation-for-Shortest-Common-Superstring-September-24-2026/build/sections/01-introduction.tex', 'preprints/A-Polynomial-Time-2-Approximation-for-Shortest-Common-Superstring-September-24-2026/build/sections/02-counts.tex', 'preprints/A-Polynomial-Time-2-Approximation-for-Shortest-Common-Superstring-September-24-2026/build/sections/07-algorithm.tex']), '138-fast-subset-sum-decision':dict(family='138',statement_type='paper_level_two_sided_randomized_subset_sum_decision',formal_scope_covers_claim=False, required_model=dict(value_model='positive_integers_repeated_values_allowed',target_model='nonnegative_integer_empty_subset_allowed', output_model='YES_NO_decision',error_model='two_sided_at_most_one_third_per_fixed_input', input_access='readonly_one_integer_per_word',randomness_model='fresh_independent_uniform_word_per_operation', word_width='ceil_four_times_n_plus_b_plus_log2_n_plus_two',bit_regime='every_fixed_c_eventually_b_at_most_n_power_c', time_model='every_random_execution_capped_word_operations',advice_model='none'), obligations=['original_positive_integer_model_and_item_identity_mapping','word_width_and_multiword_operation_cost_bridge', 'fresh_randomness_and_per_fixed_input_error_bridge','known_bit_guard_and_unevaluated_fixed_cutoff_reviewed', 'exact_fallback_and_actual_main_backend_distinguished','two_sided_decision_not_exact_witness_or_count', 'adaptive_self_reduction_and_amplification_budget_if_witness_requested','returned_original_ID_witness_exactly_checked', 'source_proof_and_absent_family_formal_scope_recorded','practical_existing_solver_and_workflow_comparison'], excluded_uses=['exact_negative_certificate_from_randomized_NO','source_decision_directly_returns_witness', 'exact_solution_count','signed_adjustments_without_bridge','combined_0_49_time_0_2_space_algorithm', 'fast_main_branch_at_practical_n_without_guards','source_verified_CP_SAT_or_MITM', 'production_reconciliation_speedup'], source_locations=['preprints/Subset-Sum-in-Time-2-power-0-49n-October-4-2026/build/sections/introduction.tex', 'preprints/Subset-Sum-in-Time-2-power-0-49n-October-4-2026/build/sections/setup.tex', 'preprints/Subset-Sum-in-Time-2-power-0-49n-October-4-2026/build/sections/implementation.tex']), '138-low-space-subset-sum-decision':dict(family='138',statement_type='paper_level_one_sided_low_space_subset_sum_decision',formal_scope_covers_claim=False, required_model=dict(value_model='positive_integers_repeated_values_allowed',target_model='nonnegative_integer_empty_subset_allowed', output_model='YES_NO_decision',error_model='never_false_YES_at_most_one_third_false_NO', input_access='readonly_one_integer_per_word',randomness_model='fresh_independent_uniform_word_per_operation', writable_space_model='all_registers_addresses_counters_stacks_tables_seeds_random_values', bit_regime='every_fixed_c_eventually_b_at_most_n_power_c',time_model='every_random_execution_capped_word_operations', space_bound='A_c_times_n_plus_b_plus_two_power_15_times_2_power_0_199n_words'), obligations=['original_positive_integer_model_and_item_identity_mapping','word_width_and_multiword_operation_cost_bridge', 'all_writable_state_and_record_vs_occurrence_memory_accounted','known_u_guard_and_unevaluated_fixed_cutoff_reviewed', 'all_subset_exact_fallback_not_fast_main_branch','fresh_round_trials_and_capped_work_reviewed', 'one_sided_decision_not_exact_negative_or_count','overlap_masks_not_merged_only_by_equal_sum', 'adaptive_witness_recovery_error_budget_and_ID_check','source_proof_and_absent_family_formal_scope_recorded'], excluded_uses=['exact_negative_certificate_from_randomized_NO','exact_solution_count', 'combined_0_49_time_0_2_space_algorithm','low_space_main_branch_at_practical_n_without_guards', 'merge_equal_weight_different_overlap_masks','space_excludes_stacks_or_random_seeds', 'source_verified_CP_SAT_or_MITM','production_reconciliation_speedup'], source_locations=['preprints/A-Low-Space-Algorithm-for-Worst-Case-Subset-Sum-September-26-2026/build/introduction.tex', 'preprints/A-Low-Space-Algorithm-for-Worst-Case-Subset-Sum-September-26-2026/build/resources.tex', 'preprints/A-Low-Space-Algorithm-for-Worst-Case-Subset-Sum-September-26-2026/build/implementation.tex']), '124-three-machine-unit-scheduling':dict(family='124',statement_type='fixed_finite_machine_polynomial_exact_unit_scheduling',formal_scope_covers_claim=True, required_model=dict(graph_model='explicitly_listed_nonempty_finite_DAG',machine_count=3, processing_times='all_one',nonpreemptive=True,machines='identical',release_times='all_zero', communication_delays='none',eligibility='all_machines',additional_resources='none', deadline_model='none_or_integer_one_through_n',time_model='deterministic_multitape_binary_input_length', machine_model='one_fixed_finite_machine_for_all_inputs'), obligations=['explicit_graph_acyclicity_and_job_identity_mapping','unit_nonpreemptive_identical_machine_model_fit', 'no_silent_release_eligibility_setup_or_resource_features','binary_input_and_schedule_output_encoding_bridge', 'actual_implementation_correspondence_to_fixed_machine','proof_imports_and_independent_check_status_recorded', 'direct_capacity_and_strict_precedence_witness_checks','polynomial_backend_not_tiny_exponential_reference', 'large_exponent_and_constant_practical_limits_reviewed','existing_solver_and_workflow_value_comparison'], excluded_uses=['generic_unequal_duration_scheduler','four_machine_extension','release_or_eligibility_extension', 'unit_splitting_automatically_preserves_nonpreemption','tiny_DP_is_source_polynomial_backend', 'CP_SAT_is_source_verified_machine','solver_optimal_status_is_independent_proof', 'production_speedup_from_polynomial_classification'], source_locations=['preprints/A-polynomial-time-algorithm-for-three-machine-unit-job-scheduling-September-24-2026/build/paper.tex', 'lean/docs/124.md','lean/ComparatorChallenges/ThreeMachine.lean', 'lean/ComparatorChallenges/ThreeMachine.json','lean/OAI/Computability/Scheduling/Main.lean']), '115-bounded-integral-flow':dict(family='115',statement_type='paper_level_bounded_flow_counting_and_approximate_sampling',formal_scope_covers_claim=False, required_model=dict(graph_model='finite_directed_multigraph_loops_allowed',state_model='integer_arc_value_vector', commodity_model='single_commodity',bound_model='finite_binary_integer_lower_upper', balance_model='outflow_minus_inflow_prescribed',target_law='uniform_all_feasible_arc_vectors', randomness_model='independent_fair_bits',sampling_model='TV_tau_bounded_time_polynomial_inverse_tau', counting_model='relative_epsilon_confidence_one_minus_delta',cost_model='no_extra_global_cost_constraint'), obligations=['lower_bound_shift_and_balance_validated','parallel_and_loop_private_vertices_preserved', 'source_flow_to_table_bijection_mapping','actual_count_backend_and_parameters_reviewed', 'exact_feasibility_at_each_sampling_child','fresh_adaptive_count_calls_and_failure_budget', 'finite_bit_branch_precision_and_total_TV_bound','feasible_output_on_every_execution', 'scenario_law_and_integer_units_fit_workflow','source_paper_vs_selected_formal_scope_recorded'], excluded_uses=['exact_uniform_bounded_flow_sampler','sampling_runtime_polynomial_only_log_inverse_tau', 'multicommodity_extension','uniform_path_decompositions','uniform_cost_optimal_flows', 'zero_approximate_count_proves_infeasible','actual_outage_probability', 'selected_formal_flow_sampler_without_bridge'], source_locations=['preprints/An-FPRAS-for-Cell-Bounded-Contingency-Tables-September-24-2026/build/sections/flows.tex', 'lean/docs/115.md','lean/ComparatorChallenges/ContingencyTables.lean', 'lean/ComparatorChallenges/ContingencyTables.json']), '238-coordinate-trace-smoothing':dict(family='238',statement_type='uniform_full_permutation_trace_mixing_bound',formal_scope_covers_claim=True, required_model=dict(domain_model='dyadic_labeled_slots',switch_model='one_shared_bit_per_sweep_coordinate_pair', randomness_model='independent_fair_switch_bits',permutation_convention='input_to_output', time_unit='complete_forward_coordinate_sweeps',error_model='full_permutation_total_variation'), obligations=['universal_source_P_or_u_selected_and_validated','integer_v_twice_v_at_least_P', 'source_protocol_and_implementation_mapping','same_assignment_forward_inverse_and_workers', 'independent_randomness_or_separate_prg_bridge','optional_non_dyadic_cycle_bridge_and_query_cost', 'full_joint_law_not_only_marginals','independent_check_status_recorded'], excluded_uses=['single_card_uniform_implies_joint_uniform','one_sweep_general_uniform', 'fixed_unreviewed_sweep_count','seeded_rng_is_independent_fair_bit_oracle', 'non_dyadic_constant_worst_case_cycle_cost','cryptographic_security', 'perfect_uniform_general_permutation','source_point_query_compiler_formally_verified'], source_locations=['lean/docs/238.md','lean/ComparatorChallenges/CoordinateTrace.lean', 'lean/ComparatorChallenges/CoordinateTrace.json', 'lean/OAI/Probability/ThorpRouting/RegularTrace.lean', 'lean/OAI/Probability/ThorpRouting/TraceDecay.lean', 'preprints/Random-subspace-tests-and-trace-smoothing-for-coordinate-sweeps-September-26-2026/build/sections/introduction.tex', 'preprints/Random-subspace-tests-and-trace-smoothing-for-coordinate-sweeps-September-26-2026/build/sections/proof.tex']), '103-logspace-language-equality':dict(family='103',statement_type='language_class_equality',formal_scope_covers_claim=True, required_model=dict(input_model='binary_language',machine_model='finite_control_endmarked_input_local_binary_work_tapes', randomness_model='fresh_independent_fair_bits',space_model='all_traversed_writable_cells', randomized_time_model='polynomial_worst_case_all_coin_tapes'), obligations=['exact_machine_semantics_mapping','fixed_machine_time_and_space_promises', 'rl_or_bpl_acceptance_gap','language_decision_not_random_sample_output', 'compiler_and_numerical_time_bounds_separately_reviewed','independent_check_status_recorded'], excluded_uses=['derandomize_arbitrary_ml','deterministic_cryptographic_randomness','preserve_random_output_distribution', 'selected_formal_compiler_resource_bounds','production_speedup','automatic_resource_promise_verification'], source_locations=['lean/docs/103.md','lean/OAI/Computability/Logspace/Deterministic.lean', 'lean/OAI/Computability/Logspace/Equality.lean', 'preprints/Exact-Derandomization-of-Logarithmic-Space-L-equals-RL-equals-BPL-September-23-2026/build/sections/compiler.tex']), '110-uniform-kserver':dict(family='110',statement_type='finite_metric_uniform_online_algorithm',formal_scope_covers_claim=True, required_model=dict(metric_model='finite_rational_metric',request_model='oblivious_finite_sequence', service_model='one_labeled_server_per_request',time_model='polynomial_in_encoding_and_log_request_counter', additive_cost_model='finite_unrestricted_instance_constant'), obligations=['two_at_most_k_below_number_of_points','metric_and_encoding_validated','legal_server_choice', 'implementation_correspondence','constructor_steps_and_activation_reviewed', 'finite_horizon_additive_loss_reviewed','actual_request_latency_measured','independent_check_status_recorded'], excluded_uses=['zero_additive_loss_for_uniform_implementation','polynomial_activation_delay','adaptive_adversary', 'deadlines_or_heterogeneous_capacity','production_speedup','request_time_independent_of_history_counter'], source_locations=['lean/docs/110.md','lean/ComparatorChallenges/UniformKServer.lean', 'preprints/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026/build/source/sections/04-uniform-computation.tex']), '374-brenier-stability':dict(family='374',statement_type='uniform_one_third_holder_transport_map_stability',formal_scope_covers_claim=True, required_model=dict(dimension_minimum=2,source_model='uniform_compact_convex_body_nonempty_interior', target_model='borel_probabilities_one_fixed_nonempty_compact_container', map_model='unique_quadratic_optimal_maps',error_model='source_L2_map_norm_vs_target_W2'), obligations=['uniform_source_and_domain','fixed_compact_target_container','quadratic_optimality_mapping', 'domain_constant_selected_and_validated','same_source_l2_and_target_w2_metrics', 'discretization_or_regularization_bridge_separately_reviewed','independent_check_status_recorded'], excluded_uses=['uniform_half_exponent','pointwise_prediction_error','automatic_entropic_solver_guarantee', 'arbitrary_learned_transport_map','discrete_source_same_theorem','algorithm_for_fitting_transport_maps'], source_locations=['lean/docs/374.md','lean/OAI/Analysis/Brenier/Basic.lean', 'lean/OAI/Analysis/Brenier/Stability.lean', 'preprints/Sharp-One-Third-Stability-of-Brenier-Maps-September-25-2026/build/source/sections/gradient.tex']), '131-lazy-switch-chain':dict(family='131',statement_type='specified_markov_chain_mixing',formal_scope_covers_claim=True, required_model=dict(graph_model='simple_undirected_labeled',host_model='complete_host', kernel='half_hold_uniform_four_set_uniform_ordered_matching_pair', step_unit='all_holding_rejected_and_accepted_steps',target_law='uniform_labeled_degree_fiber'), obligations=['graphical_labeled_degree_vector','n_at_least_four_or_separate_small_case', 'implementation_kernel_correspondence','total_chain_step_accounting','target_tv_and_bound_recorded', 'no_host_connectivity_attribute_or_weight_restrictions','source_claim_vs_independent_check_recorded'], excluded_uses=['selected_formal_exact_sampler','host_restricted_switch_mixing','connected_only_mixing', 'directed_or_weighted_extension','accepted_swaps_use_same_step_bound','practical_large_graph_deadline']), '365-joint-same-patch':dict(family='365',statement_type='identifiability',formal_scope_covers_claim=False, required_model=dict(dimension_minimum=3,regularity='smooth',measurement_model='ideal_same_patch_boundary_operator'), obligations=['smooth_manifold_and_boundary','trivial_rank_two_bundle','smooth_unitary_connection','nonempty_open_patch','gauge_and_diffeomorphism_quotient'], excluded_uses=['finite_noisy_reconstruction_guarantee','efficient_reconstruction_algorithm']), '372-static-elasticity':dict(family='372',statement_type='uniqueness',formal_scope_covers_claim=True, required_model=dict(dimension=3,regularity='smooth',measurement_model='full_static_boundary_operator'), obligations=['connected_bounded_smooth_domain','smooth_lame_parameters','mu_positive','three_lambda_plus_two_mu_positive','full_operator_equality'], excluded_uses=['finite_noisy_reconstruction_guarantee','efficient_reconstruction_algorithm','anisotropic_elasticity']), '281-qaoa-energy':dict(family='281',statement_type='ordered_limit_expected_energy',formal_scope_covers_claim=False, required_model=dict(instance_model='gaussian_zero_field_SK',limit_order='size_then_depth'), obligations=['unique_source_version','expected_energy_per_spin','ordered_limits','angle_selection_cost_recorded','required_depth_unknown'], excluded_uses=['finite_instance_optimality','efficient_angle_selection','hardware_speedup']), '266-three-bases':dict(family='266',statement_type='computer_assisted_exclusion',formal_scope_covers_claim=False, required_model=dict(dimension=6,arithmetic_model='specified_binary64_compiler_contract'), obligations=['complete_verifier_pipeline','compiler_conditions','rounding_and_arithmetic_conditions','source_and_certificate_hashes','four_basis_exclusion'], excluded_uses=['lean_verified_exactly_three']), '276-gad-capacity':dict(family='276',statement_type='memoryless_classical_capacity',formal_scope_covers_claim=True, required_model=dict(channel_model='qubit_generalized_amplitude_damping',decoding_model='asymptotic_collective'), obligations=['parameter_convention','memoryless_channel','channel_fit_evidence','scalar_optimization_error','collective_decoding_assumption'], excluded_uses=['quantum_capacity','secret_key_capacity','separate_measurement_capacity','finite_block_decoder']), '245-pts-beta-normalization':dict(family='245',statement_type='conditional_system_wide_termination',formal_scope_covers_claim=True, required_model=dict(expression_calculus='pure_type_system',reduction_relation='full_beta_including_annotations', normalization_quantifier='all_legal_expressions_all_valid_contexts'), obligations=['exact_pts_specification_mapping','global_weak_normalization_proof','legal_expression_and_valid_context', 'full_annotation_reduction','no_added_rewrite_rules_or_eta','runtime_bound_status_recorded'], excluded_uses=['single_term_normal_form_implies_strong_normalization','termination_of_added_rewrite_rules', 'beta_eta_normalization','practical_runtime_bound','arbitrary_program_termination']), '254-artin-membership':dict(family='254',statement_type='effective_decision_procedure',formal_scope_covers_claim=False, required_model=dict(group_class='finite_rank_Artin',input_model='coxeter_matrix_subset_conjugator_word_test_word', arithmetic_model='exact_computable_cyclotomic_field'), obligations=['valid_finite_coxeter_matrix','exact_word_and_parabolic_input','categorical_detector_implementation', 'exact_coefficient_field','complex_size_and_coefficient_growth_measured','external_kernel_trust_record'], excluded_uses=['polynomial_runtime','production_speedup','lean_verified_membership_algorithm', 'intersection_constructor_supplied_by_membership_test']), '279-exact-quantum-factoring':dict(family='279',statement_type='ideal_exact_uniform_circuit_factoring',formal_scope_covers_claim=True, required_model=dict(input_model='binary_integer_at_least_two',hardware_model='ideal_exact_qubit_circuit', gate_set='NOT_CNOT_Toffoli_H_S_inverses_and_single_controls'), obligations=['complete_prime_factorization_output','uniform_classical_circuit_generator','gate_and_qubit_bounds', 'exact_probability_one_model','noise_and_fault_tolerance_separately_analyzed','practical_resources_measured'], excluded_uses=['classical_polynomial_factoring','hardware_probability_one','practical_resource_improvement', 'standard_Clifford_T_gate_set_without_translation']), '314-chromatic-cyclic-length':dict(family='314',statement_type='finite_p_group_fixed_point_loss',formal_scope_covers_claim=False, required_model=dict(group_class='finite_p_group',subgroup_model='embedded_subgroup', spectrum_class='finite_p_local_genuine_G_spectrum',height_model='nonnegative_integer'), obligations=['finite_p_group_verified','embedded_subgroup_verified','shortest_subnormal_cyclic_chain', 'cyclic_quotient_counted_once','finite_genuine_spectrum_hypothesis','target_height_nonnegative'], excluded_uses=['arbitrary_finite_group_without_reduction','loss_from_abstract_subgroup_type_alone', 'polynomial_subgroup_enumeration','spectrum_witness_constructor']), } def audit(record): if not isinstance(record,dict):raise ValueError('The claim record must be an object') contract_id=record.get('contract_id') if contract_id not in CONTRACTS:raise ValueError('Unknown contract_id') contract=CONTRACTS[contract_id] issues=[] def add(code,message,obligation=None): item=dict(code=code,message=message) if obligation is not None:item['obligation']=obligation issues.append(item) if record.get('source_commit')!=COMMIT: add('SOURCE_VERSION_MISMATCH','The input does not cite the reviewed source revision; scope must be reviewed again.') requested=record.get('requested_evidence_label','source_claim') if requested not in ('source_claim','selected_formal_scope','independently_verified'): raise ValueError('Unknown requested_evidence_label') if requested in ('selected_formal_scope','independently_verified') and not contract['formal_scope_covers_claim']: add('FORMAL_SCOPE_MISMATCH','The reviewed family-level formal scope does not cover this exact claim.') if requested=='independently_verified': add('INDEPENDENT_CHECK_NOT_RUN','This linter runs no trusted proof checker and cannot grant an independently verified label.') model=record.get('model',{}) if not isinstance(model,dict):raise ValueError('model must be an object') for field,required in contract['required_model'].items(): if field=='dimension_minimum': value=model.get('dimension') if value is None:add('MODEL_FIELD_UNKNOWN','The model dimension is undocumented.','dimension') elif isinstance(value,bool) or not isinstance(value,int):raise ValueError('dimension must be an integer') elif value