/media/bill/PROJECTS/Lucas - Universal Force/0_Lucas ToDos.txt
www.BillHowell.ca 12Sep2018 initial - taken from "0_Lucas notes.txt"
***********
ToDos - current :
16Dec2019 Thomas Barnes' feedback fields derivation of relativistic correction factor :
01Oct2019? Versions – experimental, Jeffimenko, Dowdye, Weber electrodynamics (Assize)
O10ct2019? redo math (4-33) to (4-37)
***********
Questions :
30Aug2019 (4-30) Shouldn't this be a full integral? [2*PI = Aθpc(POIo(t),t=0) for 2D, or spherical surface]
∫[∂(Aθpc),0.to.Aθpc(POIo(t),t=0): Rpcs(POIo(t),t)^(-6)*sin(Aθpc(POIo(t),t))^3*cos(Aθpc(POIp(t),t)) ]
16Dec2019 infinite number of observer frames (each v [direction, speed, acceleration, etc], so infinite number of field strengths at a given point in space at a given point in time!! So you calculate for the frame of the [sensor, instrument]s (i.e. "observer")
16Dec2019 Barnes integrates over all space, but for only ONE unique observer frame!! (ergo only one v). But for a forces, don't all frames count? Does it make sense to have an infinite number of forces, one per observer frame? Probably yes?
***********
ToDos - symbols :
24Jul2018 tranLists: insert tabs to make columns align!! (should write an operator for that!!)
24Jul2018 add "symList bads $symSet.txt" to "symbols sort-archive-move, post-manual-class.sh" !!!
26Jul2018 sorts of [sym,tran]Lists must be done by QNial, as QNial does symbol processing and [QNial,bash] sorts differ!
27Jul2018 What is the correct format of 'E0pcs(POIo)' ??
'E0pcs(POIo(t),t)' seems best as POIo is moving i RFp, so it the the same as E0ocs(POI,t)
'E0pcs(POIo)' ???? NYET
but if the POI of interest is moving in BOTH RFs, that is different - special treatment (real world & curvilinear)
27Jul2018 I can go much further with symbol_check_POI_format -> eg when a variable = 0 EIpxx_zero(POIp)
(so symbol stays together!)
28Jul2018 special nomenclatures, examples :
'ETisE0pdv(POIp)' -> 'ETpdv(POIp)' is always equal to 'E0pdv(POIp)'
'EIpds(POIp)' 'EI_ZEROpds(POIp)' -> 'EIpds(POIp)' is always zero
18Sep2018 Need translation between [RFp, RFo] and create RFm (for hybrid [RFp, RFo] for minimum expression length)
18Nov2018 Make sure that lists are pre-sorted - greatly speeds up searches!
20Nov2018 sortup parnLists BEFORE using - find will go MUCH faster, can't do with exprLists
27Nov2018 file translations - lines should NOT be changed if there are no symbol substitutions
that way formatting is retained over time
might be hard to do, especially as multi-lines are consolidated!
29Nov2018, 01Dec2018
write tranCheck - to make sure that translation tables are consistent, complete, etc :
All legitimate Lucas symbols must appear in HFLN tranTable, and visa-versa!
expressions won't sub into other symbols,
01Dec2018 strOfType_extTranSub_symGenl does not address "crossover" of symbols ;
***********
17Dec2019 Theorem provers versus software verification tools
It seems that software verification tools may be more appropriate for my purposes.
WAIT until I've FINISHED my verifications, THEN look at the tools. It's not clear that ANY will be appropriate, or reasonable to use.
+-----+
Symbolic math software
http://www.MapleSoft.com
http://www.cl.cam.ac.uk/research/hvg/Isabelle/
LMDE2 Software Manager :
Why3 software verification tool - It generates proof obligations for many systems:
the proof assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar
the decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.
Spin formal software verification tool
I purchased matlab (after 20+ years!!)
+-----+
Plato again!
https://scholarworks.umt.edu/cgi/viewcontent.cgi?article=1379&context=tme
Plato on the foundations of Modern Theorem Provers
Ines Hipolito
Hipolito, Ines (2016) "Plato on the foundations of Modern Theorem Provers," The Mathematics Enthusiast: Vol. 13 : No. 3 , Article 8. Available at: https://scholarworks.umt.edu/tme/vol13/iss3/8
Hipolito 2016 Plato on the foundations of Modern Theorem Provers.pdf
Nowadays, there is a large number of computer provers, that can check or construct computer assisted proofs, such as the HOL Light for classical and higher order logic, based on a formulation of type theory; and Coq. The theorem provers allow the expression of mathematical assertions; mechanically checks proofs; helps to find computer assisted proofs; and extracts a certified program from the constructive proof of its formal specification. Other theorem provers are Mizar, PVS, Otter/Ivy, Isabelle/Isar, Affa/Agda, ACL2, PhoX, IMPS, Metamath, Theorema, Lego, Nuprl, Ωmega, B method and Minlog.
+-----+
https://golem.ph.utexas.edu/category/2007/04/automated_theorem_proving.html
Posted by: Michael Kinyon on April 5, 2007 3:23 PM
"... Well, there are those of us who use automated theorem provers, but don’t hold the computer’s hand to make them prove known results or to win competitions. Rather we use them in our research to discover new results.
..."
"... Eventually, with enough patience, I can get a proof that is not only checkable by humans (as any proof generated by this kind of software is, at least in principle), but is, in fact, comprehensible. ..."
>> awesome, author had to simplify prover output to make it human comprehensible
***********
*****************************
OLD ToDos
06Jul2018 09:44 failed symTranslate_string_tests [5,5a,9,9a,10] - blanks spacing issue :
>> 1. I don't want compression as [spaces,tabs] are important to alignment
>> 2. BUT: substitution of symExpressions requires (for now) blanks compression, so substituted symExpr will be compressed
10Jul2018 SO - TIME TO GO BACK TO PHYSICS!!!
(or translate "Howell - Background math for Lucas Universal Force, Chapter 4.odt")
13Jul2018 I had to add the symbol counts manually, using :
$ paste "/media/bill/ramdisk/symTranslate_file_test f_counts.txt" "/media/bill/ramdisk/symTranslate_file_test fSym_names.txt" >>"/media/bill/ramdisk/farterg.txt"
>> ??? why didn't this work within "symTranslate_file_Lucas" -> $ bash "symbols file counts Lucas.sh"
>> do I need sleep 4s to ensure files are ready to count?
16Jul2018 incompatible QNial versus bash sorts : see "/media/bill/PROJECTS/Qnial/MY_NDFS/symbols zProcess notes.txt"
23Jul2018 CHECK if worked : "symbols classify manual.sh" must be fixed to insert tabs, not "\t"
25Jul2018 I need a bisection (not Fibonacci) search for symbols! 0 1 1 2 3 5 8 13 21 34 ...
see "/media/bill/PROJECTS/Qnial/MY_NDFS/lists.ndf", where I verified the following :
# find -> Pragmatics
The operation find uses a linear search on the items of B if the array has not been sorted, or uses a binary search algorithm if it has. The latter fact suggests that an array that is searched frequently should be kept in lexicographical order by applying sortup to it when it is created or changed.
29Jul2018 for now only the [HFLN,Lucas] symbolSets are recognized ...
29Jul2018 Corrupted arguments for symExtract_file_Lucas (changed format - must change old code)
# 02Aug2018 WARNING sym_stdForm_file: Start each input file pname_inn with an empty line, or at least NOT with one of '=<>#$%'
# For some unknown reason, first line with '=<>#$%' leads to "mashed unicode" output...
13Aug2018 symTranslate_file_Lucas IS OP f_derivations -> Changed!! as f_derivations is a "base name" without '.txt'
must change some other codes as well
28Aug2018 17:34 The Earth just moved! Day became night! A day of 36 hours!
03Sep2018 sym[Extract,Translate]_file - use file that has already been processed by sym_stdForm_file
03Sep2018 charrep now returns integers > 127 for unicodes, nit negatives!!! WHY??? - due to RaspPi unsigned ints
+-----+
IMPORTANT CHANGE :
12Sep2018 Write a separate system to "align-format" derivations!!!
This allows :
- Abandon tracking of [symbol, expression] positions - translations work in str_stdForm
- I still need typeList
- symExtract_stringRecur IS OP str_stdForm - doesn't have to return symType?
HUGE difference :
- enormously simplify sym[Extract, Translate]
- highly useful for non-aligned derivations and adhoc work day-by-day
- allows changes in symTrans_lineType within a single line of text - i.e. mixing of symTrans_lineTypes
- allows comments to be put almost anywhere
- no need to "close" symTrans_lineType areas - simply "switch" to new symTrans_lineType anywhere within the text
+-----+
06Dec2018 Symbolic processing software. Yoonsuck Choe : can't find my notes!!
I purchased matlab (after 20+ years!!)
/home/bill/matlab
# enddoc