module module

`IndisputableMonolith.Verification.RecognitionStabilityAudit.RL`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.RecognitionStabilityAudit module_import
IndisputableMonolith.Verification.RecognitionStabilityAudit.RL.Attr module_import

declarations in this module (31)

def getRsaSimpNames L42
def getRsaMilestoneNames L46
theorem BoundaryHitAt_def L108
theorem SchurOn_def L111
theorem Problem_XiFromSensor_def L114
theorem SensorBlowsUpAt_def L117
theorem sensorOfObstruction_def L120
theorem goal_theta_eq_div L146
theorem goal_theta_invTheta L150
theorem goal_invTheta_theta L154
theorem goal_pole_implies_boundaryHit L158
theorem goal_obstruction_to_sensor_blowup L164
theorem goal_frontEnd_from_candidate_obligations L173
theorem goal_boundaryHit_value L192
theorem goal_boundaryHit_forces_const_one L199
theorem goal_backEnd_const_zero L211
theorem goal_correctness_trivial_univ L227
theorem goal_correctness_usage L238
theorem goal_virtueAction_zero_norm L260
theorem goal_virtueAction_norm_nonneg L264
theorem goal_virtueAction_scale_norm L268
theorem goal_lexBetter_irrefl L273
theorem goal_gibbs_weight_pos L277
theorem goal_gibbs_partitionFn_pos L282
theorem goal_eightTick_value_finite L288
theorem goal_sigma_feasibility L293
theorem goal_harm_bound_zero L298
theorem goal_consent_condition L303
theorem goal_parasitism_threshold_phi L308
theorem goal_LACompletion_identity_project L313
theorem goal_temperance_check L318