theorem
other
other
predicts
show as:
view Lean formalization →
formal statement (Lean)
58theorem predicts perfect linear correlation under the binary
59preference model.
60-/
61
62namespace IndisputableMonolith
63namespace Decision
64namespace AbileneParadox
65
66open Constants Cost
67
68/-! ## §1. Agent type and σ-charge -/
69
70/-- A binary preference: `true = stay`, `false = go`. -/
used by (35)
-
methaneAngle -
neutralAt_const_zero -
phi_critical_numeric -
constant_energy_density -
observational_tests -
jcost_equilibrium_profile -
mondAcceleration -
abundanceVsEta -
amplitude_derivation -
w_mass_rs_prediction -
stPetersburgCert -
cooper_pair_binding_exceeds_thermal -
substrate_model -
no_sterile_needed -
ssm_plus_rs_equals_obs -
blackHoleEchoesCert -
VacuumPersistence -
equivalence_implies_ratio_one -
rs_eotvos_zero -
solar_deflection_positive -
c_grav_RS -
tauon_rung_minus_electron_rung -
j_positive_off_fixed_point -
info_scales_with_boundary -
anomalous_e_tau_universal -
predictions -
three_generations_from_8_tick -
conventions_differ_bottom -
dirac_degeneracy -
predictions